1(* Title: HOL/Groups.thy 2 Author: Gertrud Bauer 3 Author: Steven Obua 4 Author: Lawrence C Paulson 5 Author: Markus Wenzel 6 Author: Jeremy Avigad 7*) 8 9section \<open>Groups, also combined with orderings\<close> 10 11theory Groups 12 imports Orderings 13begin 14 15subsection \<open>Dynamic facts\<close> 16 17named_theorems ac_simps "associativity and commutativity simplification rules" 18 and algebra_simps "algebra simplification rules" 19 and field_simps "algebra simplification rules for fields" 20 21text \<open> 22 The rewrites accumulated in \<open>algebra_simps\<close> deal with the classical 23 algebraic structures of groups, rings and family. They simplify terms by 24 multiplying everything out (in case of a ring) and bringing sums and 25 products into a canonical form (by ordered rewriting). As a result it 26 decides group and ring equalities but also helps with inequalities. 27 28 Of course it also works for fields, but it knows nothing about 29 multiplicative inverses or division. This is catered for by \<open>field_simps\<close>. 30 31 Facts in \<open>field_simps\<close> multiply with denominators in (in)equations if they 32 can be proved to be non-zero (for equations) or positive/negative (for 33 inequalities). Can be too aggressive and is therefore separate from the more 34 benign \<open>algebra_simps\<close>. 35\<close> 36 37 38subsection \<open>Abstract structures\<close> 39 40text \<open> 41 These locales provide basic structures for interpretation into bigger 42 structures; extensions require careful thinking, otherwise undesired effects 43 may occur due to interpretation. 44\<close> 45 46locale semigroup = 47 fixes f :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<^bold>*" 70) 48 assumes assoc [ac_simps]: "a \<^bold>* b \<^bold>* c = a \<^bold>* (b \<^bold>* c)" 49 50locale abel_semigroup = semigroup + 51 assumes commute [ac_simps]: "a \<^bold>* b = b \<^bold>* a" 52begin 53 54lemma left_commute [ac_simps]: "b \<^bold>* (a \<^bold>* c) = a \<^bold>* (b \<^bold>* c)" 55proof - 56 have "(b \<^bold>* a) \<^bold>* c = (a \<^bold>* b) \<^bold>* c" 57 by (simp only: commute) 58 then show ?thesis 59 by (simp only: assoc) 60qed 61 62end 63 64locale monoid = semigroup + 65 fixes z :: 'a ("\<^bold>1") 66 assumes left_neutral [simp]: "\<^bold>1 \<^bold>* a = a" 67 assumes right_neutral [simp]: "a \<^bold>* \<^bold>1 = a" 68 69locale comm_monoid = abel_semigroup + 70 fixes z :: 'a ("\<^bold>1") 71 assumes comm_neutral: "a \<^bold>* \<^bold>1 = a" 72begin 73 74sublocale monoid 75 by standard (simp_all add: commute comm_neutral) 76 77end 78 79locale group = semigroup + 80 fixes z :: 'a ("\<^bold>1") 81 fixes inverse :: "'a \<Rightarrow> 'a" 82 assumes group_left_neutral: "\<^bold>1 \<^bold>* a = a" 83 assumes left_inverse [simp]: "inverse a \<^bold>* a = \<^bold>1" 84begin 85 86lemma left_cancel: "a \<^bold>* b = a \<^bold>* c \<longleftrightarrow> b = c" 87proof 88 assume "a \<^bold>* b = a \<^bold>* c" 89 then have "inverse a \<^bold>* (a \<^bold>* b) = inverse a \<^bold>* (a \<^bold>* c)" by simp 90 then have "(inverse a \<^bold>* a) \<^bold>* b = (inverse a \<^bold>* a) \<^bold>* c" 91 by (simp only: assoc) 92 then show "b = c" by (simp add: group_left_neutral) 93qed simp 94 95sublocale monoid 96proof 97 fix a 98 have "inverse a \<^bold>* a = \<^bold>1" by simp 99 then have "inverse a \<^bold>* (a \<^bold>* \<^bold>1) = inverse a \<^bold>* a" 100 by (simp add: group_left_neutral assoc [symmetric]) 101 with left_cancel show "a \<^bold>* \<^bold>1 = a" 102 by (simp only: left_cancel) 103qed (fact group_left_neutral) 104 105lemma inverse_unique: 106 assumes "a \<^bold>* b = \<^bold>1" 107 shows "inverse a = b" 108proof - 109 from assms have "inverse a \<^bold>* (a \<^bold>* b) = inverse a" 110 by simp 111 then show ?thesis 112 by (simp add: assoc [symmetric]) 113qed 114 115lemma inverse_neutral [simp]: "inverse \<^bold>1 = \<^bold>1" 116 by (rule inverse_unique) simp 117 118lemma inverse_inverse [simp]: "inverse (inverse a) = a" 119 by (rule inverse_unique) simp 120 121lemma right_inverse [simp]: "a \<^bold>* inverse a = \<^bold>1" 122proof - 123 have "a \<^bold>* inverse a = inverse (inverse a) \<^bold>* inverse a" 124 by simp 125 also have "\<dots> = \<^bold>1" 126 by (rule left_inverse) 127 then show ?thesis by simp 128qed 129 130lemma inverse_distrib_swap: "inverse (a \<^bold>* b) = inverse b \<^bold>* inverse a" 131proof (rule inverse_unique) 132 have "a \<^bold>* b \<^bold>* (inverse b \<^bold>* inverse a) = 133 a \<^bold>* (b \<^bold>* inverse b) \<^bold>* inverse a" 134 by (simp only: assoc) 135 also have "\<dots> = \<^bold>1" 136 by simp 137 finally show "a \<^bold>* b \<^bold>* (inverse b \<^bold>* inverse a) = \<^bold>1" . 138qed 139 140lemma right_cancel: "b \<^bold>* a = c \<^bold>* a \<longleftrightarrow> b = c" 141proof 142 assume "b \<^bold>* a = c \<^bold>* a" 143 then have "b \<^bold>* a \<^bold>* inverse a= c \<^bold>* a \<^bold>* inverse a" 144 by simp 145 then show "b = c" 146 by (simp add: assoc) 147qed simp 148 149end 150 151 152subsection \<open>Generic operations\<close> 153 154class zero = 155 fixes zero :: 'a ("0") 156 157class one = 158 fixes one :: 'a ("1") 159 160hide_const (open) zero one 161 162lemma Let_0 [simp]: "Let 0 f = f 0" 163 unfolding Let_def .. 164 165lemma Let_1 [simp]: "Let 1 f = f 1" 166 unfolding Let_def .. 167 168setup \<open> 169 Reorient_Proc.add 170 (fn Const(@{const_name Groups.zero}, _) => true 171 | Const(@{const_name Groups.one}, _) => true 172 | _ => false) 173\<close> 174 175simproc_setup reorient_zero ("0 = x") = Reorient_Proc.proc 176simproc_setup reorient_one ("1 = x") = Reorient_Proc.proc 177 178typed_print_translation \<open> 179 let 180 fun tr' c = (c, fn ctxt => fn T => fn ts => 181 if null ts andalso Printer.type_emphasis ctxt T then 182 Syntax.const @{syntax_const "_constrain"} $ Syntax.const c $ 183 Syntax_Phases.term_of_typ ctxt T 184 else raise Match); 185 in map tr' [@{const_syntax Groups.one}, @{const_syntax Groups.zero}] end; 186\<close> \<comment> \<open>show types that are presumably too general\<close> 187 188class plus = 189 fixes plus :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "+" 65) 190 191class minus = 192 fixes minus :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "-" 65) 193 194class uminus = 195 fixes uminus :: "'a \<Rightarrow> 'a" ("- _" [81] 80) 196 197class times = 198 fixes times :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "*" 70) 199 200 201subsection \<open>Semigroups and Monoids\<close> 202 203class semigroup_add = plus + 204 assumes add_assoc [algebra_simps, field_simps]: "(a + b) + c = a + (b + c)" 205begin 206 207sublocale add: semigroup plus 208 by standard (fact add_assoc) 209 210end 211 212hide_fact add_assoc 213 214class ab_semigroup_add = semigroup_add + 215 assumes add_commute [algebra_simps, field_simps]: "a + b = b + a" 216begin 217 218sublocale add: abel_semigroup plus 219 by standard (fact add_commute) 220 221declare add.left_commute [algebra_simps, field_simps] 222 223lemmas add_ac = add.assoc add.commute add.left_commute 224 225end 226 227hide_fact add_commute 228 229lemmas add_ac = add.assoc add.commute add.left_commute 230 231class semigroup_mult = times + 232 assumes mult_assoc [algebra_simps, field_simps]: "(a * b) * c = a * (b * c)" 233begin 234 235sublocale mult: semigroup times 236 by standard (fact mult_assoc) 237 238end 239 240hide_fact mult_assoc 241 242class ab_semigroup_mult = semigroup_mult + 243 assumes mult_commute [algebra_simps, field_simps]: "a * b = b * a" 244begin 245 246sublocale mult: abel_semigroup times 247 by standard (fact mult_commute) 248 249declare mult.left_commute [algebra_simps, field_simps] 250 251lemmas mult_ac = mult.assoc mult.commute mult.left_commute 252 253end 254 255hide_fact mult_commute 256 257lemmas mult_ac = mult.assoc mult.commute mult.left_commute 258 259class monoid_add = zero + semigroup_add + 260 assumes add_0_left: "0 + a = a" 261 and add_0_right: "a + 0 = a" 262begin 263 264sublocale add: monoid plus 0 265 by standard (fact add_0_left add_0_right)+ 266 267end 268 269lemma zero_reorient: "0 = x \<longleftrightarrow> x = 0" 270 by (fact eq_commute) 271 272class comm_monoid_add = zero + ab_semigroup_add + 273 assumes add_0: "0 + a = a" 274begin 275 276subclass monoid_add 277 by standard (simp_all add: add_0 add.commute [of _ 0]) 278 279sublocale add: comm_monoid plus 0 280 by standard (simp add: ac_simps) 281 282end 283 284class monoid_mult = one + semigroup_mult + 285 assumes mult_1_left: "1 * a = a" 286 and mult_1_right: "a * 1 = a" 287begin 288 289sublocale mult: monoid times 1 290 by standard (fact mult_1_left mult_1_right)+ 291 292end 293 294lemma one_reorient: "1 = x \<longleftrightarrow> x = 1" 295 by (fact eq_commute) 296 297class comm_monoid_mult = one + ab_semigroup_mult + 298 assumes mult_1: "1 * a = a" 299begin 300 301subclass monoid_mult 302 by standard (simp_all add: mult_1 mult.commute [of _ 1]) 303 304sublocale mult: comm_monoid times 1 305 by standard (simp add: ac_simps) 306 307end 308 309class cancel_semigroup_add = semigroup_add + 310 assumes add_left_imp_eq: "a + b = a + c \<Longrightarrow> b = c" 311 assumes add_right_imp_eq: "b + a = c + a \<Longrightarrow> b = c" 312begin 313 314lemma add_left_cancel [simp]: "a + b = a + c \<longleftrightarrow> b = c" 315 by (blast dest: add_left_imp_eq) 316 317lemma add_right_cancel [simp]: "b + a = c + a \<longleftrightarrow> b = c" 318 by (blast dest: add_right_imp_eq) 319 320end 321 322class cancel_ab_semigroup_add = ab_semigroup_add + minus + 323 assumes add_diff_cancel_left' [simp]: "(a + b) - a = b" 324 assumes diff_diff_add [algebra_simps, field_simps]: "a - b - c = a - (b + c)" 325begin 326 327lemma add_diff_cancel_right' [simp]: "(a + b) - b = a" 328 using add_diff_cancel_left' [of b a] by (simp add: ac_simps) 329 330subclass cancel_semigroup_add 331proof 332 fix a b c :: 'a 333 assume "a + b = a + c" 334 then have "a + b - a = a + c - a" 335 by simp 336 then show "b = c" 337 by simp 338next 339 fix a b c :: 'a 340 assume "b + a = c + a" 341 then have "b + a - a = c + a - a" 342 by simp 343 then show "b = c" 344 by simp 345qed 346 347lemma add_diff_cancel_left [simp]: "(c + a) - (c + b) = a - b" 348 unfolding diff_diff_add [symmetric] by simp 349 350lemma add_diff_cancel_right [simp]: "(a + c) - (b + c) = a - b" 351 using add_diff_cancel_left [symmetric] by (simp add: ac_simps) 352 353lemma diff_right_commute: "a - c - b = a - b - c" 354 by (simp add: diff_diff_add add.commute) 355 356end 357 358class cancel_comm_monoid_add = cancel_ab_semigroup_add + comm_monoid_add 359begin 360 361lemma diff_zero [simp]: "a - 0 = a" 362 using add_diff_cancel_right' [of a 0] by simp 363 364lemma diff_cancel [simp]: "a - a = 0" 365proof - 366 have "(a + 0) - (a + 0) = 0" 367 by (simp only: add_diff_cancel_left diff_zero) 368 then show ?thesis by simp 369qed 370 371lemma add_implies_diff: 372 assumes "c + b = a" 373 shows "c = a - b" 374proof - 375 from assms have "(b + c) - (b + 0) = a - b" 376 by (simp add: add.commute) 377 then show "c = a - b" by simp 378qed 379 380lemma add_cancel_right_right [simp]: "a = a + b \<longleftrightarrow> b = 0" 381 (is "?P \<longleftrightarrow> ?Q") 382proof 383 assume ?Q 384 then show ?P by simp 385next 386 assume ?P 387 then have "a - a = a + b - a" by simp 388 then show ?Q by simp 389qed 390 391lemma add_cancel_right_left [simp]: "a = b + a \<longleftrightarrow> b = 0" 392 using add_cancel_right_right [of a b] by (simp add: ac_simps) 393 394lemma add_cancel_left_right [simp]: "a + b = a \<longleftrightarrow> b = 0" 395 by (auto dest: sym) 396 397lemma add_cancel_left_left [simp]: "b + a = a \<longleftrightarrow> b = 0" 398 by (auto dest: sym) 399 400end 401 402class comm_monoid_diff = cancel_comm_monoid_add + 403 assumes zero_diff [simp]: "0 - a = 0" 404begin 405 406lemma diff_add_zero [simp]: "a - (a + b) = 0" 407proof - 408 have "a - (a + b) = (a + 0) - (a + b)" 409 by simp 410 also have "\<dots> = 0" 411 by (simp only: add_diff_cancel_left zero_diff) 412 finally show ?thesis . 413qed 414 415end 416 417 418subsection \<open>Groups\<close> 419 420class group_add = minus + uminus + monoid_add + 421 assumes left_minus: "- a + a = 0" 422 assumes add_uminus_conv_diff [simp]: "a + (- b) = a - b" 423begin 424 425lemma diff_conv_add_uminus: "a - b = a + (- b)" 426 by simp 427 428sublocale add: group plus 0 uminus 429 by standard (simp_all add: left_minus) 430 431lemma minus_unique: "a + b = 0 \<Longrightarrow> - a = b" 432 by (fact add.inverse_unique) 433 434lemma minus_zero: "- 0 = 0" 435 by (fact add.inverse_neutral) 436 437lemma minus_minus: "- (- a) = a" 438 by (fact add.inverse_inverse) 439 440lemma right_minus: "a + - a = 0" 441 by (fact add.right_inverse) 442 443lemma diff_self [simp]: "a - a = 0" 444 using right_minus [of a] by simp 445 446subclass cancel_semigroup_add 447 by standard (simp_all add: add.left_cancel add.right_cancel) 448 449lemma minus_add_cancel [simp]: "- a + (a + b) = b" 450 by (simp add: add.assoc [symmetric]) 451 452lemma add_minus_cancel [simp]: "a + (- a + b) = b" 453 by (simp add: add.assoc [symmetric]) 454 455lemma diff_add_cancel [simp]: "a - b + b = a" 456 by (simp only: diff_conv_add_uminus add.assoc) simp 457 458lemma add_diff_cancel [simp]: "a + b - b = a" 459 by (simp only: diff_conv_add_uminus add.assoc) simp 460 461lemma minus_add: "- (a + b) = - b + - a" 462 by (fact add.inverse_distrib_swap) 463 464lemma right_minus_eq [simp]: "a - b = 0 \<longleftrightarrow> a = b" 465proof 466 assume "a - b = 0" 467 have "a = (a - b) + b" by (simp add: add.assoc) 468 also have "\<dots> = b" using \<open>a - b = 0\<close> by simp 469 finally show "a = b" . 470next 471 assume "a = b" 472 then show "a - b = 0" by simp 473qed 474 475lemma eq_iff_diff_eq_0: "a = b \<longleftrightarrow> a - b = 0" 476 by (fact right_minus_eq [symmetric]) 477 478lemma diff_0 [simp]: "0 - a = - a" 479 by (simp only: diff_conv_add_uminus add_0_left) 480 481lemma diff_0_right [simp]: "a - 0 = a" 482 by (simp only: diff_conv_add_uminus minus_zero add_0_right) 483 484lemma diff_minus_eq_add [simp]: "a - - b = a + b" 485 by (simp only: diff_conv_add_uminus minus_minus) 486 487lemma neg_equal_iff_equal [simp]: "- a = - b \<longleftrightarrow> a = b" 488proof 489 assume "- a = - b" 490 then have "- (- a) = - (- b)" by simp 491 then show "a = b" by simp 492next 493 assume "a = b" 494 then show "- a = - b" by simp 495qed 496 497lemma neg_equal_0_iff_equal [simp]: "- a = 0 \<longleftrightarrow> a = 0" 498 by (subst neg_equal_iff_equal [symmetric]) simp 499 500lemma neg_0_equal_iff_equal [simp]: "0 = - a \<longleftrightarrow> 0 = a" 501 by (subst neg_equal_iff_equal [symmetric]) simp 502 503text \<open>The next two equations can make the simplifier loop!\<close> 504 505lemma equation_minus_iff: "a = - b \<longleftrightarrow> b = - a" 506proof - 507 have "- (- a) = - b \<longleftrightarrow> - a = b" 508 by (rule neg_equal_iff_equal) 509 then show ?thesis 510 by (simp add: eq_commute) 511qed 512 513lemma minus_equation_iff: "- a = b \<longleftrightarrow> - b = a" 514proof - 515 have "- a = - (- b) \<longleftrightarrow> a = -b" 516 by (rule neg_equal_iff_equal) 517 then show ?thesis 518 by (simp add: eq_commute) 519qed 520 521lemma eq_neg_iff_add_eq_0: "a = - b \<longleftrightarrow> a + b = 0" 522proof 523 assume "a = - b" 524 then show "a + b = 0" by simp 525next 526 assume "a + b = 0" 527 moreover have "a + (b + - b) = (a + b) + - b" 528 by (simp only: add.assoc) 529 ultimately show "a = - b" 530 by simp 531qed 532 533lemma add_eq_0_iff2: "a + b = 0 \<longleftrightarrow> a = - b" 534 by (fact eq_neg_iff_add_eq_0 [symmetric]) 535 536lemma neg_eq_iff_add_eq_0: "- a = b \<longleftrightarrow> a + b = 0" 537 by (auto simp add: add_eq_0_iff2) 538 539lemma add_eq_0_iff: "a + b = 0 \<longleftrightarrow> b = - a" 540 by (auto simp add: neg_eq_iff_add_eq_0 [symmetric]) 541 542lemma minus_diff_eq [simp]: "- (a - b) = b - a" 543 by (simp only: neg_eq_iff_add_eq_0 diff_conv_add_uminus add.assoc minus_add_cancel) simp 544 545lemma add_diff_eq [algebra_simps, field_simps]: "a + (b - c) = (a + b) - c" 546 by (simp only: diff_conv_add_uminus add.assoc) 547 548lemma diff_add_eq_diff_diff_swap: "a - (b + c) = a - c - b" 549 by (simp only: diff_conv_add_uminus add.assoc minus_add) 550 551lemma diff_eq_eq [algebra_simps, field_simps]: "a - b = c \<longleftrightarrow> a = c + b" 552 by auto 553 554lemma eq_diff_eq [algebra_simps, field_simps]: "a = c - b \<longleftrightarrow> a + b = c" 555 by auto 556 557lemma diff_diff_eq2 [algebra_simps, field_simps]: "a - (b - c) = (a + c) - b" 558 by (simp only: diff_conv_add_uminus add.assoc) simp 559 560lemma diff_eq_diff_eq: "a - b = c - d \<Longrightarrow> a = b \<longleftrightarrow> c = d" 561 by (simp only: eq_iff_diff_eq_0 [of a b] eq_iff_diff_eq_0 [of c d]) 562 563end 564 565class ab_group_add = minus + uminus + comm_monoid_add + 566 assumes ab_left_minus: "- a + a = 0" 567 assumes ab_diff_conv_add_uminus: "a - b = a + (- b)" 568begin 569 570subclass group_add 571 by standard (simp_all add: ab_left_minus ab_diff_conv_add_uminus) 572 573subclass cancel_comm_monoid_add 574proof 575 fix a b c :: 'a 576 have "b + a - a = b" 577 by simp 578 then show "a + b - a = b" 579 by (simp add: ac_simps) 580 show "a - b - c = a - (b + c)" 581 by (simp add: algebra_simps) 582qed 583 584lemma uminus_add_conv_diff [simp]: "- a + b = b - a" 585 by (simp add: add.commute) 586 587lemma minus_add_distrib [simp]: "- (a + b) = - a + - b" 588 by (simp add: algebra_simps) 589 590lemma diff_add_eq [algebra_simps, field_simps]: "(a - b) + c = (a + c) - b" 591 by (simp add: algebra_simps) 592 593end 594 595 596subsection \<open>(Partially) Ordered Groups\<close> 597 598text \<open> 599 The theory of partially ordered groups is taken from the books: 600 601 \<^item> \<^emph>\<open>Lattice Theory\<close> by Garret Birkhoff, American Mathematical Society, 1979 602 \<^item> \<^emph>\<open>Partially Ordered Algebraic Systems\<close>, Pergamon Press, 1963 603 604 Most of the used notions can also be looked up in 605 \<^item> \<^url>\<open>http://www.mathworld.com\<close> by Eric Weisstein et. al. 606 \<^item> \<^emph>\<open>Algebra I\<close> by van der Waerden, Springer 607\<close> 608 609class ordered_ab_semigroup_add = order + ab_semigroup_add + 610 assumes add_left_mono: "a \<le> b \<Longrightarrow> c + a \<le> c + b" 611begin 612 613lemma add_right_mono: "a \<le> b \<Longrightarrow> a + c \<le> b + c" 614 by (simp add: add.commute [of _ c] add_left_mono) 615 616text \<open>non-strict, in both arguments\<close> 617lemma add_mono: "a \<le> b \<Longrightarrow> c \<le> d \<Longrightarrow> a + c \<le> b + d" 618 apply (erule add_right_mono [THEN order_trans]) 619 apply (simp add: add.commute add_left_mono) 620 done 621 622end 623 624text \<open>Strict monotonicity in both arguments\<close> 625class strict_ordered_ab_semigroup_add = ordered_ab_semigroup_add + 626 assumes add_strict_mono: "a < b \<Longrightarrow> c < d \<Longrightarrow> a + c < b + d" 627 628class ordered_cancel_ab_semigroup_add = 629 ordered_ab_semigroup_add + cancel_ab_semigroup_add 630begin 631 632lemma add_strict_left_mono: "a < b \<Longrightarrow> c + a < c + b" 633 by (auto simp add: less_le add_left_mono) 634 635lemma add_strict_right_mono: "a < b \<Longrightarrow> a + c < b + c" 636 by (simp add: add.commute [of _ c] add_strict_left_mono) 637 638subclass strict_ordered_ab_semigroup_add 639 apply standard 640 apply (erule add_strict_right_mono [THEN less_trans]) 641 apply (erule add_strict_left_mono) 642 done 643 644lemma add_less_le_mono: "a < b \<Longrightarrow> c \<le> d \<Longrightarrow> a + c < b + d" 645 apply (erule add_strict_right_mono [THEN less_le_trans]) 646 apply (erule add_left_mono) 647 done 648 649lemma add_le_less_mono: "a \<le> b \<Longrightarrow> c < d \<Longrightarrow> a + c < b + d" 650 apply (erule add_right_mono [THEN le_less_trans]) 651 apply (erule add_strict_left_mono) 652 done 653 654end 655 656class ordered_ab_semigroup_add_imp_le = ordered_cancel_ab_semigroup_add + 657 assumes add_le_imp_le_left: "c + a \<le> c + b \<Longrightarrow> a \<le> b" 658begin 659 660lemma add_less_imp_less_left: 661 assumes less: "c + a < c + b" 662 shows "a < b" 663proof - 664 from less have le: "c + a \<le> c + b" 665 by (simp add: order_le_less) 666 have "a \<le> b" 667 apply (insert le) 668 apply (drule add_le_imp_le_left) 669 apply (insert le) 670 apply (drule add_le_imp_le_left) 671 apply assumption 672 done 673 moreover have "a \<noteq> b" 674 proof (rule ccontr) 675 assume "\<not> ?thesis" 676 then have "a = b" by simp 677 then have "c + a = c + b" by simp 678 with less show "False" by simp 679 qed 680 ultimately show "a < b" 681 by (simp add: order_le_less) 682qed 683 684lemma add_less_imp_less_right: "a + c < b + c \<Longrightarrow> a < b" 685 by (rule add_less_imp_less_left [of c]) (simp add: add.commute) 686 687lemma add_less_cancel_left [simp]: "c + a < c + b \<longleftrightarrow> a < b" 688 by (blast intro: add_less_imp_less_left add_strict_left_mono) 689 690lemma add_less_cancel_right [simp]: "a + c < b + c \<longleftrightarrow> a < b" 691 by (blast intro: add_less_imp_less_right add_strict_right_mono) 692 693lemma add_le_cancel_left [simp]: "c + a \<le> c + b \<longleftrightarrow> a \<le> b" 694 apply auto 695 apply (drule add_le_imp_le_left) 696 apply (simp_all add: add_left_mono) 697 done 698 699lemma add_le_cancel_right [simp]: "a + c \<le> b + c \<longleftrightarrow> a \<le> b" 700 by (simp add: add.commute [of a c] add.commute [of b c]) 701 702lemma add_le_imp_le_right: "a + c \<le> b + c \<Longrightarrow> a \<le> b" 703 by simp 704 705lemma max_add_distrib_left: "max x y + z = max (x + z) (y + z)" 706 unfolding max_def by auto 707 708lemma min_add_distrib_left: "min x y + z = min (x + z) (y + z)" 709 unfolding min_def by auto 710 711lemma max_add_distrib_right: "x + max y z = max (x + y) (x + z)" 712 unfolding max_def by auto 713 714lemma min_add_distrib_right: "x + min y z = min (x + y) (x + z)" 715 unfolding min_def by auto 716 717end 718 719subsection \<open>Support for reasoning about signs\<close> 720 721class ordered_comm_monoid_add = comm_monoid_add + ordered_ab_semigroup_add 722begin 723 724lemma add_nonneg_nonneg [simp]: "0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 \<le> a + b" 725 using add_mono[of 0 a 0 b] by simp 726 727lemma add_nonpos_nonpos: "a \<le> 0 \<Longrightarrow> b \<le> 0 \<Longrightarrow> a + b \<le> 0" 728 using add_mono[of a 0 b 0] by simp 729 730lemma add_nonneg_eq_0_iff: "0 \<le> x \<Longrightarrow> 0 \<le> y \<Longrightarrow> x + y = 0 \<longleftrightarrow> x = 0 \<and> y = 0" 731 using add_left_mono[of 0 y x] add_right_mono[of 0 x y] by auto 732 733lemma add_nonpos_eq_0_iff: "x \<le> 0 \<Longrightarrow> y \<le> 0 \<Longrightarrow> x + y = 0 \<longleftrightarrow> x = 0 \<and> y = 0" 734 using add_left_mono[of y 0 x] add_right_mono[of x 0 y] by auto 735 736lemma add_increasing: "0 \<le> a \<Longrightarrow> b \<le> c \<Longrightarrow> b \<le> a + c" 737 using add_mono [of 0 a b c] by simp 738 739lemma add_increasing2: "0 \<le> c \<Longrightarrow> b \<le> a \<Longrightarrow> b \<le> a + c" 740 by (simp add: add_increasing add.commute [of a]) 741 742lemma add_decreasing: "a \<le> 0 \<Longrightarrow> c \<le> b \<Longrightarrow> a + c \<le> b" 743 using add_mono [of a 0 c b] by simp 744 745lemma add_decreasing2: "c \<le> 0 \<Longrightarrow> a \<le> b \<Longrightarrow> a + c \<le> b" 746 using add_mono[of a b c 0] by simp 747 748lemma add_pos_nonneg: "0 < a \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 < a + b" 749 using less_le_trans[of 0 a "a + b"] by (simp add: add_increasing2) 750 751lemma add_pos_pos: "0 < a \<Longrightarrow> 0 < b \<Longrightarrow> 0 < a + b" 752 by (intro add_pos_nonneg less_imp_le) 753 754lemma add_nonneg_pos: "0 \<le> a \<Longrightarrow> 0 < b \<Longrightarrow> 0 < a + b" 755 using add_pos_nonneg[of b a] by (simp add: add_commute) 756 757lemma add_neg_nonpos: "a < 0 \<Longrightarrow> b \<le> 0 \<Longrightarrow> a + b < 0" 758 using le_less_trans[of "a + b" a 0] by (simp add: add_decreasing2) 759 760lemma add_neg_neg: "a < 0 \<Longrightarrow> b < 0 \<Longrightarrow> a + b < 0" 761 by (intro add_neg_nonpos less_imp_le) 762 763lemma add_nonpos_neg: "a \<le> 0 \<Longrightarrow> b < 0 \<Longrightarrow> a + b < 0" 764 using add_neg_nonpos[of b a] by (simp add: add_commute) 765 766lemmas add_sign_intros = 767 add_pos_nonneg add_pos_pos add_nonneg_pos add_nonneg_nonneg 768 add_neg_nonpos add_neg_neg add_nonpos_neg add_nonpos_nonpos 769 770end 771 772class strict_ordered_comm_monoid_add = comm_monoid_add + strict_ordered_ab_semigroup_add 773begin 774 775lemma pos_add_strict: "0 < a \<Longrightarrow> b < c \<Longrightarrow> b < a + c" 776 using add_strict_mono [of 0 a b c] by simp 777 778end 779 780class ordered_cancel_comm_monoid_add = ordered_comm_monoid_add + cancel_ab_semigroup_add 781begin 782 783subclass ordered_cancel_ab_semigroup_add .. 784subclass strict_ordered_comm_monoid_add .. 785 786lemma add_strict_increasing: "0 < a \<Longrightarrow> b \<le> c \<Longrightarrow> b < a + c" 787 using add_less_le_mono [of 0 a b c] by simp 788 789lemma add_strict_increasing2: "0 \<le> a \<Longrightarrow> b < c \<Longrightarrow> b < a + c" 790 using add_le_less_mono [of 0 a b c] by simp 791 792end 793 794class ordered_ab_semigroup_monoid_add_imp_le = monoid_add + ordered_ab_semigroup_add_imp_le 795begin 796 797lemma add_less_same_cancel1 [simp]: "b + a < b \<longleftrightarrow> a < 0" 798 using add_less_cancel_left [of _ _ 0] by simp 799 800lemma add_less_same_cancel2 [simp]: "a + b < b \<longleftrightarrow> a < 0" 801 using add_less_cancel_right [of _ _ 0] by simp 802 803lemma less_add_same_cancel1 [simp]: "a < a + b \<longleftrightarrow> 0 < b" 804 using add_less_cancel_left [of _ 0] by simp 805 806lemma less_add_same_cancel2 [simp]: "a < b + a \<longleftrightarrow> 0 < b" 807 using add_less_cancel_right [of 0] by simp 808 809lemma add_le_same_cancel1 [simp]: "b + a \<le> b \<longleftrightarrow> a \<le> 0" 810 using add_le_cancel_left [of _ _ 0] by simp 811 812lemma add_le_same_cancel2 [simp]: "a + b \<le> b \<longleftrightarrow> a \<le> 0" 813 using add_le_cancel_right [of _ _ 0] by simp 814 815lemma le_add_same_cancel1 [simp]: "a \<le> a + b \<longleftrightarrow> 0 \<le> b" 816 using add_le_cancel_left [of _ 0] by simp 817 818lemma le_add_same_cancel2 [simp]: "a \<le> b + a \<longleftrightarrow> 0 \<le> b" 819 using add_le_cancel_right [of 0] by simp 820 821subclass cancel_comm_monoid_add 822 by standard auto 823 824subclass ordered_cancel_comm_monoid_add 825 by standard 826 827end 828 829class ordered_ab_group_add = ab_group_add + ordered_ab_semigroup_add 830begin 831 832subclass ordered_cancel_ab_semigroup_add .. 833 834subclass ordered_ab_semigroup_monoid_add_imp_le 835proof 836 fix a b c :: 'a 837 assume "c + a \<le> c + b" 838 then have "(-c) + (c + a) \<le> (-c) + (c + b)" 839 by (rule add_left_mono) 840 then have "((-c) + c) + a \<le> ((-c) + c) + b" 841 by (simp only: add.assoc) 842 then show "a \<le> b" by simp 843qed 844 845lemma max_diff_distrib_left: "max x y - z = max (x - z) (y - z)" 846 using max_add_distrib_left [of x y "- z"] by simp 847 848lemma min_diff_distrib_left: "min x y - z = min (x - z) (y - z)" 849 using min_add_distrib_left [of x y "- z"] by simp 850 851lemma le_imp_neg_le: 852 assumes "a \<le> b" 853 shows "- b \<le> - a" 854proof - 855 from assms have "- a + a \<le> - a + b" 856 by (rule add_left_mono) 857 then have "0 \<le> - a + b" 858 by simp 859 then have "0 + (- b) \<le> (- a + b) + (- b)" 860 by (rule add_right_mono) 861 then show ?thesis 862 by (simp add: algebra_simps) 863qed 864 865lemma neg_le_iff_le [simp]: "- b \<le> - a \<longleftrightarrow> a \<le> b" 866proof 867 assume "- b \<le> - a" 868 then have "- (- a) \<le> - (- b)" 869 by (rule le_imp_neg_le) 870 then show "a \<le> b" 871 by simp 872next 873 assume "a \<le> b" 874 then show "- b \<le> - a" 875 by (rule le_imp_neg_le) 876qed 877 878lemma neg_le_0_iff_le [simp]: "- a \<le> 0 \<longleftrightarrow> 0 \<le> a" 879 by (subst neg_le_iff_le [symmetric]) simp 880 881lemma neg_0_le_iff_le [simp]: "0 \<le> - a \<longleftrightarrow> a \<le> 0" 882 by (subst neg_le_iff_le [symmetric]) simp 883 884lemma neg_less_iff_less [simp]: "- b < - a \<longleftrightarrow> a < b" 885 by (auto simp add: less_le) 886 887lemma neg_less_0_iff_less [simp]: "- a < 0 \<longleftrightarrow> 0 < a" 888 by (subst neg_less_iff_less [symmetric]) simp 889 890lemma neg_0_less_iff_less [simp]: "0 < - a \<longleftrightarrow> a < 0" 891 by (subst neg_less_iff_less [symmetric]) simp 892 893text \<open>The next several equations can make the simplifier loop!\<close> 894 895lemma less_minus_iff: "a < - b \<longleftrightarrow> b < - a" 896proof - 897 have "- (- a) < - b \<longleftrightarrow> b < - a" 898 by (rule neg_less_iff_less) 899 then show ?thesis by simp 900qed 901 902lemma minus_less_iff: "- a < b \<longleftrightarrow> - b < a" 903proof - 904 have "- a < - (- b) \<longleftrightarrow> - b < a" 905 by (rule neg_less_iff_less) 906 then show ?thesis by simp 907qed 908 909lemma le_minus_iff: "a \<le> - b \<longleftrightarrow> b \<le> - a" 910proof - 911 have mm: "- (- a) < - b \<Longrightarrow> - (- b) < -a" for a b :: 'a 912 by (simp only: minus_less_iff) 913 have "- (- a) \<le> - b \<longleftrightarrow> b \<le> - a" 914 apply (auto simp only: le_less) 915 apply (drule mm) 916 apply (simp_all) 917 apply (drule mm[simplified], assumption) 918 done 919 then show ?thesis by simp 920qed 921 922lemma minus_le_iff: "- a \<le> b \<longleftrightarrow> - b \<le> a" 923 by (auto simp add: le_less minus_less_iff) 924 925lemma diff_less_0_iff_less [simp]: "a - b < 0 \<longleftrightarrow> a < b" 926proof - 927 have "a - b < 0 \<longleftrightarrow> a + (- b) < b + (- b)" 928 by simp 929 also have "\<dots> \<longleftrightarrow> a < b" 930 by (simp only: add_less_cancel_right) 931 finally show ?thesis . 932qed 933 934lemmas less_iff_diff_less_0 = diff_less_0_iff_less [symmetric] 935 936lemma diff_less_eq [algebra_simps, field_simps]: "a - b < c \<longleftrightarrow> a < c + b" 937 apply (subst less_iff_diff_less_0 [of a]) 938 apply (rule less_iff_diff_less_0 [of _ c, THEN ssubst]) 939 apply (simp add: algebra_simps) 940 done 941 942lemma less_diff_eq[algebra_simps, field_simps]: "a < c - b \<longleftrightarrow> a + b < c" 943 apply (subst less_iff_diff_less_0 [of "a + b"]) 944 apply (subst less_iff_diff_less_0 [of a]) 945 apply (simp add: algebra_simps) 946 done 947 948lemma diff_gt_0_iff_gt [simp]: "a - b > 0 \<longleftrightarrow> a > b" 949 by (simp add: less_diff_eq) 950 951lemma diff_le_eq [algebra_simps, field_simps]: "a - b \<le> c \<longleftrightarrow> a \<le> c + b" 952 by (auto simp add: le_less diff_less_eq ) 953 954lemma le_diff_eq [algebra_simps, field_simps]: "a \<le> c - b \<longleftrightarrow> a + b \<le> c" 955 by (auto simp add: le_less less_diff_eq) 956 957lemma diff_le_0_iff_le [simp]: "a - b \<le> 0 \<longleftrightarrow> a \<le> b" 958 by (simp add: algebra_simps) 959 960lemmas le_iff_diff_le_0 = diff_le_0_iff_le [symmetric] 961 962lemma diff_ge_0_iff_ge [simp]: "a - b \<ge> 0 \<longleftrightarrow> a \<ge> b" 963 by (simp add: le_diff_eq) 964 965lemma diff_eq_diff_less: "a - b = c - d \<Longrightarrow> a < b \<longleftrightarrow> c < d" 966 by (auto simp only: less_iff_diff_less_0 [of a b] less_iff_diff_less_0 [of c d]) 967 968lemma diff_eq_diff_less_eq: "a - b = c - d \<Longrightarrow> a \<le> b \<longleftrightarrow> c \<le> d" 969 by (auto simp only: le_iff_diff_le_0 [of a b] le_iff_diff_le_0 [of c d]) 970 971lemma diff_mono: "a \<le> b \<Longrightarrow> d \<le> c \<Longrightarrow> a - c \<le> b - d" 972 by (simp add: field_simps add_mono) 973 974lemma diff_left_mono: "b \<le> a \<Longrightarrow> c - a \<le> c - b" 975 by (simp add: field_simps) 976 977lemma diff_right_mono: "a \<le> b \<Longrightarrow> a - c \<le> b - c" 978 by (simp add: field_simps) 979 980lemma diff_strict_mono: "a < b \<Longrightarrow> d < c \<Longrightarrow> a - c < b - d" 981 by (simp add: field_simps add_strict_mono) 982 983lemma diff_strict_left_mono: "b < a \<Longrightarrow> c - a < c - b" 984 by (simp add: field_simps) 985 986lemma diff_strict_right_mono: "a < b \<Longrightarrow> a - c < b - c" 987 by (simp add: field_simps) 988 989end 990 991ML_file "Tools/group_cancel.ML" 992 993simproc_setup group_cancel_add ("a + b::'a::ab_group_add") = 994 \<open>fn phi => fn ss => try Group_Cancel.cancel_add_conv\<close> 995 996simproc_setup group_cancel_diff ("a - b::'a::ab_group_add") = 997 \<open>fn phi => fn ss => try Group_Cancel.cancel_diff_conv\<close> 998 999simproc_setup group_cancel_eq ("a = (b::'a::ab_group_add)") = 1000 \<open>fn phi => fn ss => try Group_Cancel.cancel_eq_conv\<close> 1001 1002simproc_setup group_cancel_le ("a \<le> (b::'a::ordered_ab_group_add)") = 1003 \<open>fn phi => fn ss => try Group_Cancel.cancel_le_conv\<close> 1004 1005simproc_setup group_cancel_less ("a < (b::'a::ordered_ab_group_add)") = 1006 \<open>fn phi => fn ss => try Group_Cancel.cancel_less_conv\<close> 1007 1008class linordered_ab_semigroup_add = 1009 linorder + ordered_ab_semigroup_add 1010 1011class linordered_cancel_ab_semigroup_add = 1012 linorder + ordered_cancel_ab_semigroup_add 1013begin 1014 1015subclass linordered_ab_semigroup_add .. 1016 1017subclass ordered_ab_semigroup_add_imp_le 1018proof 1019 fix a b c :: 'a 1020 assume le1: "c + a \<le> c + b" 1021 show "a \<le> b" 1022 proof (rule ccontr) 1023 assume *: "\<not> ?thesis" 1024 then have "b \<le> a" by (simp add: linorder_not_le) 1025 then have "c + b \<le> c + a" by (rule add_left_mono) 1026 with le1 have "a = b" 1027 apply - 1028 apply (drule antisym) 1029 apply simp_all 1030 done 1031 with * show False 1032 by (simp add: linorder_not_le [symmetric]) 1033 qed 1034qed 1035 1036end 1037 1038class linordered_ab_group_add = linorder + ordered_ab_group_add 1039begin 1040 1041subclass linordered_cancel_ab_semigroup_add .. 1042 1043lemma equal_neg_zero [simp]: "a = - a \<longleftrightarrow> a = 0" 1044proof 1045 assume "a = 0" 1046 then show "a = - a" by simp 1047next 1048 assume A: "a = - a" 1049 show "a = 0" 1050 proof (cases "0 \<le> a") 1051 case True 1052 with A have "0 \<le> - a" by auto 1053 with le_minus_iff have "a \<le> 0" by simp 1054 with True show ?thesis by (auto intro: order_trans) 1055 next 1056 case False 1057 then have B: "a \<le> 0" by auto 1058 with A have "- a \<le> 0" by auto 1059 with B show ?thesis by (auto intro: order_trans) 1060 qed 1061qed 1062 1063lemma neg_equal_zero [simp]: "- a = a \<longleftrightarrow> a = 0" 1064 by (auto dest: sym) 1065 1066lemma neg_less_eq_nonneg [simp]: "- a \<le> a \<longleftrightarrow> 0 \<le> a" 1067proof 1068 assume *: "- a \<le> a" 1069 show "0 \<le> a" 1070 proof (rule classical) 1071 assume "\<not> ?thesis" 1072 then have "a < 0" by auto 1073 with * have "- a < 0" by (rule le_less_trans) 1074 then show ?thesis by auto 1075 qed 1076next 1077 assume *: "0 \<le> a" 1078 then have "- a \<le> 0" by (simp add: minus_le_iff) 1079 from this * show "- a \<le> a" by (rule order_trans) 1080qed 1081 1082lemma neg_less_pos [simp]: "- a < a \<longleftrightarrow> 0 < a" 1083 by (auto simp add: less_le) 1084 1085lemma less_eq_neg_nonpos [simp]: "a \<le> - a \<longleftrightarrow> a \<le> 0" 1086 using neg_less_eq_nonneg [of "- a"] by simp 1087 1088lemma less_neg_neg [simp]: "a < - a \<longleftrightarrow> a < 0" 1089 using neg_less_pos [of "- a"] by simp 1090 1091lemma double_zero [simp]: "a + a = 0 \<longleftrightarrow> a = 0" 1092proof 1093 assume "a + a = 0" 1094 then have a: "- a = a" by (rule minus_unique) 1095 then show "a = 0" by (simp only: neg_equal_zero) 1096next 1097 assume "a = 0" 1098 then show "a + a = 0" by simp 1099qed 1100 1101lemma double_zero_sym [simp]: "0 = a + a \<longleftrightarrow> a = 0" 1102 apply (rule iffI) 1103 apply (drule sym) 1104 apply simp_all 1105 done 1106 1107lemma zero_less_double_add_iff_zero_less_single_add [simp]: "0 < a + a \<longleftrightarrow> 0 < a" 1108proof 1109 assume "0 < a + a" 1110 then have "0 - a < a" by (simp only: diff_less_eq) 1111 then have "- a < a" by simp 1112 then show "0 < a" by simp 1113next 1114 assume "0 < a" 1115 with this have "0 + 0 < a + a" 1116 by (rule add_strict_mono) 1117 then show "0 < a + a" by simp 1118qed 1119 1120lemma zero_le_double_add_iff_zero_le_single_add [simp]: "0 \<le> a + a \<longleftrightarrow> 0 \<le> a" 1121 by (auto simp add: le_less) 1122 1123lemma double_add_less_zero_iff_single_add_less_zero [simp]: "a + a < 0 \<longleftrightarrow> a < 0" 1124proof - 1125 have "\<not> a + a < 0 \<longleftrightarrow> \<not> a < 0" 1126 by (simp add: not_less) 1127 then show ?thesis by simp 1128qed 1129 1130lemma double_add_le_zero_iff_single_add_le_zero [simp]: "a + a \<le> 0 \<longleftrightarrow> a \<le> 0" 1131proof - 1132 have "\<not> a + a \<le> 0 \<longleftrightarrow> \<not> a \<le> 0" 1133 by (simp add: not_le) 1134 then show ?thesis by simp 1135qed 1136 1137lemma minus_max_eq_min: "- max x y = min (- x) (- y)" 1138 by (auto simp add: max_def min_def) 1139 1140lemma minus_min_eq_max: "- min x y = max (- x) (- y)" 1141 by (auto simp add: max_def min_def) 1142 1143end 1144 1145class abs = 1146 fixes abs :: "'a \<Rightarrow> 'a" ("\<bar>_\<bar>") 1147 1148class sgn = 1149 fixes sgn :: "'a \<Rightarrow> 'a" 1150 1151class ordered_ab_group_add_abs = ordered_ab_group_add + abs + 1152 assumes abs_ge_zero [simp]: "\<bar>a\<bar> \<ge> 0" 1153 and abs_ge_self: "a \<le> \<bar>a\<bar>" 1154 and abs_leI: "a \<le> b \<Longrightarrow> - a \<le> b \<Longrightarrow> \<bar>a\<bar> \<le> b" 1155 and abs_minus_cancel [simp]: "\<bar>-a\<bar> = \<bar>a\<bar>" 1156 and abs_triangle_ineq: "\<bar>a + b\<bar> \<le> \<bar>a\<bar> + \<bar>b\<bar>" 1157begin 1158 1159lemma abs_minus_le_zero: "- \<bar>a\<bar> \<le> 0" 1160 unfolding neg_le_0_iff_le by simp 1161 1162lemma abs_of_nonneg [simp]: 1163 assumes nonneg: "0 \<le> a" 1164 shows "\<bar>a\<bar> = a" 1165proof (rule antisym) 1166 show "a \<le> \<bar>a\<bar>" by (rule abs_ge_self) 1167 from nonneg le_imp_neg_le have "- a \<le> 0" by simp 1168 from this nonneg have "- a \<le> a" by (rule order_trans) 1169 then show "\<bar>a\<bar> \<le> a" by (auto intro: abs_leI) 1170qed 1171 1172lemma abs_idempotent [simp]: "\<bar>\<bar>a\<bar>\<bar> = \<bar>a\<bar>" 1173 by (rule antisym) (auto intro!: abs_ge_self abs_leI order_trans [of "- \<bar>a\<bar>" 0 "\<bar>a\<bar>"]) 1174 1175lemma abs_eq_0 [simp]: "\<bar>a\<bar> = 0 \<longleftrightarrow> a = 0" 1176proof - 1177 have "\<bar>a\<bar> = 0 \<Longrightarrow> a = 0" 1178 proof (rule antisym) 1179 assume zero: "\<bar>a\<bar> = 0" 1180 with abs_ge_self show "a \<le> 0" by auto 1181 from zero have "\<bar>-a\<bar> = 0" by simp 1182 with abs_ge_self [of "- a"] have "- a \<le> 0" by auto 1183 with neg_le_0_iff_le show "0 \<le> a" by auto 1184 qed 1185 then show ?thesis by auto 1186qed 1187 1188lemma abs_zero [simp]: "\<bar>0\<bar> = 0" 1189 by simp 1190 1191lemma abs_0_eq [simp]: "0 = \<bar>a\<bar> \<longleftrightarrow> a = 0" 1192proof - 1193 have "0 = \<bar>a\<bar> \<longleftrightarrow> \<bar>a\<bar> = 0" by (simp only: eq_ac) 1194 then show ?thesis by simp 1195qed 1196 1197lemma abs_le_zero_iff [simp]: "\<bar>a\<bar> \<le> 0 \<longleftrightarrow> a = 0" 1198proof 1199 assume "\<bar>a\<bar> \<le> 0" 1200 then have "\<bar>a\<bar> = 0" by (rule antisym) simp 1201 then show "a = 0" by simp 1202next 1203 assume "a = 0" 1204 then show "\<bar>a\<bar> \<le> 0" by simp 1205qed 1206 1207lemma abs_le_self_iff [simp]: "\<bar>a\<bar> \<le> a \<longleftrightarrow> 0 \<le> a" 1208proof - 1209 have "0 \<le> \<bar>a\<bar>" 1210 using abs_ge_zero by blast 1211 then have "\<bar>a\<bar> \<le> a \<Longrightarrow> 0 \<le> a" 1212 using order.trans by blast 1213 then show ?thesis 1214 using abs_of_nonneg eq_refl by blast 1215qed 1216 1217lemma zero_less_abs_iff [simp]: "0 < \<bar>a\<bar> \<longleftrightarrow> a \<noteq> 0" 1218 by (simp add: less_le) 1219 1220lemma abs_not_less_zero [simp]: "\<not> \<bar>a\<bar> < 0" 1221proof - 1222 have "x \<le> y \<Longrightarrow> \<not> y < x" for x y by auto 1223 then show ?thesis by simp 1224qed 1225 1226lemma abs_ge_minus_self: "- a \<le> \<bar>a\<bar>" 1227proof - 1228 have "- a \<le> \<bar>-a\<bar>" by (rule abs_ge_self) 1229 then show ?thesis by simp 1230qed 1231 1232lemma abs_minus_commute: "\<bar>a - b\<bar> = \<bar>b - a\<bar>" 1233proof - 1234 have "\<bar>a - b\<bar> = \<bar>- (a - b)\<bar>" 1235 by (simp only: abs_minus_cancel) 1236 also have "\<dots> = \<bar>b - a\<bar>" by simp 1237 finally show ?thesis . 1238qed 1239 1240lemma abs_of_pos: "0 < a \<Longrightarrow> \<bar>a\<bar> = a" 1241 by (rule abs_of_nonneg) (rule less_imp_le) 1242 1243lemma abs_of_nonpos [simp]: 1244 assumes "a \<le> 0" 1245 shows "\<bar>a\<bar> = - a" 1246proof - 1247 let ?b = "- a" 1248 have "- ?b \<le> 0 \<Longrightarrow> \<bar>- ?b\<bar> = - (- ?b)" 1249 unfolding abs_minus_cancel [of ?b] 1250 unfolding neg_le_0_iff_le [of ?b] 1251 unfolding minus_minus by (erule abs_of_nonneg) 1252 then show ?thesis using assms by auto 1253qed 1254 1255lemma abs_of_neg: "a < 0 \<Longrightarrow> \<bar>a\<bar> = - a" 1256 by (rule abs_of_nonpos) (rule less_imp_le) 1257 1258lemma abs_le_D1: "\<bar>a\<bar> \<le> b \<Longrightarrow> a \<le> b" 1259 using abs_ge_self by (blast intro: order_trans) 1260 1261lemma abs_le_D2: "\<bar>a\<bar> \<le> b \<Longrightarrow> - a \<le> b" 1262 using abs_le_D1 [of "- a"] by simp 1263 1264lemma abs_le_iff: "\<bar>a\<bar> \<le> b \<longleftrightarrow> a \<le> b \<and> - a \<le> b" 1265 by (blast intro: abs_leI dest: abs_le_D1 abs_le_D2) 1266 1267lemma abs_triangle_ineq2: "\<bar>a\<bar> - \<bar>b\<bar> \<le> \<bar>a - b\<bar>" 1268proof - 1269 have "\<bar>a\<bar> = \<bar>b + (a - b)\<bar>" 1270 by (simp add: algebra_simps) 1271 then have "\<bar>a\<bar> \<le> \<bar>b\<bar> + \<bar>a - b\<bar>" 1272 by (simp add: abs_triangle_ineq) 1273 then show ?thesis 1274 by (simp add: algebra_simps) 1275qed 1276 1277lemma abs_triangle_ineq2_sym: "\<bar>a\<bar> - \<bar>b\<bar> \<le> \<bar>b - a\<bar>" 1278 by (simp only: abs_minus_commute [of b] abs_triangle_ineq2) 1279 1280lemma abs_triangle_ineq3: "\<bar>\<bar>a\<bar> - \<bar>b\<bar>\<bar> \<le> \<bar>a - b\<bar>" 1281 by (simp add: abs_le_iff abs_triangle_ineq2 abs_triangle_ineq2_sym) 1282 1283lemma abs_triangle_ineq4: "\<bar>a - b\<bar> \<le> \<bar>a\<bar> + \<bar>b\<bar>" 1284proof - 1285 have "\<bar>a - b\<bar> = \<bar>a + - b\<bar>" 1286 by (simp add: algebra_simps) 1287 also have "\<dots> \<le> \<bar>a\<bar> + \<bar>- b\<bar>" 1288 by (rule abs_triangle_ineq) 1289 finally show ?thesis by simp 1290qed 1291 1292lemma abs_diff_triangle_ineq: "\<bar>a + b - (c + d)\<bar> \<le> \<bar>a - c\<bar> + \<bar>b - d\<bar>" 1293proof - 1294 have "\<bar>a + b - (c + d)\<bar> = \<bar>(a - c) + (b - d)\<bar>" 1295 by (simp add: algebra_simps) 1296 also have "\<dots> \<le> \<bar>a - c\<bar> + \<bar>b - d\<bar>" 1297 by (rule abs_triangle_ineq) 1298 finally show ?thesis . 1299qed 1300 1301lemma abs_add_abs [simp]: "\<bar>\<bar>a\<bar> + \<bar>b\<bar>\<bar> = \<bar>a\<bar> + \<bar>b\<bar>" 1302 (is "?L = ?R") 1303proof (rule antisym) 1304 show "?L \<ge> ?R" by (rule abs_ge_self) 1305 have "?L \<le> \<bar>\<bar>a\<bar>\<bar> + \<bar>\<bar>b\<bar>\<bar>" by (rule abs_triangle_ineq) 1306 also have "\<dots> = ?R" by simp 1307 finally show "?L \<le> ?R" . 1308qed 1309 1310end 1311 1312lemma dense_eq0_I: 1313 fixes x::"'a::{dense_linorder,ordered_ab_group_add_abs}" 1314 shows "(\<And>e. 0 < e \<Longrightarrow> \<bar>x\<bar> \<le> e) \<Longrightarrow> x = 0" 1315 apply (cases "\<bar>x\<bar> = 0") 1316 apply simp 1317 apply (simp only: zero_less_abs_iff [symmetric]) 1318 apply (drule dense) 1319 apply (auto simp add: not_less [symmetric]) 1320 done 1321 1322hide_fact (open) ab_diff_conv_add_uminus add_0 mult_1 ab_left_minus 1323 1324lemmas add_0 = add_0_left (* FIXME duplicate *) 1325lemmas mult_1 = mult_1_left (* FIXME duplicate *) 1326lemmas ab_left_minus = left_minus (* FIXME duplicate *) 1327lemmas diff_diff_eq = diff_diff_add (* FIXME duplicate *) 1328 1329 1330subsection \<open>Canonically ordered monoids\<close> 1331 1332text \<open>Canonically ordered monoids are never groups.\<close> 1333 1334class canonically_ordered_monoid_add = comm_monoid_add + order + 1335 assumes le_iff_add: "a \<le> b \<longleftrightarrow> (\<exists>c. b = a + c)" 1336begin 1337 1338lemma zero_le[simp]: "0 \<le> x" 1339 by (auto simp: le_iff_add) 1340 1341lemma le_zero_eq[simp]: "n \<le> 0 \<longleftrightarrow> n = 0" 1342 by (auto intro: antisym) 1343 1344lemma not_less_zero[simp]: "\<not> n < 0" 1345 by (auto simp: less_le) 1346 1347lemma zero_less_iff_neq_zero: "0 < n \<longleftrightarrow> n \<noteq> 0" 1348 by (auto simp: less_le) 1349 1350text \<open>This theorem is useful with \<open>blast\<close>\<close> 1351lemma gr_zeroI: "(n = 0 \<Longrightarrow> False) \<Longrightarrow> 0 < n" 1352 by (rule zero_less_iff_neq_zero[THEN iffD2]) iprover 1353 1354lemma not_gr_zero[simp]: "\<not> 0 < n \<longleftrightarrow> n = 0" 1355 by (simp add: zero_less_iff_neq_zero) 1356 1357subclass ordered_comm_monoid_add 1358 proof qed (auto simp: le_iff_add add_ac) 1359 1360lemma gr_implies_not_zero: "m < n \<Longrightarrow> n \<noteq> 0" 1361 by auto 1362 1363lemma add_eq_0_iff_both_eq_0[simp]: "x + y = 0 \<longleftrightarrow> x = 0 \<and> y = 0" 1364 by (intro add_nonneg_eq_0_iff zero_le) 1365 1366lemma zero_eq_add_iff_both_eq_0[simp]: "0 = x + y \<longleftrightarrow> x = 0 \<and> y = 0" 1367 using add_eq_0_iff_both_eq_0[of x y] unfolding eq_commute[of 0] . 1368 1369lemmas zero_order = zero_le le_zero_eq not_less_zero zero_less_iff_neq_zero not_gr_zero 1370 \<comment> \<open>This should be attributed with \<open>[iff]\<close>, but then \<open>blast\<close> fails in \<open>Set\<close>.\<close> 1371 1372end 1373 1374class ordered_cancel_comm_monoid_diff = 1375 canonically_ordered_monoid_add + comm_monoid_diff + ordered_ab_semigroup_add_imp_le 1376begin 1377 1378context 1379 fixes a b :: 'a 1380 assumes le: "a \<le> b" 1381begin 1382 1383lemma add_diff_inverse: "a + (b - a) = b" 1384 using le by (auto simp add: le_iff_add) 1385 1386lemma add_diff_assoc: "c + (b - a) = c + b - a" 1387 using le by (auto simp add: le_iff_add add.left_commute [of c]) 1388 1389lemma add_diff_assoc2: "b - a + c = b + c - a" 1390 using le by (auto simp add: le_iff_add add.assoc) 1391 1392lemma diff_add_assoc: "c + b - a = c + (b - a)" 1393 using le by (simp add: add.commute add_diff_assoc) 1394 1395lemma diff_add_assoc2: "b + c - a = b - a + c" 1396 using le by (simp add: add.commute add_diff_assoc) 1397 1398lemma diff_diff_right: "c - (b - a) = c + a - b" 1399 by (simp add: add_diff_inverse add_diff_cancel_left [of a c "b - a", symmetric] add.commute) 1400 1401lemma diff_add: "b - a + a = b" 1402 by (simp add: add.commute add_diff_inverse) 1403 1404lemma le_add_diff: "c \<le> b + c - a" 1405 by (auto simp add: add.commute diff_add_assoc2 le_iff_add) 1406 1407lemma le_imp_diff_is_add: "a \<le> b \<Longrightarrow> b - a = c \<longleftrightarrow> b = c + a" 1408 by (auto simp add: add.commute add_diff_inverse) 1409 1410lemma le_diff_conv2: "c \<le> b - a \<longleftrightarrow> c + a \<le> b" 1411 (is "?P \<longleftrightarrow> ?Q") 1412proof 1413 assume ?P 1414 then have "c + a \<le> b - a + a" 1415 by (rule add_right_mono) 1416 then show ?Q 1417 by (simp add: add_diff_inverse add.commute) 1418next 1419 assume ?Q 1420 then have "a + c \<le> a + (b - a)" 1421 by (simp add: add_diff_inverse add.commute) 1422 then show ?P by simp 1423qed 1424 1425end 1426 1427end 1428 1429 1430subsection \<open>Tools setup\<close> 1431 1432lemma add_mono_thms_linordered_semiring: 1433 fixes i j k :: "'a::ordered_ab_semigroup_add" 1434 shows "i \<le> j \<and> k \<le> l \<Longrightarrow> i + k \<le> j + l" 1435 and "i = j \<and> k \<le> l \<Longrightarrow> i + k \<le> j + l" 1436 and "i \<le> j \<and> k = l \<Longrightarrow> i + k \<le> j + l" 1437 and "i = j \<and> k = l \<Longrightarrow> i + k = j + l" 1438 by (rule add_mono, clarify+)+ 1439 1440lemma add_mono_thms_linordered_field: 1441 fixes i j k :: "'a::ordered_cancel_ab_semigroup_add" 1442 shows "i < j \<and> k = l \<Longrightarrow> i + k < j + l" 1443 and "i = j \<and> k < l \<Longrightarrow> i + k < j + l" 1444 and "i < j \<and> k \<le> l \<Longrightarrow> i + k < j + l" 1445 and "i \<le> j \<and> k < l \<Longrightarrow> i + k < j + l" 1446 and "i < j \<and> k < l \<Longrightarrow> i + k < j + l" 1447 by (auto intro: add_strict_right_mono add_strict_left_mono 1448 add_less_le_mono add_le_less_mono add_strict_mono) 1449 1450code_identifier 1451 code_module Groups \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith 1452 1453end 1454