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