src/HOL/Groups.thy
 author wenzelm Fri Aug 12 17:53:55 2016 +0200 (2016-08-12) changeset 63680 6e1e8b5abbfa parent 63588 d0e2bad67bd4 child 63878 e26c7f58d78e permissions -rw-r--r--
more symbols;
```     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
```
```     9 section \<open>Groups, also combined with orderings\<close>
```
```    10
```
```    11 theory Groups
```
```    12   imports Orderings
```
```    13 begin
```
```    14
```
```    15 subsection \<open>Dynamic facts\<close>
```
```    16
```
```    17 named_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
```
```    21 text \<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
```
```    38 subsection \<open>Abstract structures\<close>
```
```    39
```
```    40 text \<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
```
```    46 locale 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
```
```    50 locale abel_semigroup = semigroup +
```
```    51   assumes commute [ac_simps]: "a \<^bold>* b = b \<^bold>* a"
```
```    52 begin
```
```    53
```
```    54 lemma left_commute [ac_simps]: "b \<^bold>* (a \<^bold>* c) = a \<^bold>* (b \<^bold>* c)"
```
```    55 proof -
```
```    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)
```
```    60 qed
```
```    61
```
```    62 end
```
```    63
```
```    64 locale 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
```
```    69 locale comm_monoid = abel_semigroup +
```
```    70   fixes z :: 'a ("\<^bold>1")
```
```    71   assumes comm_neutral: "a \<^bold>* \<^bold>1 = a"
```
```    72 begin
```
```    73
```
```    74 sublocale monoid
```
```    75   by standard (simp_all add: commute comm_neutral)
```
```    76
```
```    77 end
```
```    78
```
```    79 locale 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"
```
```    84 begin
```
```    85
```
```    86 lemma left_cancel: "a \<^bold>* b = a \<^bold>* c \<longleftrightarrow> b = c"
```
```    87 proof
```
```    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)
```
```    93 qed simp
```
```    94
```
```    95 sublocale monoid
```
```    96 proof
```
```    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)
```
```   103 qed (fact group_left_neutral)
```
```   104
```
```   105 lemma inverse_unique:
```
```   106   assumes "a \<^bold>* b = \<^bold>1"
```
```   107   shows "inverse a = b"
```
```   108 proof -
```
```   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])
```
```   113 qed
```
```   114
```
```   115 lemma inverse_neutral [simp]: "inverse \<^bold>1 = \<^bold>1"
```
```   116   by (rule inverse_unique) simp
```
```   117
```
```   118 lemma inverse_inverse [simp]: "inverse (inverse a) = a"
```
```   119   by (rule inverse_unique) simp
```
```   120
```
```   121 lemma right_inverse [simp]: "a \<^bold>* inverse a = \<^bold>1"
```
```   122 proof -
```
```   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
```
```   128 qed
```
```   129
```
```   130 lemma inverse_distrib_swap: "inverse (a \<^bold>* b) = inverse b \<^bold>* inverse a"
```
```   131 proof (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" .
```
```   138 qed
```
```   139
```
```   140 lemma right_cancel: "b \<^bold>* a = c \<^bold>* a \<longleftrightarrow> b = c"
```
```   141 proof
```
```   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)
```
```   147 qed simp
```
```   148
```
```   149 end
```
```   150
```
```   151
```
```   152 subsection \<open>Generic operations\<close>
```
```   153
```
```   154 class zero =
```
```   155   fixes zero :: 'a  ("0")
```
```   156
```
```   157 class one =
```
```   158   fixes one  :: 'a  ("1")
```
```   159
```
```   160 hide_const (open) zero one
```
```   161
```
```   162 lemma Let_0 [simp]: "Let 0 f = f 0"
```
```   163   unfolding Let_def ..
```
```   164
```
```   165 lemma Let_1 [simp]: "Let 1 f = f 1"
```
```   166   unfolding Let_def ..
```
```   167
```
```   168 setup \<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
```
```   175 simproc_setup reorient_zero ("0 = x") = Reorient_Proc.proc
```
```   176 simproc_setup reorient_one ("1 = x") = Reorient_Proc.proc
```
```   177
```
```   178 typed_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
```
```   188 class plus =
```
```   189   fixes plus :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "+" 65)
```
```   190
```
```   191 class minus =
```
```   192   fixes minus :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "-" 65)
```
```   193
```
```   194 class uminus =
```
```   195   fixes uminus :: "'a \<Rightarrow> 'a"  ("- _" [81] 80)
```
```   196
```
```   197 class times =
```
```   198   fixes times :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "*" 70)
```
```   199
```
```   200
```
```   201 subsection \<open>Semigroups and Monoids\<close>
```
```   202
```
```   203 class semigroup_add = plus +
```
```   204   assumes add_assoc [algebra_simps, field_simps]: "(a + b) + c = a + (b + c)"
```
```   205 begin
```
```   206
```
```   207 sublocale add: semigroup plus
```
```   208   by standard (fact add_assoc)
```
```   209
```
```   210 end
```
```   211
```
```   212 hide_fact add_assoc
```
```   213
```
```   214 class ab_semigroup_add = semigroup_add +
```
```   215   assumes add_commute [algebra_simps, field_simps]: "a + b = b + a"
```
```   216 begin
```
```   217
```
```   218 sublocale add: abel_semigroup plus
```
```   219   by standard (fact add_commute)
```
```   220
```
```   221 declare add.left_commute [algebra_simps, field_simps]
```
```   222
```
```   223 lemmas add_ac = add.assoc add.commute add.left_commute
```
```   224
```
```   225 end
```
```   226
```
```   227 hide_fact add_commute
```
```   228
```
```   229 lemmas add_ac = add.assoc add.commute add.left_commute
```
```   230
```
```   231 class semigroup_mult = times +
```
```   232   assumes mult_assoc [algebra_simps, field_simps]: "(a * b) * c = a * (b * c)"
```
```   233 begin
```
```   234
```
```   235 sublocale mult: semigroup times
```
```   236   by standard (fact mult_assoc)
```
```   237
```
```   238 end
```
```   239
```
```   240 hide_fact mult_assoc
```
```   241
```
```   242 class ab_semigroup_mult = semigroup_mult +
```
```   243   assumes mult_commute [algebra_simps, field_simps]: "a * b = b * a"
```
```   244 begin
```
```   245
```
```   246 sublocale mult: abel_semigroup times
```
```   247   by standard (fact mult_commute)
```
```   248
```
```   249 declare mult.left_commute [algebra_simps, field_simps]
```
```   250
```
```   251 lemmas mult_ac = mult.assoc mult.commute mult.left_commute
```
```   252
```
```   253 end
```
```   254
```
```   255 hide_fact mult_commute
```
```   256
```
```   257 lemmas mult_ac = mult.assoc mult.commute mult.left_commute
```
```   258
```
```   259 class monoid_add = zero + semigroup_add +
```
```   260   assumes add_0_left: "0 + a = a"
```
```   261     and add_0_right: "a + 0 = a"
```
```   262 begin
```
```   263
```
```   264 sublocale add: monoid plus 0
```
```   265   by standard (fact add_0_left add_0_right)+
```
```   266
```
```   267 end
```
```   268
```
```   269 lemma zero_reorient: "0 = x \<longleftrightarrow> x = 0"
```
```   270   by (fact eq_commute)
```
```   271
```
```   272 class comm_monoid_add = zero + ab_semigroup_add +
```
```   273   assumes add_0: "0 + a = a"
```
```   274 begin
```
```   275
```
```   276 subclass monoid_add
```
```   277   by standard (simp_all add: add_0 add.commute [of _ 0])
```
```   278
```
```   279 sublocale add: comm_monoid plus 0
```
```   280   by standard (simp add: ac_simps)
```
```   281
```
```   282 end
```
```   283
```
```   284 class monoid_mult = one + semigroup_mult +
```
```   285   assumes mult_1_left: "1 * a  = a"
```
```   286     and mult_1_right: "a * 1 = a"
```
```   287 begin
```
```   288
```
```   289 sublocale mult: monoid times 1
```
```   290   by standard (fact mult_1_left mult_1_right)+
```
```   291
```
```   292 end
```
```   293
```
```   294 lemma one_reorient: "1 = x \<longleftrightarrow> x = 1"
```
```   295   by (fact eq_commute)
```
```   296
```
```   297 class comm_monoid_mult = one + ab_semigroup_mult +
```
```   298   assumes mult_1: "1 * a = a"
```
```   299 begin
```
```   300
```
```   301 subclass monoid_mult
```
```   302   by standard (simp_all add: mult_1 mult.commute [of _ 1])
```
```   303
```
```   304 sublocale mult: comm_monoid times 1
```
```   305   by standard (simp add: ac_simps)
```
```   306
```
```   307 end
```
```   308
```
```   309 class 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"
```
```   312 begin
```
```   313
```
```   314 lemma add_left_cancel [simp]: "a + b = a + c \<longleftrightarrow> b = c"
```
```   315   by (blast dest: add_left_imp_eq)
```
```   316
```
```   317 lemma add_right_cancel [simp]: "b + a = c + a \<longleftrightarrow> b = c"
```
```   318   by (blast dest: add_right_imp_eq)
```
```   319
```
```   320 end
```
```   321
```
```   322 class 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)"
```
```   325 begin
```
```   326
```
```   327 lemma add_diff_cancel_right' [simp]: "(a + b) - b = a"
```
```   328   using add_diff_cancel_left' [of b a] by (simp add: ac_simps)
```
```   329
```
```   330 subclass cancel_semigroup_add
```
```   331 proof
```
```   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
```
```   338 next
```
```   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
```
```   345 qed
```
```   346
```
```   347 lemma add_diff_cancel_left [simp]: "(c + a) - (c + b) = a - b"
```
```   348   unfolding diff_diff_add [symmetric] by simp
```
```   349
```
```   350 lemma add_diff_cancel_right [simp]: "(a + c) - (b + c) = a - b"
```
```   351   using add_diff_cancel_left [symmetric] by (simp add: ac_simps)
```
```   352
```
```   353 lemma diff_right_commute: "a - c - b = a - b - c"
```
```   354   by (simp add: diff_diff_add add.commute)
```
```   355
```
```   356 end
```
```   357
```
```   358 class cancel_comm_monoid_add = cancel_ab_semigroup_add + comm_monoid_add
```
```   359 begin
```
```   360
```
```   361 lemma diff_zero [simp]: "a - 0 = a"
```
```   362   using add_diff_cancel_right' [of a 0] by simp
```
```   363
```
```   364 lemma diff_cancel [simp]: "a - a = 0"
```
```   365 proof -
```
```   366   have "(a + 0) - (a + 0) = 0"
```
```   367     by (simp only: add_diff_cancel_left diff_zero)
```
```   368   then show ?thesis by simp
```
```   369 qed
```
```   370
```
```   371 lemma add_implies_diff:
```
```   372   assumes "c + b = a"
```
```   373   shows "c = a - b"
```
```   374 proof -
```
```   375   from assms have "(b + c) - (b + 0) = a - b"
```
```   376     by (simp add: add.commute)
```
```   377   then show "c = a - b" by simp
```
```   378 qed
```
```   379
```
```   380 lemma add_cancel_right_right [simp]: "a = a + b \<longleftrightarrow> b = 0"
```
```   381   (is "?P \<longleftrightarrow> ?Q")
```
```   382 proof
```
```   383   assume ?Q
```
```   384   then show ?P by simp
```
```   385 next
```
```   386   assume ?P
```
```   387   then have "a - a = a + b - a" by simp
```
```   388   then show ?Q by simp
```
```   389 qed
```
```   390
```
```   391 lemma 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
```
```   394 lemma add_cancel_left_right [simp]: "a + b = a \<longleftrightarrow> b = 0"
```
```   395   by (auto dest: sym)
```
```   396
```
```   397 lemma add_cancel_left_left [simp]: "b + a = a \<longleftrightarrow> b = 0"
```
```   398   by (auto dest: sym)
```
```   399
```
```   400 end
```
```   401
```
```   402 class comm_monoid_diff = cancel_comm_monoid_add +
```
```   403   assumes zero_diff [simp]: "0 - a = 0"
```
```   404 begin
```
```   405
```
```   406 lemma diff_add_zero [simp]: "a - (a + b) = 0"
```
```   407 proof -
```
```   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 .
```
```   413 qed
```
```   414
```
```   415 end
```
```   416
```
```   417
```
```   418 subsection \<open>Groups\<close>
```
```   419
```
```   420 class group_add = minus + uminus + monoid_add +
```
```   421   assumes left_minus: "- a + a = 0"
```
```   422   assumes add_uminus_conv_diff [simp]: "a + (- b) = a - b"
```
```   423 begin
```
```   424
```
```   425 lemma diff_conv_add_uminus: "a - b = a + (- b)"
```
```   426   by simp
```
```   427
```
```   428 sublocale add: group plus 0 uminus
```
```   429   by standard (simp_all add: left_minus)
```
```   430
```
```   431 lemma minus_unique: "a + b = 0 \<Longrightarrow> - a = b"
```
```   432   by (fact add.inverse_unique)
```
```   433
```
```   434 lemma minus_zero: "- 0 = 0"
```
```   435   by (fact add.inverse_neutral)
```
```   436
```
```   437 lemma minus_minus: "- (- a) = a"
```
```   438   by (fact add.inverse_inverse)
```
```   439
```
```   440 lemma right_minus: "a + - a = 0"
```
```   441   by (fact add.right_inverse)
```
```   442
```
```   443 lemma diff_self [simp]: "a - a = 0"
```
```   444   using right_minus [of a] by simp
```
```   445
```
```   446 subclass cancel_semigroup_add
```
```   447   by standard (simp_all add: add.left_cancel add.right_cancel)
```
```   448
```
```   449 lemma minus_add_cancel [simp]: "- a + (a + b) = b"
```
```   450   by (simp add: add.assoc [symmetric])
```
```   451
```
```   452 lemma add_minus_cancel [simp]: "a + (- a + b) = b"
```
```   453   by (simp add: add.assoc [symmetric])
```
```   454
```
```   455 lemma diff_add_cancel [simp]: "a - b + b = a"
```
```   456   by (simp only: diff_conv_add_uminus add.assoc) simp
```
```   457
```
```   458 lemma add_diff_cancel [simp]: "a + b - b = a"
```
```   459   by (simp only: diff_conv_add_uminus add.assoc) simp
```
```   460
```
```   461 lemma minus_add: "- (a + b) = - b + - a"
```
```   462   by (fact add.inverse_distrib_swap)
```
```   463
```
```   464 lemma right_minus_eq [simp]: "a - b = 0 \<longleftrightarrow> a = b"
```
```   465 proof
```
```   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" .
```
```   470 next
```
```   471   assume "a = b"
```
```   472   then show "a - b = 0" by simp
```
```   473 qed
```
```   474
```
```   475 lemma eq_iff_diff_eq_0: "a = b \<longleftrightarrow> a - b = 0"
```
```   476   by (fact right_minus_eq [symmetric])
```
```   477
```
```   478 lemma diff_0 [simp]: "0 - a = - a"
```
```   479   by (simp only: diff_conv_add_uminus add_0_left)
```
```   480
```
```   481 lemma diff_0_right [simp]: "a - 0 = a"
```
```   482   by (simp only: diff_conv_add_uminus minus_zero add_0_right)
```
```   483
```
```   484 lemma diff_minus_eq_add [simp]: "a - - b = a + b"
```
```   485   by (simp only: diff_conv_add_uminus minus_minus)
```
```   486
```
```   487 lemma neg_equal_iff_equal [simp]: "- a = - b \<longleftrightarrow> a = b"
```
```   488 proof
```
```   489   assume "- a = - b"
```
```   490   then have "- (- a) = - (- b)" by simp
```
```   491   then show "a = b" by simp
```
```   492 next
```
```   493   assume "a = b"
```
```   494   then show "- a = - b" by simp
```
```   495 qed
```
```   496
```
```   497 lemma neg_equal_0_iff_equal [simp]: "- a = 0 \<longleftrightarrow> a = 0"
```
```   498   by (subst neg_equal_iff_equal [symmetric]) simp
```
```   499
```
```   500 lemma neg_0_equal_iff_equal [simp]: "0 = - a \<longleftrightarrow> 0 = a"
```
```   501   by (subst neg_equal_iff_equal [symmetric]) simp
```
```   502
```
```   503 text \<open>The next two equations can make the simplifier loop!\<close>
```
```   504
```
```   505 lemma equation_minus_iff: "a = - b \<longleftrightarrow> b = - a"
```
```   506 proof -
```
```   507   have "- (- a) = - b \<longleftrightarrow> - a = b"
```
```   508     by (rule neg_equal_iff_equal)
```
```   509   then show ?thesis
```
```   510     by (simp add: eq_commute)
```
```   511 qed
```
```   512
```
```   513 lemma minus_equation_iff: "- a = b \<longleftrightarrow> - b = a"
```
```   514 proof -
```
```   515   have "- a = - (- b) \<longleftrightarrow> a = -b"
```
```   516     by (rule neg_equal_iff_equal)
```
```   517   then show ?thesis
```
```   518     by (simp add: eq_commute)
```
```   519 qed
```
```   520
```
```   521 lemma eq_neg_iff_add_eq_0: "a = - b \<longleftrightarrow> a + b = 0"
```
```   522 proof
```
```   523   assume "a = - b"
```
```   524   then show "a + b = 0" by simp
```
```   525 next
```
```   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
```
```   531 qed
```
```   532
```
```   533 lemma add_eq_0_iff2: "a + b = 0 \<longleftrightarrow> a = - b"
```
```   534   by (fact eq_neg_iff_add_eq_0 [symmetric])
```
```   535
```
```   536 lemma neg_eq_iff_add_eq_0: "- a = b \<longleftrightarrow> a + b = 0"
```
```   537   by (auto simp add: add_eq_0_iff2)
```
```   538
```
```   539 lemma add_eq_0_iff: "a + b = 0 \<longleftrightarrow> b = - a"
```
```   540   by (auto simp add: neg_eq_iff_add_eq_0 [symmetric])
```
```   541
```
```   542 lemma 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
```
```   545 lemma add_diff_eq [algebra_simps, field_simps]: "a + (b - c) = (a + b) - c"
```
```   546   by (simp only: diff_conv_add_uminus add.assoc)
```
```   547
```
```   548 lemma 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
```
```   551 lemma diff_eq_eq [algebra_simps, field_simps]: "a - b = c \<longleftrightarrow> a = c + b"
```
```   552   by auto
```
```   553
```
```   554 lemma eq_diff_eq [algebra_simps, field_simps]: "a = c - b \<longleftrightarrow> a + b = c"
```
```   555   by auto
```
```   556
```
```   557 lemma 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
```
```   560 lemma 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
```
```   563 end
```
```   564
```
```   565 class 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)"
```
```   568 begin
```
```   569
```
```   570 subclass group_add
```
```   571   by standard (simp_all add: ab_left_minus ab_diff_conv_add_uminus)
```
```   572
```
```   573 subclass cancel_comm_monoid_add
```
```   574 proof
```
```   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)
```
```   582 qed
```
```   583
```
```   584 lemma uminus_add_conv_diff [simp]: "- a + b = b - a"
```
```   585   by (simp add: add.commute)
```
```   586
```
```   587 lemma minus_add_distrib [simp]: "- (a + b) = - a + - b"
```
```   588   by (simp add: algebra_simps)
```
```   589
```
```   590 lemma diff_add_eq [algebra_simps, field_simps]: "(a - b) + c = (a + c) - b"
```
```   591   by (simp add: algebra_simps)
```
```   592
```
```   593 end
```
```   594
```
```   595
```
```   596 subsection \<open>(Partially) Ordered Groups\<close>
```
```   597
```
```   598 text \<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
```
```   609 class ordered_ab_semigroup_add = order + ab_semigroup_add +
```
```   610   assumes add_left_mono: "a \<le> b \<Longrightarrow> c + a \<le> c + b"
```
```   611 begin
```
```   612
```
```   613 lemma add_right_mono: "a \<le> b \<Longrightarrow> a + c \<le> b + c"
```
```   614   by (simp add: add.commute [of _ c] add_left_mono)
```
```   615
```
```   616 text \<open>non-strict, in both arguments\<close>
```
```   617 lemma 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
```
```   622 end
```
```   623
```
```   624 text \<open>Strict monotonicity in both arguments\<close>
```
```   625 class 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
```
```   628 class ordered_cancel_ab_semigroup_add =
```
```   629   ordered_ab_semigroup_add + cancel_ab_semigroup_add
```
```   630 begin
```
```   631
```
```   632 lemma add_strict_left_mono: "a < b \<Longrightarrow> c + a < c + b"
```
```   633   by (auto simp add: less_le add_left_mono)
```
```   634
```
```   635 lemma add_strict_right_mono: "a < b \<Longrightarrow> a + c < b + c"
```
```   636   by (simp add: add.commute [of _ c] add_strict_left_mono)
```
```   637
```
```   638 subclass 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
```
```   644 lemma 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
```
```   649 lemma 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
```
```   654 end
```
```   655
```
```   656 class 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"
```
```   658 begin
```
```   659
```
```   660 lemma add_less_imp_less_left:
```
```   661   assumes less: "c + a < c + b"
```
```   662   shows "a < b"
```
```   663 proof -
```
```   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)
```
```   682 qed
```
```   683
```
```   684 lemma 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
```
```   687 lemma 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
```
```   690 lemma 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
```
```   693 lemma 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
```
```   699 lemma 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
```
```   702 lemma add_le_imp_le_right: "a + c \<le> b + c \<Longrightarrow> a \<le> b"
```
```   703   by simp
```
```   704
```
```   705 lemma max_add_distrib_left: "max x y + z = max (x + z) (y + z)"
```
```   706   unfolding max_def by auto
```
```   707
```
```   708 lemma min_add_distrib_left: "min x y + z = min (x + z) (y + z)"
```
```   709   unfolding min_def by auto
```
```   710
```
```   711 lemma max_add_distrib_right: "x + max y z = max (x + y) (x + z)"
```
```   712   unfolding max_def by auto
```
```   713
```
```   714 lemma min_add_distrib_right: "x + min y z = min (x + y) (x + z)"
```
```   715   unfolding min_def by auto
```
```   716
```
```   717 end
```
```   718
```
```   719 subsection \<open>Support for reasoning about signs\<close>
```
```   720
```
```   721 class ordered_comm_monoid_add = comm_monoid_add + ordered_ab_semigroup_add
```
```   722 begin
```
```   723
```
```   724 lemma 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
```
```   727 lemma 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
```
```   730 lemma 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
```
```   733 lemma 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
```
```   736 lemma 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
```
```   739 lemma 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
```
```   742 lemma 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
```
```   745 lemma 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
```
```   748 lemma 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
```
```   751 lemma add_pos_pos: "0 < a \<Longrightarrow> 0 < b \<Longrightarrow> 0 < a + b"
```
```   752   by (intro add_pos_nonneg less_imp_le)
```
```   753
```
```   754 lemma 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
```
```   757 lemma 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
```
```   760 lemma add_neg_neg: "a < 0 \<Longrightarrow> b < 0 \<Longrightarrow> a + b < 0"
```
```   761   by (intro add_neg_nonpos less_imp_le)
```
```   762
```
```   763 lemma 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
```
```   766 lemmas 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
```
```   770 end
```
```   771
```
```   772 class strict_ordered_comm_monoid_add = comm_monoid_add + strict_ordered_ab_semigroup_add
```
```   773 begin
```
```   774
```
```   775 lemma 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
```
```   778 end
```
```   779
```
```   780 class ordered_cancel_comm_monoid_add = ordered_comm_monoid_add + cancel_ab_semigroup_add
```
```   781 begin
```
```   782
```
```   783 subclass ordered_cancel_ab_semigroup_add ..
```
```   784 subclass strict_ordered_comm_monoid_add ..
```
```   785
```
```   786 lemma 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
```
```   789 lemma 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
```
```   792 end
```
```   793
```
```   794 class ordered_ab_semigroup_monoid_add_imp_le = monoid_add + ordered_ab_semigroup_add_imp_le
```
```   795 begin
```
```   796
```
```   797 lemma add_less_same_cancel1 [simp]: "b + a < b \<longleftrightarrow> a < 0"
```
```   798   using add_less_cancel_left [of _ _ 0] by simp
```
```   799
```
```   800 lemma add_less_same_cancel2 [simp]: "a + b < b \<longleftrightarrow> a < 0"
```
```   801   using add_less_cancel_right [of _ _ 0] by simp
```
```   802
```
```   803 lemma less_add_same_cancel1 [simp]: "a < a + b \<longleftrightarrow> 0 < b"
```
```   804   using add_less_cancel_left [of _ 0] by simp
```
```   805
```
```   806 lemma less_add_same_cancel2 [simp]: "a < b + a \<longleftrightarrow> 0 < b"
```
```   807   using add_less_cancel_right [of 0] by simp
```
```   808
```
```   809 lemma add_le_same_cancel1 [simp]: "b + a \<le> b \<longleftrightarrow> a \<le> 0"
```
```   810   using add_le_cancel_left [of _ _ 0] by simp
```
```   811
```
```   812 lemma add_le_same_cancel2 [simp]: "a + b \<le> b \<longleftrightarrow> a \<le> 0"
```
```   813   using add_le_cancel_right [of _ _ 0] by simp
```
```   814
```
```   815 lemma le_add_same_cancel1 [simp]: "a \<le> a + b \<longleftrightarrow> 0 \<le> b"
```
```   816   using add_le_cancel_left [of _ 0] by simp
```
```   817
```
```   818 lemma le_add_same_cancel2 [simp]: "a \<le> b + a \<longleftrightarrow> 0 \<le> b"
```
```   819   using add_le_cancel_right [of 0] by simp
```
```   820
```
```   821 subclass cancel_comm_monoid_add
```
```   822   by standard auto
```
```   823
```
```   824 subclass ordered_cancel_comm_monoid_add
```
```   825   by standard
```
```   826
```
```   827 end
```
```   828
```
```   829 class ordered_ab_group_add = ab_group_add + ordered_ab_semigroup_add
```
```   830 begin
```
```   831
```
```   832 subclass ordered_cancel_ab_semigroup_add ..
```
```   833
```
```   834 subclass ordered_ab_semigroup_monoid_add_imp_le
```
```   835 proof
```
```   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
```
```   843 qed
```
```   844
```
```   845 lemma 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
```
```   848 lemma 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
```
```   851 lemma le_imp_neg_le:
```
```   852   assumes "a \<le> b"
```
```   853   shows "- b \<le> - a"
```
```   854 proof -
```
```   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)
```
```   863 qed
```
```   864
```
```   865 lemma neg_le_iff_le [simp]: "- b \<le> - a \<longleftrightarrow> a \<le> b"
```
```   866 proof
```
```   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
```
```   872 next
```
```   873   assume "a \<le> b"
```
```   874   then show "- b \<le> - a"
```
```   875     by (rule le_imp_neg_le)
```
```   876 qed
```
```   877
```
```   878 lemma neg_le_0_iff_le [simp]: "- a \<le> 0 \<longleftrightarrow> 0 \<le> a"
```
```   879   by (subst neg_le_iff_le [symmetric]) simp
```
```   880
```
```   881 lemma neg_0_le_iff_le [simp]: "0 \<le> - a \<longleftrightarrow> a \<le> 0"
```
```   882   by (subst neg_le_iff_le [symmetric]) simp
```
```   883
```
```   884 lemma neg_less_iff_less [simp]: "- b < - a \<longleftrightarrow> a < b"
```
```   885   by (auto simp add: less_le)
```
```   886
```
```   887 lemma neg_less_0_iff_less [simp]: "- a < 0 \<longleftrightarrow> 0 < a"
```
```   888   by (subst neg_less_iff_less [symmetric]) simp
```
```   889
```
```   890 lemma neg_0_less_iff_less [simp]: "0 < - a \<longleftrightarrow> a < 0"
```
```   891   by (subst neg_less_iff_less [symmetric]) simp
```
```   892
```
```   893 text \<open>The next several equations can make the simplifier loop!\<close>
```
```   894
```
```   895 lemma less_minus_iff: "a < - b \<longleftrightarrow> b < - a"
```
```   896 proof -
```
```   897   have "- (- a) < - b \<longleftrightarrow> b < - a"
```
```   898     by (rule neg_less_iff_less)
```
```   899   then show ?thesis by simp
```
```   900 qed
```
```   901
```
```   902 lemma minus_less_iff: "- a < b \<longleftrightarrow> - b < a"
```
```   903 proof -
```
```   904   have "- a < - (- b) \<longleftrightarrow> - b < a"
```
```   905     by (rule neg_less_iff_less)
```
```   906   then show ?thesis by simp
```
```   907 qed
```
```   908
```
```   909 lemma le_minus_iff: "a \<le> - b \<longleftrightarrow> b \<le> - a"
```
```   910 proof -
```
```   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
```
```   920 qed
```
```   921
```
```   922 lemma minus_le_iff: "- a \<le> b \<longleftrightarrow> - b \<le> a"
```
```   923   by (auto simp add: le_less minus_less_iff)
```
```   924
```
```   925 lemma diff_less_0_iff_less [simp]: "a - b < 0 \<longleftrightarrow> a < b"
```
```   926 proof -
```
```   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 .
```
```   932 qed
```
```   933
```
```   934 lemmas less_iff_diff_less_0 = diff_less_0_iff_less [symmetric]
```
```   935
```
```   936 lemma 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
```
```   942 lemma 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
```
```   948 lemma diff_gt_0_iff_gt [simp]: "a - b > 0 \<longleftrightarrow> a > b"
```
```   949   by (simp add: less_diff_eq)
```
```   950
```
```   951 lemma 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
```
```   954 lemma 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
```
```   957 lemma diff_le_0_iff_le [simp]: "a - b \<le> 0 \<longleftrightarrow> a \<le> b"
```
```   958   by (simp add: algebra_simps)
```
```   959
```
```   960 lemmas le_iff_diff_le_0 = diff_le_0_iff_le [symmetric]
```
```   961
```
```   962 lemma diff_ge_0_iff_ge [simp]: "a - b \<ge> 0 \<longleftrightarrow> a \<ge> b"
```
```   963   by (simp add: le_diff_eq)
```
```   964
```
```   965 lemma 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
```
```   968 lemma 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
```
```   971 lemma diff_mono: "a \<le> b \<Longrightarrow> d \<le> c \<Longrightarrow> a - c \<le> b - d"
```
```   972   by (simp add: field_simps add_mono)
```
```   973
```
```   974 lemma diff_left_mono: "b \<le> a \<Longrightarrow> c - a \<le> c - b"
```
```   975   by (simp add: field_simps)
```
```   976
```
```   977 lemma diff_right_mono: "a \<le> b \<Longrightarrow> a - c \<le> b - c"
```
```   978   by (simp add: field_simps)
```
```   979
```
```   980 lemma diff_strict_mono: "a < b \<Longrightarrow> d < c \<Longrightarrow> a - c < b - d"
```
```   981   by (simp add: field_simps add_strict_mono)
```
```   982
```
```   983 lemma diff_strict_left_mono: "b < a \<Longrightarrow> c - a < c - b"
```
```   984   by (simp add: field_simps)
```
```   985
```
```   986 lemma diff_strict_right_mono: "a < b \<Longrightarrow> a - c < b - c"
```
```   987   by (simp add: field_simps)
```
```   988
```
```   989 end
```
```   990
```
```   991 ML_file "Tools/group_cancel.ML"
```
```   992
```
```   993 simproc_setup group_cancel_add ("a + b::'a::ab_group_add") =
```
```   994   \<open>fn phi => fn ss => try Group_Cancel.cancel_add_conv\<close>
```
```   995
```
```   996 simproc_setup group_cancel_diff ("a - b::'a::ab_group_add") =
```
```   997   \<open>fn phi => fn ss => try Group_Cancel.cancel_diff_conv\<close>
```
```   998
```
```   999 simproc_setup group_cancel_eq ("a = (b::'a::ab_group_add)") =
```
```  1000   \<open>fn phi => fn ss => try Group_Cancel.cancel_eq_conv\<close>
```
```  1001
```
```  1002 simproc_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
```
```  1005 simproc_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
```
```  1008 class linordered_ab_semigroup_add =
```
```  1009   linorder + ordered_ab_semigroup_add
```
```  1010
```
```  1011 class linordered_cancel_ab_semigroup_add =
```
```  1012   linorder + ordered_cancel_ab_semigroup_add
```
```  1013 begin
```
```  1014
```
```  1015 subclass linordered_ab_semigroup_add ..
```
```  1016
```
```  1017 subclass ordered_ab_semigroup_add_imp_le
```
```  1018 proof
```
```  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
```
```  1034 qed
```
```  1035
```
```  1036 end
```
```  1037
```
```  1038 class linordered_ab_group_add = linorder + ordered_ab_group_add
```
```  1039 begin
```
```  1040
```
```  1041 subclass linordered_cancel_ab_semigroup_add ..
```
```  1042
```
```  1043 lemma equal_neg_zero [simp]: "a = - a \<longleftrightarrow> a = 0"
```
```  1044 proof
```
```  1045   assume "a = 0"
```
```  1046   then show "a = - a" by simp
```
```  1047 next
```
```  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
```
```  1061 qed
```
```  1062
```
```  1063 lemma neg_equal_zero [simp]: "- a = a \<longleftrightarrow> a = 0"
```
```  1064   by (auto dest: sym)
```
```  1065
```
```  1066 lemma neg_less_eq_nonneg [simp]: "- a \<le> a \<longleftrightarrow> 0 \<le> a"
```
```  1067 proof
```
```  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
```
```  1076 next
```
```  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)
```
```  1080 qed
```
```  1081
```
```  1082 lemma neg_less_pos [simp]: "- a < a \<longleftrightarrow> 0 < a"
```
```  1083   by (auto simp add: less_le)
```
```  1084
```
```  1085 lemma less_eq_neg_nonpos [simp]: "a \<le> - a \<longleftrightarrow> a \<le> 0"
```
```  1086   using neg_less_eq_nonneg [of "- a"] by simp
```
```  1087
```
```  1088 lemma less_neg_neg [simp]: "a < - a \<longleftrightarrow> a < 0"
```
```  1089   using neg_less_pos [of "- a"] by simp
```
```  1090
```
```  1091 lemma double_zero [simp]: "a + a = 0 \<longleftrightarrow> a = 0"
```
```  1092 proof
```
```  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)
```
```  1096 next
```
```  1097   assume "a = 0"
```
```  1098   then show "a + a = 0" by simp
```
```  1099 qed
```
```  1100
```
```  1101 lemma 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
```
```  1107 lemma zero_less_double_add_iff_zero_less_single_add [simp]: "0 < a + a \<longleftrightarrow> 0 < a"
```
```  1108 proof
```
```  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
```
```  1113 next
```
```  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
```
```  1118 qed
```
```  1119
```
```  1120 lemma 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
```
```  1123 lemma double_add_less_zero_iff_single_add_less_zero [simp]: "a + a < 0 \<longleftrightarrow> a < 0"
```
```  1124 proof -
```
```  1125   have "\<not> a + a < 0 \<longleftrightarrow> \<not> a < 0"
```
```  1126     by (simp add: not_less)
```
```  1127   then show ?thesis by simp
```
```  1128 qed
```
```  1129
```
```  1130 lemma double_add_le_zero_iff_single_add_le_zero [simp]: "a + a \<le> 0 \<longleftrightarrow> a \<le> 0"
```
```  1131 proof -
```
```  1132   have "\<not> a + a \<le> 0 \<longleftrightarrow> \<not> a \<le> 0"
```
```  1133     by (simp add: not_le)
```
```  1134   then show ?thesis by simp
```
```  1135 qed
```
```  1136
```
```  1137 lemma minus_max_eq_min: "- max x y = min (- x) (- y)"
```
```  1138   by (auto simp add: max_def min_def)
```
```  1139
```
```  1140 lemma minus_min_eq_max: "- min x y = max (- x) (- y)"
```
```  1141   by (auto simp add: max_def min_def)
```
```  1142
```
```  1143 end
```
```  1144
```
```  1145 class abs =
```
```  1146   fixes abs :: "'a \<Rightarrow> 'a"  ("\<bar>_\<bar>")
```
```  1147
```
```  1148 class sgn =
```
```  1149   fixes sgn :: "'a \<Rightarrow> 'a"
```
```  1150
```
```  1151 class abs_if = minus + uminus + ord + zero + abs +
```
```  1152   assumes abs_if: "\<bar>a\<bar> = (if a < 0 then - a else a)"
```
```  1153
```
```  1154 class sgn_if = minus + uminus + zero + one + ord + sgn +
```
```  1155   assumes sgn_if: "sgn x = (if x = 0 then 0 else if 0 < x then 1 else - 1)"
```
```  1156 begin
```
```  1157
```
```  1158 lemma sgn0 [simp]: "sgn 0 = 0"
```
```  1159   by (simp add:sgn_if)
```
```  1160
```
```  1161 end
```
```  1162
```
```  1163 class ordered_ab_group_add_abs = ordered_ab_group_add + abs +
```
```  1164   assumes abs_ge_zero [simp]: "\<bar>a\<bar> \<ge> 0"
```
```  1165     and abs_ge_self: "a \<le> \<bar>a\<bar>"
```
```  1166     and abs_leI: "a \<le> b \<Longrightarrow> - a \<le> b \<Longrightarrow> \<bar>a\<bar> \<le> b"
```
```  1167     and abs_minus_cancel [simp]: "\<bar>-a\<bar> = \<bar>a\<bar>"
```
```  1168     and abs_triangle_ineq: "\<bar>a + b\<bar> \<le> \<bar>a\<bar> + \<bar>b\<bar>"
```
```  1169 begin
```
```  1170
```
```  1171 lemma abs_minus_le_zero: "- \<bar>a\<bar> \<le> 0"
```
```  1172   unfolding neg_le_0_iff_le by simp
```
```  1173
```
```  1174 lemma abs_of_nonneg [simp]:
```
```  1175   assumes nonneg: "0 \<le> a"
```
```  1176   shows "\<bar>a\<bar> = a"
```
```  1177 proof (rule antisym)
```
```  1178   show "a \<le> \<bar>a\<bar>" by (rule abs_ge_self)
```
```  1179   from nonneg le_imp_neg_le have "- a \<le> 0" by simp
```
```  1180   from this nonneg have "- a \<le> a" by (rule order_trans)
```
```  1181   then show "\<bar>a\<bar> \<le> a" by (auto intro: abs_leI)
```
```  1182 qed
```
```  1183
```
```  1184 lemma abs_idempotent [simp]: "\<bar>\<bar>a\<bar>\<bar> = \<bar>a\<bar>"
```
```  1185   by (rule antisym) (auto intro!: abs_ge_self abs_leI order_trans [of "- \<bar>a\<bar>" 0 "\<bar>a\<bar>"])
```
```  1186
```
```  1187 lemma abs_eq_0 [simp]: "\<bar>a\<bar> = 0 \<longleftrightarrow> a = 0"
```
```  1188 proof -
```
```  1189   have "\<bar>a\<bar> = 0 \<Longrightarrow> a = 0"
```
```  1190   proof (rule antisym)
```
```  1191     assume zero: "\<bar>a\<bar> = 0"
```
```  1192     with abs_ge_self show "a \<le> 0" by auto
```
```  1193     from zero have "\<bar>-a\<bar> = 0" by simp
```
```  1194     with abs_ge_self [of "- a"] have "- a \<le> 0" by auto
```
```  1195     with neg_le_0_iff_le show "0 \<le> a" by auto
```
```  1196   qed
```
```  1197   then show ?thesis by auto
```
```  1198 qed
```
```  1199
```
```  1200 lemma abs_zero [simp]: "\<bar>0\<bar> = 0"
```
```  1201   by simp
```
```  1202
```
```  1203 lemma abs_0_eq [simp]: "0 = \<bar>a\<bar> \<longleftrightarrow> a = 0"
```
```  1204 proof -
```
```  1205   have "0 = \<bar>a\<bar> \<longleftrightarrow> \<bar>a\<bar> = 0" by (simp only: eq_ac)
```
```  1206   then show ?thesis by simp
```
```  1207 qed
```
```  1208
```
```  1209 lemma abs_le_zero_iff [simp]: "\<bar>a\<bar> \<le> 0 \<longleftrightarrow> a = 0"
```
```  1210 proof
```
```  1211   assume "\<bar>a\<bar> \<le> 0"
```
```  1212   then have "\<bar>a\<bar> = 0" by (rule antisym) simp
```
```  1213   then show "a = 0" by simp
```
```  1214 next
```
```  1215   assume "a = 0"
```
```  1216   then show "\<bar>a\<bar> \<le> 0" by simp
```
```  1217 qed
```
```  1218
```
```  1219 lemma abs_le_self_iff [simp]: "\<bar>a\<bar> \<le> a \<longleftrightarrow> 0 \<le> a"
```
```  1220 proof -
```
```  1221   have "0 \<le> \<bar>a\<bar>"
```
```  1222     using abs_ge_zero by blast
```
```  1223   then have "\<bar>a\<bar> \<le> a \<Longrightarrow> 0 \<le> a"
```
```  1224     using order.trans by blast
```
```  1225   then show ?thesis
```
```  1226     using abs_of_nonneg eq_refl by blast
```
```  1227 qed
```
```  1228
```
```  1229 lemma zero_less_abs_iff [simp]: "0 < \<bar>a\<bar> \<longleftrightarrow> a \<noteq> 0"
```
```  1230   by (simp add: less_le)
```
```  1231
```
```  1232 lemma abs_not_less_zero [simp]: "\<not> \<bar>a\<bar> < 0"
```
```  1233 proof -
```
```  1234   have "x \<le> y \<Longrightarrow> \<not> y < x" for x y by auto
```
```  1235   then show ?thesis by simp
```
```  1236 qed
```
```  1237
```
```  1238 lemma abs_ge_minus_self: "- a \<le> \<bar>a\<bar>"
```
```  1239 proof -
```
```  1240   have "- a \<le> \<bar>-a\<bar>" by (rule abs_ge_self)
```
```  1241   then show ?thesis by simp
```
```  1242 qed
```
```  1243
```
```  1244 lemma abs_minus_commute: "\<bar>a - b\<bar> = \<bar>b - a\<bar>"
```
```  1245 proof -
```
```  1246   have "\<bar>a - b\<bar> = \<bar>- (a - b)\<bar>"
```
```  1247     by (simp only: abs_minus_cancel)
```
```  1248   also have "\<dots> = \<bar>b - a\<bar>" by simp
```
```  1249   finally show ?thesis .
```
```  1250 qed
```
```  1251
```
```  1252 lemma abs_of_pos: "0 < a \<Longrightarrow> \<bar>a\<bar> = a"
```
```  1253   by (rule abs_of_nonneg) (rule less_imp_le)
```
```  1254
```
```  1255 lemma abs_of_nonpos [simp]:
```
```  1256   assumes "a \<le> 0"
```
```  1257   shows "\<bar>a\<bar> = - a"
```
```  1258 proof -
```
```  1259   let ?b = "- a"
```
```  1260   have "- ?b \<le> 0 \<Longrightarrow> \<bar>- ?b\<bar> = - (- ?b)"
```
```  1261     unfolding abs_minus_cancel [of ?b]
```
```  1262     unfolding neg_le_0_iff_le [of ?b]
```
```  1263     unfolding minus_minus by (erule abs_of_nonneg)
```
```  1264   then show ?thesis using assms by auto
```
```  1265 qed
```
```  1266
```
```  1267 lemma abs_of_neg: "a < 0 \<Longrightarrow> \<bar>a\<bar> = - a"
```
```  1268   by (rule abs_of_nonpos) (rule less_imp_le)
```
```  1269
```
```  1270 lemma abs_le_D1: "\<bar>a\<bar> \<le> b \<Longrightarrow> a \<le> b"
```
```  1271   using abs_ge_self by (blast intro: order_trans)
```
```  1272
```
```  1273 lemma abs_le_D2: "\<bar>a\<bar> \<le> b \<Longrightarrow> - a \<le> b"
```
```  1274   using abs_le_D1 [of "- a"] by simp
```
```  1275
```
```  1276 lemma abs_le_iff: "\<bar>a\<bar> \<le> b \<longleftrightarrow> a \<le> b \<and> - a \<le> b"
```
```  1277   by (blast intro: abs_leI dest: abs_le_D1 abs_le_D2)
```
```  1278
```
```  1279 lemma abs_triangle_ineq2: "\<bar>a\<bar> - \<bar>b\<bar> \<le> \<bar>a - b\<bar>"
```
```  1280 proof -
```
```  1281   have "\<bar>a\<bar> = \<bar>b + (a - b)\<bar>"
```
```  1282     by (simp add: algebra_simps)
```
```  1283   then have "\<bar>a\<bar> \<le> \<bar>b\<bar> + \<bar>a - b\<bar>"
```
```  1284     by (simp add: abs_triangle_ineq)
```
```  1285   then show ?thesis
```
```  1286     by (simp add: algebra_simps)
```
```  1287 qed
```
```  1288
```
```  1289 lemma abs_triangle_ineq2_sym: "\<bar>a\<bar> - \<bar>b\<bar> \<le> \<bar>b - a\<bar>"
```
```  1290   by (simp only: abs_minus_commute [of b] abs_triangle_ineq2)
```
```  1291
```
```  1292 lemma abs_triangle_ineq3: "\<bar>\<bar>a\<bar> - \<bar>b\<bar>\<bar> \<le> \<bar>a - b\<bar>"
```
```  1293   by (simp add: abs_le_iff abs_triangle_ineq2 abs_triangle_ineq2_sym)
```
```  1294
```
```  1295 lemma abs_triangle_ineq4: "\<bar>a - b\<bar> \<le> \<bar>a\<bar> + \<bar>b\<bar>"
```
```  1296 proof -
```
```  1297   have "\<bar>a - b\<bar> = \<bar>a + - b\<bar>"
```
```  1298     by (simp add: algebra_simps)
```
```  1299   also have "\<dots> \<le> \<bar>a\<bar> + \<bar>- b\<bar>"
```
```  1300     by (rule abs_triangle_ineq)
```
```  1301   finally show ?thesis by simp
```
```  1302 qed
```
```  1303
```
```  1304 lemma abs_diff_triangle_ineq: "\<bar>a + b - (c + d)\<bar> \<le> \<bar>a - c\<bar> + \<bar>b - d\<bar>"
```
```  1305 proof -
```
```  1306   have "\<bar>a + b - (c + d)\<bar> = \<bar>(a - c) + (b - d)\<bar>"
```
```  1307     by (simp add: algebra_simps)
```
```  1308   also have "\<dots> \<le> \<bar>a - c\<bar> + \<bar>b - d\<bar>"
```
```  1309     by (rule abs_triangle_ineq)
```
```  1310   finally show ?thesis .
```
```  1311 qed
```
```  1312
```
```  1313 lemma abs_add_abs [simp]: "\<bar>\<bar>a\<bar> + \<bar>b\<bar>\<bar> = \<bar>a\<bar> + \<bar>b\<bar>"
```
```  1314   (is "?L = ?R")
```
```  1315 proof (rule antisym)
```
```  1316   show "?L \<ge> ?R" by (rule abs_ge_self)
```
```  1317   have "?L \<le> \<bar>\<bar>a\<bar>\<bar> + \<bar>\<bar>b\<bar>\<bar>" by (rule abs_triangle_ineq)
```
```  1318   also have "\<dots> = ?R" by simp
```
```  1319   finally show "?L \<le> ?R" .
```
```  1320 qed
```
```  1321
```
```  1322 end
```
```  1323
```
```  1324 lemma dense_eq0_I:
```
```  1325   fixes x::"'a::{dense_linorder,ordered_ab_group_add_abs}"
```
```  1326   shows "(\<And>e. 0 < e \<Longrightarrow> \<bar>x\<bar> \<le> e) \<Longrightarrow> x = 0"
```
```  1327   apply (cases "\<bar>x\<bar> = 0")
```
```  1328    apply simp
```
```  1329   apply (simp only: zero_less_abs_iff [symmetric])
```
```  1330   apply (drule dense)
```
```  1331   apply (auto simp add: not_less [symmetric])
```
```  1332   done
```
```  1333
```
```  1334 hide_fact (open) ab_diff_conv_add_uminus add_0 mult_1 ab_left_minus
```
```  1335
```
```  1336 lemmas add_0 = add_0_left (* FIXME duplicate *)
```
```  1337 lemmas mult_1 = mult_1_left (* FIXME duplicate *)
```
```  1338 lemmas ab_left_minus = left_minus (* FIXME duplicate *)
```
```  1339 lemmas diff_diff_eq = diff_diff_add (* FIXME duplicate *)
```
```  1340
```
```  1341
```
```  1342 subsection \<open>Canonically ordered monoids\<close>
```
```  1343
```
```  1344 text \<open>Canonically ordered monoids are never groups.\<close>
```
```  1345
```
```  1346 class canonically_ordered_monoid_add = comm_monoid_add + order +
```
```  1347   assumes le_iff_add: "a \<le> b \<longleftrightarrow> (\<exists>c. b = a + c)"
```
```  1348 begin
```
```  1349
```
```  1350 lemma zero_le[simp]: "0 \<le> x"
```
```  1351   by (auto simp: le_iff_add)
```
```  1352
```
```  1353 lemma le_zero_eq[simp]: "n \<le> 0 \<longleftrightarrow> n = 0"
```
```  1354   by (auto intro: antisym)
```
```  1355
```
```  1356 lemma not_less_zero[simp]: "\<not> n < 0"
```
```  1357   by (auto simp: less_le)
```
```  1358
```
```  1359 lemma zero_less_iff_neq_zero: "0 < n \<longleftrightarrow> n \<noteq> 0"
```
```  1360   by (auto simp: less_le)
```
```  1361
```
```  1362 text \<open>This theorem is useful with \<open>blast\<close>\<close>
```
```  1363 lemma gr_zeroI: "(n = 0 \<Longrightarrow> False) \<Longrightarrow> 0 < n"
```
```  1364   by (rule zero_less_iff_neq_zero[THEN iffD2]) iprover
```
```  1365
```
```  1366 lemma not_gr_zero[simp]: "\<not> 0 < n \<longleftrightarrow> n = 0"
```
```  1367   by (simp add: zero_less_iff_neq_zero)
```
```  1368
```
```  1369 subclass ordered_comm_monoid_add
```
```  1370   proof qed (auto simp: le_iff_add add_ac)
```
```  1371
```
```  1372 lemma add_eq_0_iff_both_eq_0: "x + y = 0 \<longleftrightarrow> x = 0 \<and> y = 0"
```
```  1373   by (intro add_nonneg_eq_0_iff zero_le)
```
```  1374
```
```  1375 lemma gr_implies_not_zero: "m < n \<Longrightarrow> n \<noteq> 0"
```
```  1376   using add_eq_0_iff_both_eq_0[of m] by (auto simp: le_iff_add less_le)
```
```  1377
```
```  1378 lemmas zero_order = zero_le le_zero_eq not_less_zero zero_less_iff_neq_zero not_gr_zero
```
```  1379   \<comment> \<open>This should be attributed with \<open>[iff]\<close>, but then \<open>blast\<close> fails in \<open>Set\<close>.\<close>
```
```  1380
```
```  1381 end
```
```  1382
```
```  1383 class ordered_cancel_comm_monoid_diff =
```
```  1384   canonically_ordered_monoid_add + comm_monoid_diff + ordered_ab_semigroup_add_imp_le
```
```  1385 begin
```
```  1386
```
```  1387 context
```
```  1388   fixes a b :: 'a
```
```  1389   assumes le: "a \<le> b"
```
```  1390 begin
```
```  1391
```
```  1392 lemma add_diff_inverse: "a + (b - a) = b"
```
```  1393   using le by (auto simp add: le_iff_add)
```
```  1394
```
```  1395 lemma add_diff_assoc: "c + (b - a) = c + b - a"
```
```  1396   using le by (auto simp add: le_iff_add add.left_commute [of c])
```
```  1397
```
```  1398 lemma add_diff_assoc2: "b - a + c = b + c - a"
```
```  1399   using le by (auto simp add: le_iff_add add.assoc)
```
```  1400
```
```  1401 lemma diff_add_assoc: "c + b - a = c + (b - a)"
```
```  1402   using le by (simp add: add.commute add_diff_assoc)
```
```  1403
```
```  1404 lemma diff_add_assoc2: "b + c - a = b - a + c"
```
```  1405   using le by (simp add: add.commute add_diff_assoc)
```
```  1406
```
```  1407 lemma diff_diff_right: "c - (b - a) = c + a - b"
```
```  1408   by (simp add: add_diff_inverse add_diff_cancel_left [of a c "b - a", symmetric] add.commute)
```
```  1409
```
```  1410 lemma diff_add: "b - a + a = b"
```
```  1411   by (simp add: add.commute add_diff_inverse)
```
```  1412
```
```  1413 lemma le_add_diff: "c \<le> b + c - a"
```
```  1414   by (auto simp add: add.commute diff_add_assoc2 le_iff_add)
```
```  1415
```
```  1416 lemma le_imp_diff_is_add: "a \<le> b \<Longrightarrow> b - a = c \<longleftrightarrow> b = c + a"
```
```  1417   by (auto simp add: add.commute add_diff_inverse)
```
```  1418
```
```  1419 lemma le_diff_conv2: "c \<le> b - a \<longleftrightarrow> c + a \<le> b"
```
```  1420   (is "?P \<longleftrightarrow> ?Q")
```
```  1421 proof
```
```  1422   assume ?P
```
```  1423   then have "c + a \<le> b - a + a"
```
```  1424     by (rule add_right_mono)
```
```  1425   then show ?Q
```
```  1426     by (simp add: add_diff_inverse add.commute)
```
```  1427 next
```
```  1428   assume ?Q
```
```  1429   then have "a + c \<le> a + (b - a)"
```
```  1430     by (simp add: add_diff_inverse add.commute)
```
```  1431   then show ?P by simp
```
```  1432 qed
```
```  1433
```
```  1434 end
```
```  1435
```
```  1436 end
```
```  1437
```
```  1438
```
```  1439 subsection \<open>Tools setup\<close>
```
```  1440
```
```  1441 lemma add_mono_thms_linordered_semiring:
```
```  1442   fixes i j k :: "'a::ordered_ab_semigroup_add"
```
```  1443   shows "i \<le> j \<and> k \<le> l \<Longrightarrow> i + k \<le> j + l"
```
```  1444     and "i = j \<and> k \<le> l \<Longrightarrow> i + k \<le> j + l"
```
```  1445     and "i \<le> j \<and> k = l \<Longrightarrow> i + k \<le> j + l"
```
```  1446     and "i = j \<and> k = l \<Longrightarrow> i + k = j + l"
```
```  1447   by (rule add_mono, clarify+)+
```
```  1448
```
```  1449 lemma add_mono_thms_linordered_field:
```
```  1450   fixes i j k :: "'a::ordered_cancel_ab_semigroup_add"
```
```  1451   shows "i < j \<and> k = l \<Longrightarrow> i + k < j + l"
```
```  1452     and "i = j \<and> k < l \<Longrightarrow> i + k < j + l"
```
```  1453     and "i < j \<and> k \<le> l \<Longrightarrow> i + k < j + l"
```
```  1454     and "i \<le> j \<and> k < l \<Longrightarrow> i + k < j + l"
```
```  1455     and "i < j \<and> k < l \<Longrightarrow> i + k < j + l"
```
```  1456   by (auto intro: add_strict_right_mono add_strict_left_mono
```
```  1457       add_less_le_mono add_le_less_mono add_strict_mono)
```
```  1458
```
```  1459 code_identifier
```
```  1460   code_module Groups \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith
```
```  1461
```
```  1462 end
```