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