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