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