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