src/HOL/Groups.thy
author haftmann
Fri Jun 11 17:14:02 2010 +0200 (2010-06-11)
changeset 37407 61dd8c145da7
parent 36977 71c8973a604b
child 37884 314a88278715
permissions -rw-r--r--
declare lex_prod_def [code del]
     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 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 {*
   128 let
   129   fun tr' c = (c, fn show_sorts => fn T => fn ts =>
   130     if (not o null) ts orelse T = dummyT
   131       orelse not (! 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 use "~~/src/Provers/Arith/abel_cancel.ML"
   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 lemmas equals_zero_I = minus_unique (* legacy name *)
   290 
   291 lemma minus_zero [simp]: "- 0 = 0"
   292 proof -
   293   have "0 + 0 = 0" by (rule add_0_right)
   294   thus "- 0 = 0" by (rule minus_unique)
   295 qed
   296 
   297 lemma minus_minus [simp]: "- (- a) = a"
   298 proof -
   299   have "- a + a = 0" by (rule left_minus)
   300   thus "- (- a) = a" by (rule minus_unique)
   301 qed
   302 
   303 lemma right_minus [simp]: "a + - a = 0"
   304 proof -
   305   have "a + - a = - (- a) + - a" by simp
   306   also have "\<dots> = 0" by (rule left_minus)
   307   finally show ?thesis .
   308 qed
   309 
   310 lemma minus_add_cancel: "- a + (a + b) = b"
   311 by (simp add: add_assoc [symmetric])
   312 
   313 lemma add_minus_cancel: "a + (- a + b) = b"
   314 by (simp add: add_assoc [symmetric])
   315 
   316 lemma minus_add: "- (a + b) = - b + - a"
   317 proof -
   318   have "(a + b) + (- b + - a) = 0"
   319     by (simp add: add_assoc add_minus_cancel)
   320   thus "- (a + b) = - b + - a"
   321     by (rule minus_unique)
   322 qed
   323 
   324 lemma right_minus_eq: "a - b = 0 \<longleftrightarrow> a = b"
   325 proof
   326   assume "a - b = 0"
   327   have "a = (a - b) + b" by (simp add:diff_minus add_assoc)
   328   also have "\<dots> = b" using `a - b = 0` by simp
   329   finally show "a = b" .
   330 next
   331   assume "a = b" thus "a - b = 0" by (simp add: diff_minus)
   332 qed
   333 
   334 lemma diff_self [simp]: "a - a = 0"
   335 by (simp add: diff_minus)
   336 
   337 lemma diff_0 [simp]: "0 - a = - a"
   338 by (simp add: diff_minus)
   339 
   340 lemma diff_0_right [simp]: "a - 0 = a" 
   341 by (simp add: diff_minus)
   342 
   343 lemma diff_minus_eq_add [simp]: "a - - b = a + b"
   344 by (simp add: diff_minus)
   345 
   346 lemma neg_equal_iff_equal [simp]:
   347   "- a = - b \<longleftrightarrow> a = b" 
   348 proof 
   349   assume "- a = - b"
   350   hence "- (- a) = - (- b)" by simp
   351   thus "a = b" by simp
   352 next
   353   assume "a = b"
   354   thus "- a = - b" by simp
   355 qed
   356 
   357 lemma neg_equal_0_iff_equal [simp]:
   358   "- a = 0 \<longleftrightarrow> a = 0"
   359 by (subst neg_equal_iff_equal [symmetric], simp)
   360 
   361 lemma neg_0_equal_iff_equal [simp]:
   362   "0 = - a \<longleftrightarrow> 0 = a"
   363 by (subst neg_equal_iff_equal [symmetric], simp)
   364 
   365 text{*The next two equations can make the simplifier loop!*}
   366 
   367 lemma equation_minus_iff:
   368   "a = - b \<longleftrightarrow> b = - a"
   369 proof -
   370   have "- (- a) = - b \<longleftrightarrow> - a = b" by (rule neg_equal_iff_equal)
   371   thus ?thesis by (simp add: eq_commute)
   372 qed
   373 
   374 lemma minus_equation_iff:
   375   "- a = b \<longleftrightarrow> - b = a"
   376 proof -
   377   have "- a = - (- b) \<longleftrightarrow> a = -b" by (rule neg_equal_iff_equal)
   378   thus ?thesis by (simp add: eq_commute)
   379 qed
   380 
   381 lemma diff_add_cancel: "a - b + b = a"
   382 by (simp add: diff_minus add_assoc)
   383 
   384 lemma add_diff_cancel: "a + b - b = a"
   385 by (simp add: diff_minus add_assoc)
   386 
   387 declare diff_minus[symmetric, algebra_simps, field_simps]
   388 
   389 lemma eq_neg_iff_add_eq_0: "a = - b \<longleftrightarrow> a + b = 0"
   390 proof
   391   assume "a = - b" then show "a + b = 0" by simp
   392 next
   393   assume "a + b = 0"
   394   moreover have "a + (b + - b) = (a + b) + - b"
   395     by (simp only: add_assoc)
   396   ultimately show "a = - b" by simp
   397 qed
   398 
   399 end
   400 
   401 class ab_group_add = minus + uminus + comm_monoid_add +
   402   assumes ab_left_minus: "- a + a = 0"
   403   assumes ab_diff_minus: "a - b = a + (- b)"
   404 begin
   405 
   406 subclass group_add
   407   proof qed (simp_all add: ab_left_minus ab_diff_minus)
   408 
   409 subclass cancel_comm_monoid_add
   410 proof
   411   fix a b c :: 'a
   412   assume "a + b = a + c"
   413   then have "- a + a + b = - a + a + c"
   414     unfolding add_assoc by simp
   415   then show "b = c" by simp
   416 qed
   417 
   418 lemma uminus_add_conv_diff[algebra_simps, field_simps]:
   419   "- a + b = b - a"
   420 by (simp add:diff_minus add_commute)
   421 
   422 lemma minus_add_distrib [simp]:
   423   "- (a + b) = - a + - b"
   424 by (rule minus_unique) (simp add: add_ac)
   425 
   426 lemma minus_diff_eq [simp]:
   427   "- (a - b) = b - a"
   428 by (simp add: diff_minus add_commute)
   429 
   430 lemma add_diff_eq[algebra_simps, field_simps]: "a + (b - c) = (a + b) - c"
   431 by (simp add: diff_minus add_ac)
   432 
   433 lemma diff_add_eq[algebra_simps, field_simps]: "(a - b) + c = (a + c) - b"
   434 by (simp add: diff_minus add_ac)
   435 
   436 lemma diff_eq_eq[algebra_simps, field_simps]: "a - b = c \<longleftrightarrow> a = c + b"
   437 by (auto simp add: diff_minus add_assoc)
   438 
   439 lemma eq_diff_eq[algebra_simps, field_simps]: "a = c - b \<longleftrightarrow> a + b = c"
   440 by (auto simp add: diff_minus add_assoc)
   441 
   442 lemma diff_diff_eq[algebra_simps, field_simps]: "(a - b) - c = a - (b + c)"
   443 by (simp add: diff_minus add_ac)
   444 
   445 lemma diff_diff_eq2[algebra_simps, field_simps]: "a - (b - c) = (a + c) - b"
   446 by (simp add: diff_minus add_ac)
   447 
   448 lemma eq_iff_diff_eq_0: "a = b \<longleftrightarrow> a - b = 0"
   449 by (simp add: algebra_simps)
   450 
   451 (* FIXME: duplicates right_minus_eq from class group_add *)
   452 (* but only this one is declared as a simp rule. *)
   453 lemma diff_eq_0_iff_eq [simp, no_atp]: "a - b = 0 \<longleftrightarrow> a = b"
   454 by (simp add: algebra_simps)
   455 
   456 end
   457 
   458 subsection {* (Partially) Ordered Groups *} 
   459 
   460 text {*
   461   The theory of partially ordered groups is taken from the books:
   462   \begin{itemize}
   463   \item \emph{Lattice Theory} by Garret Birkhoff, American Mathematical Society 1979 
   464   \item \emph{Partially Ordered Algebraic Systems}, Pergamon Press 1963
   465   \end{itemize}
   466   Most of the used notions can also be looked up in 
   467   \begin{itemize}
   468   \item \url{http://www.mathworld.com} by Eric Weisstein et. al.
   469   \item \emph{Algebra I} by van der Waerden, Springer.
   470   \end{itemize}
   471 *}
   472 
   473 class ordered_ab_semigroup_add = order + ab_semigroup_add +
   474   assumes add_left_mono: "a \<le> b \<Longrightarrow> c + a \<le> c + b"
   475 begin
   476 
   477 lemma add_right_mono:
   478   "a \<le> b \<Longrightarrow> a + c \<le> b + c"
   479 by (simp add: add_commute [of _ c] add_left_mono)
   480 
   481 text {* non-strict, in both arguments *}
   482 lemma add_mono:
   483   "a \<le> b \<Longrightarrow> c \<le> d \<Longrightarrow> a + c \<le> b + d"
   484   apply (erule add_right_mono [THEN order_trans])
   485   apply (simp add: add_commute add_left_mono)
   486   done
   487 
   488 end
   489 
   490 class ordered_cancel_ab_semigroup_add =
   491   ordered_ab_semigroup_add + cancel_ab_semigroup_add
   492 begin
   493 
   494 lemma add_strict_left_mono:
   495   "a < b \<Longrightarrow> c + a < c + b"
   496 by (auto simp add: less_le add_left_mono)
   497 
   498 lemma add_strict_right_mono:
   499   "a < b \<Longrightarrow> a + c < b + c"
   500 by (simp add: add_commute [of _ c] add_strict_left_mono)
   501 
   502 text{*Strict monotonicity in both arguments*}
   503 lemma add_strict_mono:
   504   "a < b \<Longrightarrow> c < d \<Longrightarrow> a + c < b + d"
   505 apply (erule add_strict_right_mono [THEN less_trans])
   506 apply (erule add_strict_left_mono)
   507 done
   508 
   509 lemma add_less_le_mono:
   510   "a < b \<Longrightarrow> c \<le> d \<Longrightarrow> a + c < b + d"
   511 apply (erule add_strict_right_mono [THEN less_le_trans])
   512 apply (erule add_left_mono)
   513 done
   514 
   515 lemma add_le_less_mono:
   516   "a \<le> b \<Longrightarrow> c < d \<Longrightarrow> a + c < b + d"
   517 apply (erule add_right_mono [THEN le_less_trans])
   518 apply (erule add_strict_left_mono) 
   519 done
   520 
   521 end
   522 
   523 class ordered_ab_semigroup_add_imp_le =
   524   ordered_cancel_ab_semigroup_add +
   525   assumes add_le_imp_le_left: "c + a \<le> c + b \<Longrightarrow> a \<le> b"
   526 begin
   527 
   528 lemma add_less_imp_less_left:
   529   assumes less: "c + a < c + b" shows "a < b"
   530 proof -
   531   from less have le: "c + a <= c + b" by (simp add: order_le_less)
   532   have "a <= b" 
   533     apply (insert le)
   534     apply (drule add_le_imp_le_left)
   535     by (insert le, drule add_le_imp_le_left, assumption)
   536   moreover have "a \<noteq> b"
   537   proof (rule ccontr)
   538     assume "~(a \<noteq> b)"
   539     then have "a = b" by simp
   540     then have "c + a = c + b" by simp
   541     with less show "False"by simp
   542   qed
   543   ultimately show "a < b" by (simp add: order_le_less)
   544 qed
   545 
   546 lemma add_less_imp_less_right:
   547   "a + c < b + c \<Longrightarrow> a < b"
   548 apply (rule add_less_imp_less_left [of c])
   549 apply (simp add: add_commute)  
   550 done
   551 
   552 lemma add_less_cancel_left [simp]:
   553   "c + a < c + b \<longleftrightarrow> a < b"
   554 by (blast intro: add_less_imp_less_left add_strict_left_mono) 
   555 
   556 lemma add_less_cancel_right [simp]:
   557   "a + c < b + c \<longleftrightarrow> a < b"
   558 by (blast intro: add_less_imp_less_right add_strict_right_mono)
   559 
   560 lemma add_le_cancel_left [simp]:
   561   "c + a \<le> c + b \<longleftrightarrow> a \<le> b"
   562 by (auto, drule add_le_imp_le_left, simp_all add: add_left_mono) 
   563 
   564 lemma add_le_cancel_right [simp]:
   565   "a + c \<le> b + c \<longleftrightarrow> a \<le> b"
   566 by (simp add: add_commute [of a c] add_commute [of b c])
   567 
   568 lemma add_le_imp_le_right:
   569   "a + c \<le> b + c \<Longrightarrow> a \<le> b"
   570 by simp
   571 
   572 lemma max_add_distrib_left:
   573   "max x y + z = max (x + z) (y + z)"
   574   unfolding max_def by auto
   575 
   576 lemma min_add_distrib_left:
   577   "min x y + z = min (x + z) (y + z)"
   578   unfolding min_def by auto
   579 
   580 end
   581 
   582 subsection {* Support for reasoning about signs *}
   583 
   584 class ordered_comm_monoid_add =
   585   ordered_cancel_ab_semigroup_add + comm_monoid_add
   586 begin
   587 
   588 lemma add_pos_nonneg:
   589   assumes "0 < a" and "0 \<le> b" shows "0 < a + b"
   590 proof -
   591   have "0 + 0 < a + b" 
   592     using assms by (rule add_less_le_mono)
   593   then show ?thesis by simp
   594 qed
   595 
   596 lemma add_pos_pos:
   597   assumes "0 < a" and "0 < b" shows "0 < a + b"
   598 by (rule add_pos_nonneg) (insert assms, auto)
   599 
   600 lemma add_nonneg_pos:
   601   assumes "0 \<le> a" and "0 < b" shows "0 < a + b"
   602 proof -
   603   have "0 + 0 < a + b" 
   604     using assms by (rule add_le_less_mono)
   605   then show ?thesis by simp
   606 qed
   607 
   608 lemma add_nonneg_nonneg [simp]:
   609   assumes "0 \<le> a" and "0 \<le> b" shows "0 \<le> a + b"
   610 proof -
   611   have "0 + 0 \<le> a + b" 
   612     using assms by (rule add_mono)
   613   then show ?thesis by simp
   614 qed
   615 
   616 lemma add_neg_nonpos:
   617   assumes "a < 0" and "b \<le> 0" shows "a + b < 0"
   618 proof -
   619   have "a + b < 0 + 0"
   620     using assms by (rule add_less_le_mono)
   621   then show ?thesis by simp
   622 qed
   623 
   624 lemma add_neg_neg: 
   625   assumes "a < 0" and "b < 0" shows "a + b < 0"
   626 by (rule add_neg_nonpos) (insert assms, auto)
   627 
   628 lemma add_nonpos_neg:
   629   assumes "a \<le> 0" and "b < 0" shows "a + b < 0"
   630 proof -
   631   have "a + b < 0 + 0"
   632     using assms by (rule add_le_less_mono)
   633   then show ?thesis by simp
   634 qed
   635 
   636 lemma add_nonpos_nonpos:
   637   assumes "a \<le> 0" and "b \<le> 0" shows "a + b \<le> 0"
   638 proof -
   639   have "a + b \<le> 0 + 0"
   640     using assms by (rule add_mono)
   641   then show ?thesis by simp
   642 qed
   643 
   644 lemmas add_sign_intros =
   645   add_pos_nonneg add_pos_pos add_nonneg_pos add_nonneg_nonneg
   646   add_neg_nonpos add_neg_neg add_nonpos_neg add_nonpos_nonpos
   647 
   648 lemma add_nonneg_eq_0_iff:
   649   assumes x: "0 \<le> x" and y: "0 \<le> y"
   650   shows "x + y = 0 \<longleftrightarrow> x = 0 \<and> y = 0"
   651 proof (intro iffI conjI)
   652   have "x = x + 0" by simp
   653   also have "x + 0 \<le> x + y" using y by (rule add_left_mono)
   654   also assume "x + y = 0"
   655   also have "0 \<le> x" using x .
   656   finally show "x = 0" .
   657 next
   658   have "y = 0 + y" by simp
   659   also have "0 + y \<le> x + y" using x by (rule add_right_mono)
   660   also assume "x + y = 0"
   661   also have "0 \<le> y" using y .
   662   finally show "y = 0" .
   663 next
   664   assume "x = 0 \<and> y = 0"
   665   then show "x + y = 0" by simp
   666 qed
   667 
   668 end
   669 
   670 class ordered_ab_group_add =
   671   ab_group_add + ordered_ab_semigroup_add
   672 begin
   673 
   674 subclass ordered_cancel_ab_semigroup_add ..
   675 
   676 subclass ordered_ab_semigroup_add_imp_le
   677 proof
   678   fix a b c :: 'a
   679   assume "c + a \<le> c + b"
   680   hence "(-c) + (c + a) \<le> (-c) + (c + b)" by (rule add_left_mono)
   681   hence "((-c) + c) + a \<le> ((-c) + c) + b" by (simp only: add_assoc)
   682   thus "a \<le> b" by simp
   683 qed
   684 
   685 subclass ordered_comm_monoid_add ..
   686 
   687 lemma max_diff_distrib_left:
   688   shows "max x y - z = max (x - z) (y - z)"
   689 by (simp add: diff_minus, rule max_add_distrib_left) 
   690 
   691 lemma min_diff_distrib_left:
   692   shows "min x y - z = min (x - z) (y - z)"
   693 by (simp add: diff_minus, rule min_add_distrib_left) 
   694 
   695 lemma le_imp_neg_le:
   696   assumes "a \<le> b" shows "-b \<le> -a"
   697 proof -
   698   have "-a+a \<le> -a+b" using `a \<le> b` by (rule add_left_mono) 
   699   hence "0 \<le> -a+b" by simp
   700   hence "0 + (-b) \<le> (-a + b) + (-b)" by (rule add_right_mono) 
   701   thus ?thesis by (simp add: add_assoc)
   702 qed
   703 
   704 lemma neg_le_iff_le [simp]: "- b \<le> - a \<longleftrightarrow> a \<le> b"
   705 proof 
   706   assume "- b \<le> - a"
   707   hence "- (- a) \<le> - (- b)" by (rule le_imp_neg_le)
   708   thus "a\<le>b" by simp
   709 next
   710   assume "a\<le>b"
   711   thus "-b \<le> -a" by (rule le_imp_neg_le)
   712 qed
   713 
   714 lemma neg_le_0_iff_le [simp]: "- a \<le> 0 \<longleftrightarrow> 0 \<le> a"
   715 by (subst neg_le_iff_le [symmetric], simp)
   716 
   717 lemma neg_0_le_iff_le [simp]: "0 \<le> - a \<longleftrightarrow> a \<le> 0"
   718 by (subst neg_le_iff_le [symmetric], simp)
   719 
   720 lemma neg_less_iff_less [simp]: "- b < - a \<longleftrightarrow> a < b"
   721 by (force simp add: less_le) 
   722 
   723 lemma neg_less_0_iff_less [simp]: "- a < 0 \<longleftrightarrow> 0 < a"
   724 by (subst neg_less_iff_less [symmetric], simp)
   725 
   726 lemma neg_0_less_iff_less [simp]: "0 < - a \<longleftrightarrow> a < 0"
   727 by (subst neg_less_iff_less [symmetric], simp)
   728 
   729 text{*The next several equations can make the simplifier loop!*}
   730 
   731 lemma less_minus_iff: "a < - b \<longleftrightarrow> b < - a"
   732 proof -
   733   have "(- (-a) < - b) = (b < - a)" by (rule neg_less_iff_less)
   734   thus ?thesis by simp
   735 qed
   736 
   737 lemma minus_less_iff: "- a < b \<longleftrightarrow> - b < a"
   738 proof -
   739   have "(- a < - (-b)) = (- b < a)" by (rule neg_less_iff_less)
   740   thus ?thesis by simp
   741 qed
   742 
   743 lemma le_minus_iff: "a \<le> - b \<longleftrightarrow> b \<le> - a"
   744 proof -
   745   have mm: "!! a (b::'a). (-(-a)) < -b \<Longrightarrow> -(-b) < -a" by (simp only: minus_less_iff)
   746   have "(- (- a) <= -b) = (b <= - a)" 
   747     apply (auto simp only: le_less)
   748     apply (drule mm)
   749     apply (simp_all)
   750     apply (drule mm[simplified], assumption)
   751     done
   752   then show ?thesis by simp
   753 qed
   754 
   755 lemma minus_le_iff: "- a \<le> b \<longleftrightarrow> - b \<le> a"
   756 by (auto simp add: le_less minus_less_iff)
   757 
   758 lemma less_iff_diff_less_0: "a < b \<longleftrightarrow> a - b < 0"
   759 proof -
   760   have  "(a < b) = (a + (- b) < b + (-b))"  
   761     by (simp only: add_less_cancel_right)
   762   also have "... =  (a - b < 0)" by (simp add: diff_minus)
   763   finally show ?thesis .
   764 qed
   765 
   766 lemma diff_less_eq[algebra_simps, field_simps]: "a - b < c \<longleftrightarrow> a < c + b"
   767 apply (subst less_iff_diff_less_0 [of a])
   768 apply (rule less_iff_diff_less_0 [of _ c, THEN ssubst])
   769 apply (simp add: diff_minus add_ac)
   770 done
   771 
   772 lemma less_diff_eq[algebra_simps, field_simps]: "a < c - b \<longleftrightarrow> a + b < c"
   773 apply (subst less_iff_diff_less_0 [of "a + b"])
   774 apply (subst less_iff_diff_less_0 [of a])
   775 apply (simp add: diff_minus add_ac)
   776 done
   777 
   778 lemma diff_le_eq[algebra_simps, field_simps]: "a - b \<le> c \<longleftrightarrow> a \<le> c + b"
   779 by (auto simp add: le_less diff_less_eq diff_add_cancel add_diff_cancel)
   780 
   781 lemma le_diff_eq[algebra_simps, field_simps]: "a \<le> c - b \<longleftrightarrow> a + b \<le> c"
   782 by (auto simp add: le_less less_diff_eq diff_add_cancel add_diff_cancel)
   783 
   784 lemma le_iff_diff_le_0: "a \<le> b \<longleftrightarrow> a - b \<le> 0"
   785 by (simp add: algebra_simps)
   786 
   787 end
   788 
   789 class linordered_ab_semigroup_add =
   790   linorder + ordered_ab_semigroup_add
   791 
   792 class linordered_cancel_ab_semigroup_add =
   793   linorder + ordered_cancel_ab_semigroup_add
   794 begin
   795 
   796 subclass linordered_ab_semigroup_add ..
   797 
   798 subclass ordered_ab_semigroup_add_imp_le
   799 proof
   800   fix a b c :: 'a
   801   assume le: "c + a <= c + b"  
   802   show "a <= b"
   803   proof (rule ccontr)
   804     assume w: "~ a \<le> b"
   805     hence "b <= a" by (simp add: linorder_not_le)
   806     hence le2: "c + b <= c + a" by (rule add_left_mono)
   807     have "a = b" 
   808       apply (insert le)
   809       apply (insert le2)
   810       apply (drule antisym, simp_all)
   811       done
   812     with w show False 
   813       by (simp add: linorder_not_le [symmetric])
   814   qed
   815 qed
   816 
   817 end
   818 
   819 class linordered_ab_group_add = linorder + ordered_ab_group_add
   820 begin
   821 
   822 subclass linordered_cancel_ab_semigroup_add ..
   823 
   824 lemma neg_less_eq_nonneg [simp]:
   825   "- a \<le> a \<longleftrightarrow> 0 \<le> a"
   826 proof
   827   assume A: "- a \<le> a" show "0 \<le> a"
   828   proof (rule classical)
   829     assume "\<not> 0 \<le> a"
   830     then have "a < 0" by auto
   831     with A have "- a < 0" by (rule le_less_trans)
   832     then show ?thesis by auto
   833   qed
   834 next
   835   assume A: "0 \<le> a" show "- a \<le> a"
   836   proof (rule order_trans)
   837     show "- a \<le> 0" using A by (simp add: minus_le_iff)
   838   next
   839     show "0 \<le> a" using A .
   840   qed
   841 qed
   842 
   843 lemma neg_less_nonneg [simp]:
   844   "- a < a \<longleftrightarrow> 0 < a"
   845 proof
   846   assume A: "- a < a" show "0 < a"
   847   proof (rule classical)
   848     assume "\<not> 0 < a"
   849     then have "a \<le> 0" by auto
   850     with A have "- a < 0" by (rule less_le_trans)
   851     then show ?thesis by auto
   852   qed
   853 next
   854   assume A: "0 < a" show "- a < a"
   855   proof (rule less_trans)
   856     show "- a < 0" using A by (simp add: minus_le_iff)
   857   next
   858     show "0 < a" using A .
   859   qed
   860 qed
   861 
   862 lemma less_eq_neg_nonpos [simp]:
   863   "a \<le> - a \<longleftrightarrow> a \<le> 0"
   864 proof
   865   assume A: "a \<le> - a" show "a \<le> 0"
   866   proof (rule classical)
   867     assume "\<not> a \<le> 0"
   868     then have "0 < a" by auto
   869     then have "0 < - a" using A by (rule less_le_trans)
   870     then show ?thesis by auto
   871   qed
   872 next
   873   assume A: "a \<le> 0" show "a \<le> - a"
   874   proof (rule order_trans)
   875     show "0 \<le> - a" using A by (simp add: minus_le_iff)
   876   next
   877     show "a \<le> 0" using A .
   878   qed
   879 qed
   880 
   881 lemma equal_neg_zero [simp]:
   882   "a = - a \<longleftrightarrow> a = 0"
   883 proof
   884   assume "a = 0" then show "a = - a" by simp
   885 next
   886   assume A: "a = - a" show "a = 0"
   887   proof (cases "0 \<le> a")
   888     case True with A have "0 \<le> - a" by auto
   889     with le_minus_iff have "a \<le> 0" by simp
   890     with True show ?thesis by (auto intro: order_trans)
   891   next
   892     case False then have B: "a \<le> 0" by auto
   893     with A have "- a \<le> 0" by auto
   894     with B show ?thesis by (auto intro: order_trans)
   895   qed
   896 qed
   897 
   898 lemma neg_equal_zero [simp]:
   899   "- a = a \<longleftrightarrow> a = 0"
   900   by (auto dest: sym)
   901 
   902 lemma double_zero [simp]:
   903   "a + a = 0 \<longleftrightarrow> a = 0"
   904 proof
   905   assume assm: "a + a = 0"
   906   then have a: "- a = a" by (rule minus_unique)
   907   then show "a = 0" by (simp only: neg_equal_zero)
   908 qed simp
   909 
   910 lemma double_zero_sym [simp]:
   911   "0 = a + a \<longleftrightarrow> a = 0"
   912   by (rule, drule sym) simp_all
   913 
   914 lemma zero_less_double_add_iff_zero_less_single_add [simp]:
   915   "0 < a + a \<longleftrightarrow> 0 < a"
   916 proof
   917   assume "0 < a + a"
   918   then have "0 - a < a" by (simp only: diff_less_eq)
   919   then have "- a < a" by simp
   920   then show "0 < a" by (simp only: neg_less_nonneg)
   921 next
   922   assume "0 < a"
   923   with this have "0 + 0 < a + a"
   924     by (rule add_strict_mono)
   925   then show "0 < a + a" by simp
   926 qed
   927 
   928 lemma zero_le_double_add_iff_zero_le_single_add [simp]:
   929   "0 \<le> a + a \<longleftrightarrow> 0 \<le> a"
   930   by (auto simp add: le_less)
   931 
   932 lemma double_add_less_zero_iff_single_add_less_zero [simp]:
   933   "a + a < 0 \<longleftrightarrow> a < 0"
   934 proof -
   935   have "\<not> a + a < 0 \<longleftrightarrow> \<not> a < 0"
   936     by (simp add: not_less)
   937   then show ?thesis by simp
   938 qed
   939 
   940 lemma double_add_le_zero_iff_single_add_le_zero [simp]:
   941   "a + a \<le> 0 \<longleftrightarrow> a \<le> 0" 
   942 proof -
   943   have "\<not> a + a \<le> 0 \<longleftrightarrow> \<not> a \<le> 0"
   944     by (simp add: not_le)
   945   then show ?thesis by simp
   946 qed
   947 
   948 lemma le_minus_self_iff:
   949   "a \<le> - a \<longleftrightarrow> a \<le> 0"
   950 proof -
   951   from add_le_cancel_left [of "- a" "a + a" 0]
   952   have "a \<le> - a \<longleftrightarrow> a + a \<le> 0" 
   953     by (simp add: add_assoc [symmetric])
   954   thus ?thesis by simp
   955 qed
   956 
   957 lemma minus_le_self_iff:
   958   "- a \<le> a \<longleftrightarrow> 0 \<le> a"
   959 proof -
   960   from add_le_cancel_left [of "- a" 0 "a + a"]
   961   have "- a \<le> a \<longleftrightarrow> 0 \<le> a + a" 
   962     by (simp add: add_assoc [symmetric])
   963   thus ?thesis by simp
   964 qed
   965 
   966 lemma minus_max_eq_min:
   967   "- max x y = min (-x) (-y)"
   968   by (auto simp add: max_def min_def)
   969 
   970 lemma minus_min_eq_max:
   971   "- min x y = max (-x) (-y)"
   972   by (auto simp add: max_def min_def)
   973 
   974 end
   975 
   976 context ordered_comm_monoid_add
   977 begin
   978 
   979 lemma add_increasing:
   980   "0 \<le> a \<Longrightarrow> b \<le> c \<Longrightarrow> b \<le> a + c"
   981   by (insert add_mono [of 0 a b c], simp)
   982 
   983 lemma add_increasing2:
   984   "0 \<le> c \<Longrightarrow> b \<le> a \<Longrightarrow> b \<le> a + c"
   985   by (simp add: add_increasing add_commute [of a])
   986 
   987 lemma add_strict_increasing:
   988   "0 < a \<Longrightarrow> b \<le> c \<Longrightarrow> b < a + c"
   989   by (insert add_less_le_mono [of 0 a b c], simp)
   990 
   991 lemma add_strict_increasing2:
   992   "0 \<le> a \<Longrightarrow> b < c \<Longrightarrow> b < a + c"
   993   by (insert add_le_less_mono [of 0 a b c], simp)
   994 
   995 end
   996 
   997 class abs =
   998   fixes abs :: "'a \<Rightarrow> 'a"
   999 begin
  1000 
  1001 notation (xsymbols)
  1002   abs  ("\<bar>_\<bar>")
  1003 
  1004 notation (HTML output)
  1005   abs  ("\<bar>_\<bar>")
  1006 
  1007 end
  1008 
  1009 class sgn =
  1010   fixes sgn :: "'a \<Rightarrow> 'a"
  1011 
  1012 class abs_if = minus + uminus + ord + zero + abs +
  1013   assumes abs_if: "\<bar>a\<bar> = (if a < 0 then - a else a)"
  1014 
  1015 class sgn_if = minus + uminus + zero + one + ord + sgn +
  1016   assumes sgn_if: "sgn x = (if x = 0 then 0 else if 0 < x then 1 else - 1)"
  1017 begin
  1018 
  1019 lemma sgn0 [simp]: "sgn 0 = 0"
  1020   by (simp add:sgn_if)
  1021 
  1022 end
  1023 
  1024 class ordered_ab_group_add_abs = ordered_ab_group_add + abs +
  1025   assumes abs_ge_zero [simp]: "\<bar>a\<bar> \<ge> 0"
  1026     and abs_ge_self: "a \<le> \<bar>a\<bar>"
  1027     and abs_leI: "a \<le> b \<Longrightarrow> - a \<le> b \<Longrightarrow> \<bar>a\<bar> \<le> b"
  1028     and abs_minus_cancel [simp]: "\<bar>-a\<bar> = \<bar>a\<bar>"
  1029     and abs_triangle_ineq: "\<bar>a + b\<bar> \<le> \<bar>a\<bar> + \<bar>b\<bar>"
  1030 begin
  1031 
  1032 lemma abs_minus_le_zero: "- \<bar>a\<bar> \<le> 0"
  1033   unfolding neg_le_0_iff_le by simp
  1034 
  1035 lemma abs_of_nonneg [simp]:
  1036   assumes nonneg: "0 \<le> a" shows "\<bar>a\<bar> = a"
  1037 proof (rule antisym)
  1038   from nonneg le_imp_neg_le have "- a \<le> 0" by simp
  1039   from this nonneg have "- a \<le> a" by (rule order_trans)
  1040   then show "\<bar>a\<bar> \<le> a" by (auto intro: abs_leI)
  1041 qed (rule abs_ge_self)
  1042 
  1043 lemma abs_idempotent [simp]: "\<bar>\<bar>a\<bar>\<bar> = \<bar>a\<bar>"
  1044 by (rule antisym)
  1045    (auto intro!: abs_ge_self abs_leI order_trans [of "- \<bar>a\<bar>" 0 "\<bar>a\<bar>"])
  1046 
  1047 lemma abs_eq_0 [simp]: "\<bar>a\<bar> = 0 \<longleftrightarrow> a = 0"
  1048 proof -
  1049   have "\<bar>a\<bar> = 0 \<Longrightarrow> a = 0"
  1050   proof (rule antisym)
  1051     assume zero: "\<bar>a\<bar> = 0"
  1052     with abs_ge_self show "a \<le> 0" by auto
  1053     from zero have "\<bar>-a\<bar> = 0" by simp
  1054     with abs_ge_self [of "- a"] have "- a \<le> 0" by auto
  1055     with neg_le_0_iff_le show "0 \<le> a" by auto
  1056   qed
  1057   then show ?thesis by auto
  1058 qed
  1059 
  1060 lemma abs_zero [simp]: "\<bar>0\<bar> = 0"
  1061 by simp
  1062 
  1063 lemma abs_0_eq [simp, no_atp]: "0 = \<bar>a\<bar> \<longleftrightarrow> a = 0"
  1064 proof -
  1065   have "0 = \<bar>a\<bar> \<longleftrightarrow> \<bar>a\<bar> = 0" by (simp only: eq_ac)
  1066   thus ?thesis by simp
  1067 qed
  1068 
  1069 lemma abs_le_zero_iff [simp]: "\<bar>a\<bar> \<le> 0 \<longleftrightarrow> a = 0" 
  1070 proof
  1071   assume "\<bar>a\<bar> \<le> 0"
  1072   then have "\<bar>a\<bar> = 0" by (rule antisym) simp
  1073   thus "a = 0" by simp
  1074 next
  1075   assume "a = 0"
  1076   thus "\<bar>a\<bar> \<le> 0" by simp
  1077 qed
  1078 
  1079 lemma zero_less_abs_iff [simp]: "0 < \<bar>a\<bar> \<longleftrightarrow> a \<noteq> 0"
  1080 by (simp add: less_le)
  1081 
  1082 lemma abs_not_less_zero [simp]: "\<not> \<bar>a\<bar> < 0"
  1083 proof -
  1084   have a: "\<And>x y. x \<le> y \<Longrightarrow> \<not> y < x" by auto
  1085   show ?thesis by (simp add: a)
  1086 qed
  1087 
  1088 lemma abs_ge_minus_self: "- a \<le> \<bar>a\<bar>"
  1089 proof -
  1090   have "- a \<le> \<bar>-a\<bar>" by (rule abs_ge_self)
  1091   then show ?thesis by simp
  1092 qed
  1093 
  1094 lemma abs_minus_commute: 
  1095   "\<bar>a - b\<bar> = \<bar>b - a\<bar>"
  1096 proof -
  1097   have "\<bar>a - b\<bar> = \<bar>- (a - b)\<bar>" by (simp only: abs_minus_cancel)
  1098   also have "... = \<bar>b - a\<bar>" by simp
  1099   finally show ?thesis .
  1100 qed
  1101 
  1102 lemma abs_of_pos: "0 < a \<Longrightarrow> \<bar>a\<bar> = a"
  1103 by (rule abs_of_nonneg, rule less_imp_le)
  1104 
  1105 lemma abs_of_nonpos [simp]:
  1106   assumes "a \<le> 0" shows "\<bar>a\<bar> = - a"
  1107 proof -
  1108   let ?b = "- a"
  1109   have "- ?b \<le> 0 \<Longrightarrow> \<bar>- ?b\<bar> = - (- ?b)"
  1110   unfolding abs_minus_cancel [of "?b"]
  1111   unfolding neg_le_0_iff_le [of "?b"]
  1112   unfolding minus_minus by (erule abs_of_nonneg)
  1113   then show ?thesis using assms by auto
  1114 qed
  1115   
  1116 lemma abs_of_neg: "a < 0 \<Longrightarrow> \<bar>a\<bar> = - a"
  1117 by (rule abs_of_nonpos, rule less_imp_le)
  1118 
  1119 lemma abs_le_D1: "\<bar>a\<bar> \<le> b \<Longrightarrow> a \<le> b"
  1120 by (insert abs_ge_self, blast intro: order_trans)
  1121 
  1122 lemma abs_le_D2: "\<bar>a\<bar> \<le> b \<Longrightarrow> - a \<le> b"
  1123 by (insert abs_le_D1 [of "- a"], simp)
  1124 
  1125 lemma abs_le_iff: "\<bar>a\<bar> \<le> b \<longleftrightarrow> a \<le> b \<and> - a \<le> b"
  1126 by (blast intro: abs_leI dest: abs_le_D1 abs_le_D2)
  1127 
  1128 lemma abs_triangle_ineq2: "\<bar>a\<bar> - \<bar>b\<bar> \<le> \<bar>a - b\<bar>"
  1129 proof -
  1130   have "\<bar>a\<bar> = \<bar>b + (a - b)\<bar>"
  1131     by (simp add: algebra_simps add_diff_cancel)
  1132   then have "\<bar>a\<bar> \<le> \<bar>b\<bar> + \<bar>a - b\<bar>"
  1133     by (simp add: abs_triangle_ineq)
  1134   then show ?thesis
  1135     by (simp add: algebra_simps)
  1136 qed
  1137 
  1138 lemma abs_triangle_ineq2_sym: "\<bar>a\<bar> - \<bar>b\<bar> \<le> \<bar>b - a\<bar>"
  1139   by (simp only: abs_minus_commute [of b] abs_triangle_ineq2)
  1140 
  1141 lemma abs_triangle_ineq3: "\<bar>\<bar>a\<bar> - \<bar>b\<bar>\<bar> \<le> \<bar>a - b\<bar>"
  1142   by (simp add: abs_le_iff abs_triangle_ineq2 abs_triangle_ineq2_sym)
  1143 
  1144 lemma abs_triangle_ineq4: "\<bar>a - b\<bar> \<le> \<bar>a\<bar> + \<bar>b\<bar>"
  1145 proof -
  1146   have "\<bar>a - b\<bar> = \<bar>a + - b\<bar>" by (subst diff_minus, rule refl)
  1147   also have "... \<le> \<bar>a\<bar> + \<bar>- b\<bar>" by (rule abs_triangle_ineq)
  1148   finally show ?thesis by simp
  1149 qed
  1150 
  1151 lemma abs_diff_triangle_ineq: "\<bar>a + b - (c + d)\<bar> \<le> \<bar>a - c\<bar> + \<bar>b - d\<bar>"
  1152 proof -
  1153   have "\<bar>a + b - (c+d)\<bar> = \<bar>(a-c) + (b-d)\<bar>" by (simp add: diff_minus add_ac)
  1154   also have "... \<le> \<bar>a-c\<bar> + \<bar>b-d\<bar>" by (rule abs_triangle_ineq)
  1155   finally show ?thesis .
  1156 qed
  1157 
  1158 lemma abs_add_abs [simp]:
  1159   "\<bar>\<bar>a\<bar> + \<bar>b\<bar>\<bar> = \<bar>a\<bar> + \<bar>b\<bar>" (is "?L = ?R")
  1160 proof (rule antisym)
  1161   show "?L \<ge> ?R" by(rule abs_ge_self)
  1162 next
  1163   have "?L \<le> \<bar>\<bar>a\<bar>\<bar> + \<bar>\<bar>b\<bar>\<bar>" by(rule abs_triangle_ineq)
  1164   also have "\<dots> = ?R" by simp
  1165   finally show "?L \<le> ?R" .
  1166 qed
  1167 
  1168 end
  1169 
  1170 text {* Needed for abelian cancellation simprocs: *}
  1171 
  1172 lemma add_cancel_21: "((x::'a::ab_group_add) + (y + z) = y + u) = (x + z = u)"
  1173 apply (subst add_left_commute)
  1174 apply (subst add_left_cancel)
  1175 apply simp
  1176 done
  1177 
  1178 lemma add_cancel_end: "(x + (y + z) = y) = (x = - (z::'a::ab_group_add))"
  1179 apply (subst add_cancel_21[of _ _ _ 0, simplified])
  1180 apply (simp add: add_right_cancel[symmetric, of "x" "-z" "z", simplified])
  1181 done
  1182 
  1183 lemma less_eqI: "(x::'a::ordered_ab_group_add) - y = x' - y' \<Longrightarrow> (x < y) = (x' < y')"
  1184 by (simp add: less_iff_diff_less_0[of x y] less_iff_diff_less_0[of x' y'])
  1185 
  1186 lemma le_eqI: "(x::'a::ordered_ab_group_add) - y = x' - y' \<Longrightarrow> (y <= x) = (y' <= x')"
  1187 apply (simp add: le_iff_diff_le_0[of y x] le_iff_diff_le_0[of  y' x'])
  1188 apply (simp add: neg_le_iff_le[symmetric, of "y-x" 0] neg_le_iff_le[symmetric, of "y'-x'" 0])
  1189 done
  1190 
  1191 lemma eq_eqI: "(x::'a::ab_group_add) - y = x' - y' \<Longrightarrow> (x = y) = (x' = y')"
  1192 by (simp only: eq_iff_diff_eq_0[of x y] eq_iff_diff_eq_0[of x' y'])
  1193 
  1194 lemma diff_def: "(x::'a::ab_group_add) - y == x + (-y)"
  1195 by (simp add: diff_minus)
  1196 
  1197 lemma le_add_right_mono: 
  1198   assumes 
  1199   "a <= b + (c::'a::ordered_ab_group_add)"
  1200   "c <= d"    
  1201   shows "a <= b + d"
  1202   apply (rule_tac order_trans[where y = "b+c"])
  1203   apply (simp_all add: prems)
  1204   done
  1205 
  1206 
  1207 subsection {* Tools setup *}
  1208 
  1209 lemma add_mono_thms_linordered_semiring [no_atp]:
  1210   fixes i j k :: "'a\<Colon>ordered_ab_semigroup_add"
  1211   shows "i \<le> j \<and> k \<le> l \<Longrightarrow> i + k \<le> j + l"
  1212     and "i = j \<and> k \<le> l \<Longrightarrow> i + k \<le> j + l"
  1213     and "i \<le> j \<and> k = l \<Longrightarrow> i + k \<le> j + l"
  1214     and "i = j \<and> k = l \<Longrightarrow> i + k = j + l"
  1215 by (rule add_mono, clarify+)+
  1216 
  1217 lemma add_mono_thms_linordered_field [no_atp]:
  1218   fixes i j k :: "'a\<Colon>ordered_cancel_ab_semigroup_add"
  1219   shows "i < j \<and> k = l \<Longrightarrow> i + k < j + l"
  1220     and "i = j \<and> k < l \<Longrightarrow> i + k < j + l"
  1221     and "i < j \<and> k \<le> l \<Longrightarrow> i + k < j + l"
  1222     and "i \<le> j \<and> k < l \<Longrightarrow> i + k < j + l"
  1223     and "i < j \<and> k < l \<Longrightarrow> i + k < j + l"
  1224 by (auto intro: add_strict_right_mono add_strict_left_mono
  1225   add_less_le_mono add_le_less_mono add_strict_mono)
  1226 
  1227 text{*Simplification of @{term "x-y < 0"}, etc.*}
  1228 lemmas diff_less_0_iff_less [simp, no_atp] = less_iff_diff_less_0 [symmetric]
  1229 lemmas diff_le_0_iff_le [simp, no_atp] = le_iff_diff_le_0 [symmetric]
  1230 
  1231 ML {*
  1232 structure ab_group_add_cancel = Abel_Cancel
  1233 (
  1234 
  1235 (* term order for abelian groups *)
  1236 
  1237 fun agrp_ord (Const (a, _)) = find_index (fn a' => a = a')
  1238       [@{const_name Groups.zero}, @{const_name Groups.plus},
  1239         @{const_name Groups.uminus}, @{const_name Groups.minus}]
  1240   | agrp_ord _ = ~1;
  1241 
  1242 fun termless_agrp (a, b) = (Term_Ord.term_lpo agrp_ord (a, b) = LESS);
  1243 
  1244 local
  1245   val ac1 = mk_meta_eq @{thm add_assoc};
  1246   val ac2 = mk_meta_eq @{thm add_commute};
  1247   val ac3 = mk_meta_eq @{thm add_left_commute};
  1248   fun solve_add_ac thy _ (_ $ (Const (@{const_name Groups.plus},_) $ _ $ _) $ _) =
  1249         SOME ac1
  1250     | solve_add_ac thy _ (_ $ x $ (Const (@{const_name Groups.plus},_) $ y $ z)) =
  1251         if termless_agrp (y, x) then SOME ac3 else NONE
  1252     | solve_add_ac thy _ (_ $ x $ y) =
  1253         if termless_agrp (y, x) then SOME ac2 else NONE
  1254     | solve_add_ac thy _ _ = NONE
  1255 in
  1256   val add_ac_proc = Simplifier.simproc @{theory}
  1257     "add_ac_proc" ["x + y::'a::ab_semigroup_add"] solve_add_ac;
  1258 end;
  1259 
  1260 val eq_reflection = @{thm eq_reflection};
  1261   
  1262 val T = @{typ "'a::ab_group_add"};
  1263 
  1264 val cancel_ss = HOL_basic_ss settermless termless_agrp
  1265   addsimprocs [add_ac_proc] addsimps
  1266   [@{thm add_0_left}, @{thm add_0_right}, @{thm diff_def},
  1267    @{thm minus_add_distrib}, @{thm minus_minus}, @{thm minus_zero},
  1268    @{thm right_minus}, @{thm left_minus}, @{thm add_minus_cancel},
  1269    @{thm minus_add_cancel}];
  1270 
  1271 val sum_pats = [@{cterm "x + y::'a::ab_group_add"}, @{cterm "x - y::'a::ab_group_add"}];
  1272   
  1273 val eqI_rules = [@{thm less_eqI}, @{thm le_eqI}, @{thm eq_eqI}];
  1274 
  1275 val dest_eqI = 
  1276   fst o HOLogic.dest_bin @{const_name "op ="} HOLogic.boolT o HOLogic.dest_Trueprop o concl_of;
  1277 
  1278 );
  1279 *}
  1280 
  1281 ML {*
  1282   Addsimprocs [ab_group_add_cancel.sum_conv, ab_group_add_cancel.rel_conv];
  1283 *}
  1284 
  1285 code_modulename SML
  1286   Groups Arith
  1287 
  1288 code_modulename OCaml
  1289   Groups Arith
  1290 
  1291 code_modulename Haskell
  1292   Groups Arith
  1293 
  1294 end