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