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