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