src/HOL/Groups.thy
author bulwahn
Fri Oct 21 11:17:14 2011 +0200 (2011-10-21)
changeset 45231 d85a2fdc586c
parent 44848 f4d0b060c7ca
child 45294 3c5d3d286055
permissions -rw-r--r--
replacing code_inline by code_unfold, removing obsolete code_unfold, code_inline del now that the ancient code generator is removed
     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 lemma max_add_distrib_right:
   600   "x + max y z = max (x + y) (x + z)"
   601   unfolding max_def by auto
   602 
   603 lemma min_add_distrib_right:
   604   "x + min y z = min (x + y) (x + z)"
   605   unfolding min_def by auto
   606 
   607 end
   608 
   609 subsection {* Support for reasoning about signs *}
   610 
   611 class ordered_comm_monoid_add =
   612   ordered_cancel_ab_semigroup_add + comm_monoid_add
   613 begin
   614 
   615 lemma add_pos_nonneg:
   616   assumes "0 < a" and "0 \<le> b" shows "0 < a + b"
   617 proof -
   618   have "0 + 0 < a + b" 
   619     using assms by (rule add_less_le_mono)
   620   then show ?thesis by simp
   621 qed
   622 
   623 lemma add_pos_pos:
   624   assumes "0 < a" and "0 < b" shows "0 < a + b"
   625 by (rule add_pos_nonneg) (insert assms, auto)
   626 
   627 lemma add_nonneg_pos:
   628   assumes "0 \<le> a" and "0 < b" shows "0 < a + b"
   629 proof -
   630   have "0 + 0 < a + b" 
   631     using assms by (rule add_le_less_mono)
   632   then show ?thesis by simp
   633 qed
   634 
   635 lemma add_nonneg_nonneg [simp]:
   636   assumes "0 \<le> a" and "0 \<le> b" shows "0 \<le> a + b"
   637 proof -
   638   have "0 + 0 \<le> a + b" 
   639     using assms by (rule add_mono)
   640   then show ?thesis by simp
   641 qed
   642 
   643 lemma add_neg_nonpos:
   644   assumes "a < 0" and "b \<le> 0" shows "a + b < 0"
   645 proof -
   646   have "a + b < 0 + 0"
   647     using assms by (rule add_less_le_mono)
   648   then show ?thesis by simp
   649 qed
   650 
   651 lemma add_neg_neg: 
   652   assumes "a < 0" and "b < 0" shows "a + b < 0"
   653 by (rule add_neg_nonpos) (insert assms, auto)
   654 
   655 lemma add_nonpos_neg:
   656   assumes "a \<le> 0" and "b < 0" shows "a + b < 0"
   657 proof -
   658   have "a + b < 0 + 0"
   659     using assms by (rule add_le_less_mono)
   660   then show ?thesis by simp
   661 qed
   662 
   663 lemma add_nonpos_nonpos:
   664   assumes "a \<le> 0" and "b \<le> 0" shows "a + b \<le> 0"
   665 proof -
   666   have "a + b \<le> 0 + 0"
   667     using assms by (rule add_mono)
   668   then show ?thesis by simp
   669 qed
   670 
   671 lemmas add_sign_intros =
   672   add_pos_nonneg add_pos_pos add_nonneg_pos add_nonneg_nonneg
   673   add_neg_nonpos add_neg_neg add_nonpos_neg add_nonpos_nonpos
   674 
   675 lemma add_nonneg_eq_0_iff:
   676   assumes x: "0 \<le> x" and y: "0 \<le> y"
   677   shows "x + y = 0 \<longleftrightarrow> x = 0 \<and> y = 0"
   678 proof (intro iffI conjI)
   679   have "x = x + 0" by simp
   680   also have "x + 0 \<le> x + y" using y by (rule add_left_mono)
   681   also assume "x + y = 0"
   682   also have "0 \<le> x" using x .
   683   finally show "x = 0" .
   684 next
   685   have "y = 0 + y" by simp
   686   also have "0 + y \<le> x + y" using x by (rule add_right_mono)
   687   also assume "x + y = 0"
   688   also have "0 \<le> y" using y .
   689   finally show "y = 0" .
   690 next
   691   assume "x = 0 \<and> y = 0"
   692   then show "x + y = 0" by simp
   693 qed
   694 
   695 end
   696 
   697 class ordered_ab_group_add =
   698   ab_group_add + ordered_ab_semigroup_add
   699 begin
   700 
   701 subclass ordered_cancel_ab_semigroup_add ..
   702 
   703 subclass ordered_ab_semigroup_add_imp_le
   704 proof
   705   fix a b c :: 'a
   706   assume "c + a \<le> c + b"
   707   hence "(-c) + (c + a) \<le> (-c) + (c + b)" by (rule add_left_mono)
   708   hence "((-c) + c) + a \<le> ((-c) + c) + b" by (simp only: add_assoc)
   709   thus "a \<le> b" by simp
   710 qed
   711 
   712 subclass ordered_comm_monoid_add ..
   713 
   714 lemma max_diff_distrib_left:
   715   shows "max x y - z = max (x - z) (y - z)"
   716 by (simp add: diff_minus, rule max_add_distrib_left) 
   717 
   718 lemma min_diff_distrib_left:
   719   shows "min x y - z = min (x - z) (y - z)"
   720 by (simp add: diff_minus, rule min_add_distrib_left) 
   721 
   722 lemma le_imp_neg_le:
   723   assumes "a \<le> b" shows "-b \<le> -a"
   724 proof -
   725   have "-a+a \<le> -a+b" using `a \<le> b` by (rule add_left_mono) 
   726   hence "0 \<le> -a+b" by simp
   727   hence "0 + (-b) \<le> (-a + b) + (-b)" by (rule add_right_mono) 
   728   thus ?thesis by (simp add: add_assoc)
   729 qed
   730 
   731 lemma neg_le_iff_le [simp]: "- b \<le> - a \<longleftrightarrow> a \<le> b"
   732 proof 
   733   assume "- b \<le> - a"
   734   hence "- (- a) \<le> - (- b)" by (rule le_imp_neg_le)
   735   thus "a\<le>b" by simp
   736 next
   737   assume "a\<le>b"
   738   thus "-b \<le> -a" by (rule le_imp_neg_le)
   739 qed
   740 
   741 lemma neg_le_0_iff_le [simp]: "- a \<le> 0 \<longleftrightarrow> 0 \<le> a"
   742 by (subst neg_le_iff_le [symmetric], simp)
   743 
   744 lemma neg_0_le_iff_le [simp]: "0 \<le> - a \<longleftrightarrow> a \<le> 0"
   745 by (subst neg_le_iff_le [symmetric], simp)
   746 
   747 lemma neg_less_iff_less [simp]: "- b < - a \<longleftrightarrow> a < b"
   748 by (force simp add: less_le) 
   749 
   750 lemma neg_less_0_iff_less [simp]: "- a < 0 \<longleftrightarrow> 0 < a"
   751 by (subst neg_less_iff_less [symmetric], simp)
   752 
   753 lemma neg_0_less_iff_less [simp]: "0 < - a \<longleftrightarrow> a < 0"
   754 by (subst neg_less_iff_less [symmetric], simp)
   755 
   756 text{*The next several equations can make the simplifier loop!*}
   757 
   758 lemma less_minus_iff: "a < - b \<longleftrightarrow> b < - a"
   759 proof -
   760   have "(- (-a) < - b) = (b < - a)" by (rule neg_less_iff_less)
   761   thus ?thesis by simp
   762 qed
   763 
   764 lemma minus_less_iff: "- a < b \<longleftrightarrow> - b < a"
   765 proof -
   766   have "(- a < - (-b)) = (- b < a)" by (rule neg_less_iff_less)
   767   thus ?thesis by simp
   768 qed
   769 
   770 lemma le_minus_iff: "a \<le> - b \<longleftrightarrow> b \<le> - a"
   771 proof -
   772   have mm: "!! a (b::'a). (-(-a)) < -b \<Longrightarrow> -(-b) < -a" by (simp only: minus_less_iff)
   773   have "(- (- a) <= -b) = (b <= - a)" 
   774     apply (auto simp only: le_less)
   775     apply (drule mm)
   776     apply (simp_all)
   777     apply (drule mm[simplified], assumption)
   778     done
   779   then show ?thesis by simp
   780 qed
   781 
   782 lemma minus_le_iff: "- a \<le> b \<longleftrightarrow> - b \<le> a"
   783 by (auto simp add: le_less minus_less_iff)
   784 
   785 lemma diff_less_0_iff_less [simp, no_atp]:
   786   "a - b < 0 \<longleftrightarrow> a < b"
   787 proof -
   788   have "a - b < 0 \<longleftrightarrow> a + (- b) < b + (- b)" by (simp add: diff_minus)
   789   also have "... \<longleftrightarrow> a < b" by (simp only: add_less_cancel_right)
   790   finally show ?thesis .
   791 qed
   792 
   793 lemmas less_iff_diff_less_0 = diff_less_0_iff_less [symmetric]
   794 
   795 lemma diff_less_eq[algebra_simps, field_simps]: "a - b < c \<longleftrightarrow> a < c + b"
   796 apply (subst less_iff_diff_less_0 [of a])
   797 apply (rule less_iff_diff_less_0 [of _ c, THEN ssubst])
   798 apply (simp add: diff_minus add_ac)
   799 done
   800 
   801 lemma less_diff_eq[algebra_simps, field_simps]: "a < c - b \<longleftrightarrow> a + b < c"
   802 apply (subst less_iff_diff_less_0 [of "a + b"])
   803 apply (subst less_iff_diff_less_0 [of a])
   804 apply (simp add: diff_minus add_ac)
   805 done
   806 
   807 lemma diff_le_eq[algebra_simps, field_simps]: "a - b \<le> c \<longleftrightarrow> a \<le> c + b"
   808 by (auto simp add: le_less diff_less_eq diff_add_cancel add_diff_cancel)
   809 
   810 lemma le_diff_eq[algebra_simps, field_simps]: "a \<le> c - b \<longleftrightarrow> a + b \<le> c"
   811 by (auto simp add: le_less less_diff_eq diff_add_cancel add_diff_cancel)
   812 
   813 lemma diff_le_0_iff_le [simp, no_atp]:
   814   "a - b \<le> 0 \<longleftrightarrow> a \<le> b"
   815   by (simp add: algebra_simps)
   816 
   817 lemmas le_iff_diff_le_0 = diff_le_0_iff_le [symmetric]
   818 
   819 lemma diff_eq_diff_less:
   820   "a - b = c - d \<Longrightarrow> a < b \<longleftrightarrow> c < d"
   821   by (auto simp only: less_iff_diff_less_0 [of a b] less_iff_diff_less_0 [of c d])
   822 
   823 lemma diff_eq_diff_less_eq:
   824   "a - b = c - d \<Longrightarrow> a \<le> b \<longleftrightarrow> c \<le> d"
   825   by (auto simp only: le_iff_diff_le_0 [of a b] le_iff_diff_le_0 [of c d])
   826 
   827 end
   828 
   829 use "Tools/abel_cancel.ML"
   830 
   831 simproc_setup abel_cancel_sum
   832   ("a + b::'a::ab_group_add" | "a - b::'a::ab_group_add") =
   833   {* fn phi => Abel_Cancel.sum_proc *}
   834 
   835 simproc_setup abel_cancel_relation
   836   ("a < (b::'a::ordered_ab_group_add)" | "a \<le> (b::'a::ordered_ab_group_add)" | "c = (d::'b::ab_group_add)") =
   837   {* fn phi => Abel_Cancel.rel_proc *}
   838 
   839 class linordered_ab_semigroup_add =
   840   linorder + ordered_ab_semigroup_add
   841 
   842 class linordered_cancel_ab_semigroup_add =
   843   linorder + ordered_cancel_ab_semigroup_add
   844 begin
   845 
   846 subclass linordered_ab_semigroup_add ..
   847 
   848 subclass ordered_ab_semigroup_add_imp_le
   849 proof
   850   fix a b c :: 'a
   851   assume le: "c + a <= c + b"  
   852   show "a <= b"
   853   proof (rule ccontr)
   854     assume w: "~ a \<le> b"
   855     hence "b <= a" by (simp add: linorder_not_le)
   856     hence le2: "c + b <= c + a" by (rule add_left_mono)
   857     have "a = b" 
   858       apply (insert le)
   859       apply (insert le2)
   860       apply (drule antisym, simp_all)
   861       done
   862     with w show False 
   863       by (simp add: linorder_not_le [symmetric])
   864   qed
   865 qed
   866 
   867 end
   868 
   869 class linordered_ab_group_add = linorder + ordered_ab_group_add
   870 begin
   871 
   872 subclass linordered_cancel_ab_semigroup_add ..
   873 
   874 lemma neg_less_eq_nonneg [simp]:
   875   "- a \<le> a \<longleftrightarrow> 0 \<le> a"
   876 proof
   877   assume A: "- a \<le> a" show "0 \<le> a"
   878   proof (rule classical)
   879     assume "\<not> 0 \<le> a"
   880     then have "a < 0" by auto
   881     with A have "- a < 0" by (rule le_less_trans)
   882     then show ?thesis by auto
   883   qed
   884 next
   885   assume A: "0 \<le> a" show "- a \<le> a"
   886   proof (rule order_trans)
   887     show "- a \<le> 0" using A by (simp add: minus_le_iff)
   888   next
   889     show "0 \<le> a" using A .
   890   qed
   891 qed
   892 
   893 lemma neg_less_nonneg [simp]:
   894   "- a < a \<longleftrightarrow> 0 < a"
   895 proof
   896   assume A: "- a < a" show "0 < a"
   897   proof (rule classical)
   898     assume "\<not> 0 < a"
   899     then have "a \<le> 0" by auto
   900     with A have "- a < 0" by (rule less_le_trans)
   901     then show ?thesis by auto
   902   qed
   903 next
   904   assume A: "0 < a" show "- a < a"
   905   proof (rule less_trans)
   906     show "- a < 0" using A by (simp add: minus_le_iff)
   907   next
   908     show "0 < a" using A .
   909   qed
   910 qed
   911 
   912 lemma less_eq_neg_nonpos [simp]:
   913   "a \<le> - a \<longleftrightarrow> a \<le> 0"
   914 proof
   915   assume A: "a \<le> - a" show "a \<le> 0"
   916   proof (rule classical)
   917     assume "\<not> a \<le> 0"
   918     then have "0 < a" by auto
   919     then have "0 < - a" using A by (rule less_le_trans)
   920     then show ?thesis by auto
   921   qed
   922 next
   923   assume A: "a \<le> 0" show "a \<le> - a"
   924   proof (rule order_trans)
   925     show "0 \<le> - a" using A by (simp add: minus_le_iff)
   926   next
   927     show "a \<le> 0" using A .
   928   qed
   929 qed
   930 
   931 lemma equal_neg_zero [simp]:
   932   "a = - a \<longleftrightarrow> a = 0"
   933 proof
   934   assume "a = 0" then show "a = - a" by simp
   935 next
   936   assume A: "a = - a" show "a = 0"
   937   proof (cases "0 \<le> a")
   938     case True with A have "0 \<le> - a" by auto
   939     with le_minus_iff have "a \<le> 0" by simp
   940     with True show ?thesis by (auto intro: order_trans)
   941   next
   942     case False then have B: "a \<le> 0" by auto
   943     with A have "- a \<le> 0" by auto
   944     with B show ?thesis by (auto intro: order_trans)
   945   qed
   946 qed
   947 
   948 lemma neg_equal_zero [simp]:
   949   "- a = a \<longleftrightarrow> a = 0"
   950   by (auto dest: sym)
   951 
   952 lemma double_zero [simp]:
   953   "a + a = 0 \<longleftrightarrow> a = 0"
   954 proof
   955   assume assm: "a + a = 0"
   956   then have a: "- a = a" by (rule minus_unique)
   957   then show "a = 0" by (simp only: neg_equal_zero)
   958 qed simp
   959 
   960 lemma double_zero_sym [simp]:
   961   "0 = a + a \<longleftrightarrow> a = 0"
   962   by (rule, drule sym) simp_all
   963 
   964 lemma zero_less_double_add_iff_zero_less_single_add [simp]:
   965   "0 < a + a \<longleftrightarrow> 0 < a"
   966 proof
   967   assume "0 < a + a"
   968   then have "0 - a < a" by (simp only: diff_less_eq)
   969   then have "- a < a" by simp
   970   then show "0 < a" by (simp only: neg_less_nonneg)
   971 next
   972   assume "0 < a"
   973   with this have "0 + 0 < a + a"
   974     by (rule add_strict_mono)
   975   then show "0 < a + a" by simp
   976 qed
   977 
   978 lemma zero_le_double_add_iff_zero_le_single_add [simp]:
   979   "0 \<le> a + a \<longleftrightarrow> 0 \<le> a"
   980   by (auto simp add: le_less)
   981 
   982 lemma double_add_less_zero_iff_single_add_less_zero [simp]:
   983   "a + a < 0 \<longleftrightarrow> a < 0"
   984 proof -
   985   have "\<not> a + a < 0 \<longleftrightarrow> \<not> a < 0"
   986     by (simp add: not_less)
   987   then show ?thesis by simp
   988 qed
   989 
   990 lemma double_add_le_zero_iff_single_add_le_zero [simp]:
   991   "a + a \<le> 0 \<longleftrightarrow> a \<le> 0" 
   992 proof -
   993   have "\<not> a + a \<le> 0 \<longleftrightarrow> \<not> a \<le> 0"
   994     by (simp add: not_le)
   995   then show ?thesis by simp
   996 qed
   997 
   998 lemma le_minus_self_iff:
   999   "a \<le> - a \<longleftrightarrow> a \<le> 0"
  1000 proof -
  1001   from add_le_cancel_left [of "- a" "a + a" 0]
  1002   have "a \<le> - a \<longleftrightarrow> a + a \<le> 0" 
  1003     by (simp add: add_assoc [symmetric])
  1004   thus ?thesis by simp
  1005 qed
  1006 
  1007 lemma minus_le_self_iff:
  1008   "- a \<le> a \<longleftrightarrow> 0 \<le> a"
  1009 proof -
  1010   from add_le_cancel_left [of "- a" 0 "a + a"]
  1011   have "- a \<le> a \<longleftrightarrow> 0 \<le> a + a" 
  1012     by (simp add: add_assoc [symmetric])
  1013   thus ?thesis by simp
  1014 qed
  1015 
  1016 lemma minus_max_eq_min:
  1017   "- max x y = min (-x) (-y)"
  1018   by (auto simp add: max_def min_def)
  1019 
  1020 lemma minus_min_eq_max:
  1021   "- min x y = max (-x) (-y)"
  1022   by (auto simp add: max_def min_def)
  1023 
  1024 end
  1025 
  1026 context ordered_comm_monoid_add
  1027 begin
  1028 
  1029 lemma add_increasing:
  1030   "0 \<le> a \<Longrightarrow> b \<le> c \<Longrightarrow> b \<le> a + c"
  1031   by (insert add_mono [of 0 a b c], simp)
  1032 
  1033 lemma add_increasing2:
  1034   "0 \<le> c \<Longrightarrow> b \<le> a \<Longrightarrow> b \<le> a + c"
  1035   by (simp add: add_increasing add_commute [of a])
  1036 
  1037 lemma add_strict_increasing:
  1038   "0 < a \<Longrightarrow> b \<le> c \<Longrightarrow> b < a + c"
  1039   by (insert add_less_le_mono [of 0 a b c], simp)
  1040 
  1041 lemma add_strict_increasing2:
  1042   "0 \<le> a \<Longrightarrow> b < c \<Longrightarrow> b < a + c"
  1043   by (insert add_le_less_mono [of 0 a b c], simp)
  1044 
  1045 end
  1046 
  1047 class abs =
  1048   fixes abs :: "'a \<Rightarrow> 'a"
  1049 begin
  1050 
  1051 notation (xsymbols)
  1052   abs  ("\<bar>_\<bar>")
  1053 
  1054 notation (HTML output)
  1055   abs  ("\<bar>_\<bar>")
  1056 
  1057 end
  1058 
  1059 class sgn =
  1060   fixes sgn :: "'a \<Rightarrow> 'a"
  1061 
  1062 class abs_if = minus + uminus + ord + zero + abs +
  1063   assumes abs_if: "\<bar>a\<bar> = (if a < 0 then - a else a)"
  1064 
  1065 class sgn_if = minus + uminus + zero + one + ord + sgn +
  1066   assumes sgn_if: "sgn x = (if x = 0 then 0 else if 0 < x then 1 else - 1)"
  1067 begin
  1068 
  1069 lemma sgn0 [simp]: "sgn 0 = 0"
  1070   by (simp add:sgn_if)
  1071 
  1072 end
  1073 
  1074 class ordered_ab_group_add_abs = ordered_ab_group_add + abs +
  1075   assumes abs_ge_zero [simp]: "\<bar>a\<bar> \<ge> 0"
  1076     and abs_ge_self: "a \<le> \<bar>a\<bar>"
  1077     and abs_leI: "a \<le> b \<Longrightarrow> - a \<le> b \<Longrightarrow> \<bar>a\<bar> \<le> b"
  1078     and abs_minus_cancel [simp]: "\<bar>-a\<bar> = \<bar>a\<bar>"
  1079     and abs_triangle_ineq: "\<bar>a + b\<bar> \<le> \<bar>a\<bar> + \<bar>b\<bar>"
  1080 begin
  1081 
  1082 lemma abs_minus_le_zero: "- \<bar>a\<bar> \<le> 0"
  1083   unfolding neg_le_0_iff_le by simp
  1084 
  1085 lemma abs_of_nonneg [simp]:
  1086   assumes nonneg: "0 \<le> a" shows "\<bar>a\<bar> = a"
  1087 proof (rule antisym)
  1088   from nonneg le_imp_neg_le have "- a \<le> 0" by simp
  1089   from this nonneg have "- a \<le> a" by (rule order_trans)
  1090   then show "\<bar>a\<bar> \<le> a" by (auto intro: abs_leI)
  1091 qed (rule abs_ge_self)
  1092 
  1093 lemma abs_idempotent [simp]: "\<bar>\<bar>a\<bar>\<bar> = \<bar>a\<bar>"
  1094 by (rule antisym)
  1095    (auto intro!: abs_ge_self abs_leI order_trans [of "- \<bar>a\<bar>" 0 "\<bar>a\<bar>"])
  1096 
  1097 lemma abs_eq_0 [simp]: "\<bar>a\<bar> = 0 \<longleftrightarrow> a = 0"
  1098 proof -
  1099   have "\<bar>a\<bar> = 0 \<Longrightarrow> a = 0"
  1100   proof (rule antisym)
  1101     assume zero: "\<bar>a\<bar> = 0"
  1102     with abs_ge_self show "a \<le> 0" by auto
  1103     from zero have "\<bar>-a\<bar> = 0" by simp
  1104     with abs_ge_self [of "- a"] have "- a \<le> 0" by auto
  1105     with neg_le_0_iff_le show "0 \<le> a" by auto
  1106   qed
  1107   then show ?thesis by auto
  1108 qed
  1109 
  1110 lemma abs_zero [simp]: "\<bar>0\<bar> = 0"
  1111 by simp
  1112 
  1113 lemma abs_0_eq [simp, no_atp]: "0 = \<bar>a\<bar> \<longleftrightarrow> a = 0"
  1114 proof -
  1115   have "0 = \<bar>a\<bar> \<longleftrightarrow> \<bar>a\<bar> = 0" by (simp only: eq_ac)
  1116   thus ?thesis by simp
  1117 qed
  1118 
  1119 lemma abs_le_zero_iff [simp]: "\<bar>a\<bar> \<le> 0 \<longleftrightarrow> a = 0" 
  1120 proof
  1121   assume "\<bar>a\<bar> \<le> 0"
  1122   then have "\<bar>a\<bar> = 0" by (rule antisym) simp
  1123   thus "a = 0" by simp
  1124 next
  1125   assume "a = 0"
  1126   thus "\<bar>a\<bar> \<le> 0" by simp
  1127 qed
  1128 
  1129 lemma zero_less_abs_iff [simp]: "0 < \<bar>a\<bar> \<longleftrightarrow> a \<noteq> 0"
  1130 by (simp add: less_le)
  1131 
  1132 lemma abs_not_less_zero [simp]: "\<not> \<bar>a\<bar> < 0"
  1133 proof -
  1134   have a: "\<And>x y. x \<le> y \<Longrightarrow> \<not> y < x" by auto
  1135   show ?thesis by (simp add: a)
  1136 qed
  1137 
  1138 lemma abs_ge_minus_self: "- a \<le> \<bar>a\<bar>"
  1139 proof -
  1140   have "- a \<le> \<bar>-a\<bar>" by (rule abs_ge_self)
  1141   then show ?thesis by simp
  1142 qed
  1143 
  1144 lemma abs_minus_commute: 
  1145   "\<bar>a - b\<bar> = \<bar>b - a\<bar>"
  1146 proof -
  1147   have "\<bar>a - b\<bar> = \<bar>- (a - b)\<bar>" by (simp only: abs_minus_cancel)
  1148   also have "... = \<bar>b - a\<bar>" by simp
  1149   finally show ?thesis .
  1150 qed
  1151 
  1152 lemma abs_of_pos: "0 < a \<Longrightarrow> \<bar>a\<bar> = a"
  1153 by (rule abs_of_nonneg, rule less_imp_le)
  1154 
  1155 lemma abs_of_nonpos [simp]:
  1156   assumes "a \<le> 0" shows "\<bar>a\<bar> = - a"
  1157 proof -
  1158   let ?b = "- a"
  1159   have "- ?b \<le> 0 \<Longrightarrow> \<bar>- ?b\<bar> = - (- ?b)"
  1160   unfolding abs_minus_cancel [of "?b"]
  1161   unfolding neg_le_0_iff_le [of "?b"]
  1162   unfolding minus_minus by (erule abs_of_nonneg)
  1163   then show ?thesis using assms by auto
  1164 qed
  1165   
  1166 lemma abs_of_neg: "a < 0 \<Longrightarrow> \<bar>a\<bar> = - a"
  1167 by (rule abs_of_nonpos, rule less_imp_le)
  1168 
  1169 lemma abs_le_D1: "\<bar>a\<bar> \<le> b \<Longrightarrow> a \<le> b"
  1170 by (insert abs_ge_self, blast intro: order_trans)
  1171 
  1172 lemma abs_le_D2: "\<bar>a\<bar> \<le> b \<Longrightarrow> - a \<le> b"
  1173 by (insert abs_le_D1 [of "- a"], simp)
  1174 
  1175 lemma abs_le_iff: "\<bar>a\<bar> \<le> b \<longleftrightarrow> a \<le> b \<and> - a \<le> b"
  1176 by (blast intro: abs_leI dest: abs_le_D1 abs_le_D2)
  1177 
  1178 lemma abs_triangle_ineq2: "\<bar>a\<bar> - \<bar>b\<bar> \<le> \<bar>a - b\<bar>"
  1179 proof -
  1180   have "\<bar>a\<bar> = \<bar>b + (a - b)\<bar>"
  1181     by (simp add: algebra_simps add_diff_cancel)
  1182   then have "\<bar>a\<bar> \<le> \<bar>b\<bar> + \<bar>a - b\<bar>"
  1183     by (simp add: abs_triangle_ineq)
  1184   then show ?thesis
  1185     by (simp add: algebra_simps)
  1186 qed
  1187 
  1188 lemma abs_triangle_ineq2_sym: "\<bar>a\<bar> - \<bar>b\<bar> \<le> \<bar>b - a\<bar>"
  1189   by (simp only: abs_minus_commute [of b] abs_triangle_ineq2)
  1190 
  1191 lemma abs_triangle_ineq3: "\<bar>\<bar>a\<bar> - \<bar>b\<bar>\<bar> \<le> \<bar>a - b\<bar>"
  1192   by (simp add: abs_le_iff abs_triangle_ineq2 abs_triangle_ineq2_sym)
  1193 
  1194 lemma abs_triangle_ineq4: "\<bar>a - b\<bar> \<le> \<bar>a\<bar> + \<bar>b\<bar>"
  1195 proof -
  1196   have "\<bar>a - b\<bar> = \<bar>a + - b\<bar>" by (subst diff_minus, rule refl)
  1197   also have "... \<le> \<bar>a\<bar> + \<bar>- b\<bar>" by (rule abs_triangle_ineq)
  1198   finally show ?thesis by simp
  1199 qed
  1200 
  1201 lemma abs_diff_triangle_ineq: "\<bar>a + b - (c + d)\<bar> \<le> \<bar>a - c\<bar> + \<bar>b - d\<bar>"
  1202 proof -
  1203   have "\<bar>a + b - (c+d)\<bar> = \<bar>(a-c) + (b-d)\<bar>" by (simp add: diff_minus add_ac)
  1204   also have "... \<le> \<bar>a-c\<bar> + \<bar>b-d\<bar>" by (rule abs_triangle_ineq)
  1205   finally show ?thesis .
  1206 qed
  1207 
  1208 lemma abs_add_abs [simp]:
  1209   "\<bar>\<bar>a\<bar> + \<bar>b\<bar>\<bar> = \<bar>a\<bar> + \<bar>b\<bar>" (is "?L = ?R")
  1210 proof (rule antisym)
  1211   show "?L \<ge> ?R" by(rule abs_ge_self)
  1212 next
  1213   have "?L \<le> \<bar>\<bar>a\<bar>\<bar> + \<bar>\<bar>b\<bar>\<bar>" by(rule abs_triangle_ineq)
  1214   also have "\<dots> = ?R" by simp
  1215   finally show "?L \<le> ?R" .
  1216 qed
  1217 
  1218 end
  1219 
  1220 
  1221 subsection {* Tools setup *}
  1222 
  1223 lemma add_mono_thms_linordered_semiring [no_atp]:
  1224   fixes i j k :: "'a\<Colon>ordered_ab_semigroup_add"
  1225   shows "i \<le> j \<and> k \<le> l \<Longrightarrow> i + k \<le> j + l"
  1226     and "i = j \<and> k \<le> l \<Longrightarrow> i + k \<le> j + l"
  1227     and "i \<le> j \<and> k = l \<Longrightarrow> i + k \<le> j + l"
  1228     and "i = j \<and> k = l \<Longrightarrow> i + k = j + l"
  1229 by (rule add_mono, clarify+)+
  1230 
  1231 lemma add_mono_thms_linordered_field [no_atp]:
  1232   fixes i j k :: "'a\<Colon>ordered_cancel_ab_semigroup_add"
  1233   shows "i < j \<and> k = l \<Longrightarrow> i + k < j + l"
  1234     and "i = j \<and> k < l \<Longrightarrow> i + k < j + l"
  1235     and "i < j \<and> k \<le> l \<Longrightarrow> i + k < j + l"
  1236     and "i \<le> j \<and> k < l \<Longrightarrow> i + k < j + l"
  1237     and "i < j \<and> k < l \<Longrightarrow> i + k < j + l"
  1238 by (auto intro: add_strict_right_mono add_strict_left_mono
  1239   add_less_le_mono add_le_less_mono add_strict_mono)
  1240 
  1241 code_modulename SML
  1242   Groups Arith
  1243 
  1244 code_modulename OCaml
  1245   Groups Arith
  1246 
  1247 code_modulename Haskell
  1248   Groups Arith
  1249 
  1250 
  1251 text {* Legacy *}
  1252 
  1253 lemmas diff_def = diff_minus
  1254 
  1255 end