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