src/HOL/Groups.thy
 author haftmann Fri Jun 11 17:14:02 2010 +0200 (2010-06-11) changeset 37407 61dd8c145da7 parent 36977 71c8973a604b child 37884 314a88278715 permissions -rw-r--r--
declare lex_prod_def [code del]
     1 (*  Title:   HOL/Groups.thy

     2     Author:  Gertrud Bauer, Steven Obua, Lawrence C Paulson, Markus Wenzel, Jeremy Avigad

     3 *)

     4

     5 header {* Groups, also combined with orderings *}

     6

     7 theory Groups

     8 imports Orderings

     9 uses ("~~/src/Provers/Arith/abel_cancel.ML")

    10 begin

    11

    12 subsection {* Fact collections *}

    13

    14 ML {*

    15 structure Ac_Simps = Named_Thms(

    16   val name = "ac_simps"

    17   val description = "associativity and commutativity simplification rules"

    18 )

    19 *}

    20

    21 setup Ac_Simps.setup

    22

    23 text{* The rewrites accumulated in @{text algebra_simps} deal with the

    24 classical algebraic structures of groups, rings and family. They simplify

    25 terms by multiplying everything out (in case of a ring) and bringing sums and

    26 products into a canonical form (by ordered rewriting). As a result it decides

    27 group and ring equalities but also helps with inequalities.

    28

    29 Of course it also works for fields, but it knows nothing about multiplicative

    30 inverses or division. This is catered for by @{text field_simps}. *}

    31

    32 ML {*

    33 structure Algebra_Simps = Named_Thms(

    34   val name = "algebra_simps"

    35   val description = "algebra simplification rules"

    36 )

    37 *}

    38

    39 setup Algebra_Simps.setup

    40

    41 text{* Lemmas @{text field_simps} multiply with denominators in (in)equations

    42 if they can be proved to be non-zero (for equations) or positive/negative

    43 (for inequations). Can be too aggressive and is therefore separate from the

    44 more benign @{text algebra_simps}. *}

    45

    46 ML {*

    47 structure Field_Simps = Named_Thms(

    48   val name = "field_simps"

    49   val description = "algebra simplification rules for fields"

    50 )

    51 *}

    52

    53 setup Field_Simps.setup

    54

    55

    56 subsection {* Abstract structures *}

    57

    58 text {*

    59   These locales provide basic structures for interpretation into

    60   bigger structures;  extensions require careful thinking, otherwise

    61   undesired effects may occur due to interpretation.

    62 *}

    63

    64 locale semigroup =

    65   fixes f :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "*" 70)

    66   assumes assoc [ac_simps]: "a * b * c = a * (b * c)"

    67

    68 locale abel_semigroup = semigroup +

    69   assumes commute [ac_simps]: "a * b = b * a"

    70 begin

    71

    72 lemma left_commute [ac_simps]:

    73   "b * (a * c) = a * (b * c)"

    74 proof -

    75   have "(b * a) * c = (a * b) * c"

    76     by (simp only: commute)

    77   then show ?thesis

    78     by (simp only: assoc)

    79 qed

    80

    81 end

    82

    83 locale monoid = semigroup +

    84   fixes z :: 'a ("1")

    85   assumes left_neutral [simp]: "1 * a = a"

    86   assumes right_neutral [simp]: "a * 1 = a"

    87

    88 locale comm_monoid = abel_semigroup +

    89   fixes z :: 'a ("1")

    90   assumes comm_neutral: "a * 1 = a"

    91

    92 sublocale comm_monoid < monoid proof

    93 qed (simp_all add: commute comm_neutral)

    94

    95

    96 subsection {* Generic operations *}

    97

    98 class zero =

    99   fixes zero :: 'a  ("0")

   100

   101 class one =

   102   fixes one  :: 'a  ("1")

   103

   104 hide_const (open) zero one

   105

   106 syntax

   107   "_index1"  :: index    ("\<^sub>1")

   108 translations

   109   (index) "\<^sub>1" => (index) "\<^bsub>\<struct>\<^esub>"

   110

   111 lemma Let_0 [simp]: "Let 0 f = f 0"

   112   unfolding Let_def ..

   113

   114 lemma Let_1 [simp]: "Let 1 f = f 1"

   115   unfolding Let_def ..

   116

   117 setup {*

   118   Reorient_Proc.add

   119     (fn Const(@{const_name Groups.zero}, _) => true

   120       | Const(@{const_name Groups.one}, _) => true

   121       | _ => false)

   122 *}

   123

   124 simproc_setup reorient_zero ("0 = x") = Reorient_Proc.proc

   125 simproc_setup reorient_one ("1 = x") = Reorient_Proc.proc

   126

   127 typed_print_translation {*

   128 let

   129   fun tr' c = (c, fn show_sorts => fn T => fn ts =>

   130     if (not o null) ts orelse T = dummyT

   131       orelse not (! show_types) andalso can Term.dest_Type T

   132     then raise Match

   133     else Syntax.const Syntax.constrainC $Syntax.const c$ Syntax.term_of_typ show_sorts T);

   134 in map tr' [@{const_syntax Groups.one}, @{const_syntax Groups.zero}] end;

   135 *} -- {* show types that are presumably too general *}

   136

   137 class plus =

   138   fixes plus :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "+" 65)

   139

   140 class minus =

   141   fixes minus :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "-" 65)

   142

   143 class uminus =

   144   fixes uminus :: "'a \<Rightarrow> 'a"  ("- _" [81] 80)

   145

   146 class times =

   147   fixes times :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "*" 70)

   148

   149 use "~~/src/Provers/Arith/abel_cancel.ML"

   150

   151

   152 subsection {* Semigroups and Monoids *}

   153

   154 class semigroup_add = plus +

   155   assumes add_assoc [algebra_simps, field_simps]: "(a + b) + c = a + (b + c)"

   156

   157 sublocale semigroup_add < add!: semigroup plus proof

   158 qed (fact add_assoc)

   159

   160 class ab_semigroup_add = semigroup_add +

   161   assumes add_commute [algebra_simps, field_simps]: "a + b = b + a"

   162

   163 sublocale ab_semigroup_add < add!: abel_semigroup plus proof

   164 qed (fact add_commute)

   165

   166 context ab_semigroup_add

   167 begin

   168

   169 lemmas add_left_commute [algebra_simps, field_simps] = add.left_commute

   170

   171 theorems add_ac = add_assoc add_commute add_left_commute

   172

   173 end

   174

   175 theorems add_ac = add_assoc add_commute add_left_commute

   176

   177 class semigroup_mult = times +

   178   assumes mult_assoc [algebra_simps, field_simps]: "(a * b) * c = a * (b * c)"

   179

   180 sublocale semigroup_mult < mult!: semigroup times proof

   181 qed (fact mult_assoc)

   182

   183 class ab_semigroup_mult = semigroup_mult +

   184   assumes mult_commute [algebra_simps, field_simps]: "a * b = b * a"

   185

   186 sublocale ab_semigroup_mult < mult!: abel_semigroup times proof

   187 qed (fact mult_commute)

   188

   189 context ab_semigroup_mult

   190 begin

   191

   192 lemmas mult_left_commute [algebra_simps, field_simps] = mult.left_commute

   193

   194 theorems mult_ac = mult_assoc mult_commute mult_left_commute

   195

   196 end

   197

   198 theorems mult_ac = mult_assoc mult_commute mult_left_commute

   199

   200 class monoid_add = zero + semigroup_add +

   201   assumes add_0_left: "0 + a = a"

   202     and add_0_right: "a + 0 = a"

   203

   204 sublocale monoid_add < add!: monoid plus 0 proof

   205 qed (fact add_0_left add_0_right)+

   206

   207 lemma zero_reorient: "0 = x \<longleftrightarrow> x = 0"

   208 by (rule eq_commute)

   209

   210 class comm_monoid_add = zero + ab_semigroup_add +

   211   assumes add_0: "0 + a = a"

   212

   213 sublocale comm_monoid_add < add!: comm_monoid plus 0 proof

   214 qed (insert add_0, simp add: ac_simps)

   215

   216 subclass (in comm_monoid_add) monoid_add proof

   217 qed (fact add.left_neutral add.right_neutral)+

   218

   219 class monoid_mult = one + semigroup_mult +

   220   assumes mult_1_left: "1 * a  = a"

   221     and mult_1_right: "a * 1 = a"

   222

   223 sublocale monoid_mult < mult!: monoid times 1 proof

   224 qed (fact mult_1_left mult_1_right)+

   225

   226 lemma one_reorient: "1 = x \<longleftrightarrow> x = 1"

   227 by (rule eq_commute)

   228

   229 class comm_monoid_mult = one + ab_semigroup_mult +

   230   assumes mult_1: "1 * a = a"

   231

   232 sublocale comm_monoid_mult < mult!: comm_monoid times 1 proof

   233 qed (insert mult_1, simp add: ac_simps)

   234

   235 subclass (in comm_monoid_mult) monoid_mult proof

   236 qed (fact mult.left_neutral mult.right_neutral)+

   237

   238 class cancel_semigroup_add = semigroup_add +

   239   assumes add_left_imp_eq: "a + b = a + c \<Longrightarrow> b = c"

   240   assumes add_right_imp_eq: "b + a = c + a \<Longrightarrow> b = c"

   241 begin

   242

   243 lemma add_left_cancel [simp]:

   244   "a + b = a + c \<longleftrightarrow> b = c"

   245 by (blast dest: add_left_imp_eq)

   246

   247 lemma add_right_cancel [simp]:

   248   "b + a = c + a \<longleftrightarrow> b = c"

   249 by (blast dest: add_right_imp_eq)

   250

   251 end

   252

   253 class cancel_ab_semigroup_add = ab_semigroup_add +

   254   assumes add_imp_eq: "a + b = a + c \<Longrightarrow> b = c"

   255 begin

   256

   257 subclass cancel_semigroup_add

   258 proof

   259   fix a b c :: 'a

   260   assume "a + b = a + c"

   261   then show "b = c" by (rule add_imp_eq)

   262 next

   263   fix a b c :: 'a

   264   assume "b + a = c + a"

   265   then have "a + b = a + c" by (simp only: add_commute)

   266   then show "b = c" by (rule add_imp_eq)

   267 qed

   268

   269 end

   270

   271 class cancel_comm_monoid_add = cancel_ab_semigroup_add + comm_monoid_add

   272

   273

   274 subsection {* Groups *}

   275

   276 class group_add = minus + uminus + monoid_add +

   277   assumes left_minus [simp]: "- a + a = 0"

   278   assumes diff_minus: "a - b = a + (- b)"

   279 begin

   280

   281 lemma minus_unique:

   282   assumes "a + b = 0" shows "- a = b"

   283 proof -

   284   have "- a = - a + (a + b)" using assms by simp

   285   also have "\<dots> = b" by (simp add: add_assoc [symmetric])

   286   finally show ?thesis .

   287 qed

   288

   289 lemmas equals_zero_I = minus_unique (* legacy name *)

   290

   291 lemma minus_zero [simp]: "- 0 = 0"

   292 proof -

   293   have "0 + 0 = 0" by (rule add_0_right)

   294   thus "- 0 = 0" by (rule minus_unique)

   295 qed

   296

   297 lemma minus_minus [simp]: "- (- a) = a"

   298 proof -

   299   have "- a + a = 0" by (rule left_minus)

   300   thus "- (- a) = a" by (rule minus_unique)

   301 qed

   302

   303 lemma right_minus [simp]: "a + - a = 0"

   304 proof -

   305   have "a + - a = - (- a) + - a" by simp

   306   also have "\<dots> = 0" by (rule left_minus)

   307   finally show ?thesis .

   308 qed

   309

   310 lemma minus_add_cancel: "- a + (a + b) = b"

   311 by (simp add: add_assoc [symmetric])

   312

   313 lemma add_minus_cancel: "a + (- a + b) = b"

   314 by (simp add: add_assoc [symmetric])

   315

   316 lemma minus_add: "- (a + b) = - b + - a"

   317 proof -

   318   have "(a + b) + (- b + - a) = 0"

   319     by (simp add: add_assoc add_minus_cancel)

   320   thus "- (a + b) = - b + - a"

   321     by (rule minus_unique)

   322 qed

   323

   324 lemma right_minus_eq: "a - b = 0 \<longleftrightarrow> a = b"

   325 proof

   326   assume "a - b = 0"

   327   have "a = (a - b) + b" by (simp add:diff_minus add_assoc)

   328   also have "\<dots> = b" using a - b = 0 by simp

   329   finally show "a = b" .

   330 next

   331   assume "a = b" thus "a - b = 0" by (simp add: diff_minus)

   332 qed

   333

   334 lemma diff_self [simp]: "a - a = 0"

   335 by (simp add: diff_minus)

   336

   337 lemma diff_0 [simp]: "0 - a = - a"

   338 by (simp add: diff_minus)

   339

   340 lemma diff_0_right [simp]: "a - 0 = a"

   341 by (simp add: diff_minus)

   342

   343 lemma diff_minus_eq_add [simp]: "a - - b = a + b"

   344 by (simp add: diff_minus)

   345

   346 lemma neg_equal_iff_equal [simp]:

   347   "- a = - b \<longleftrightarrow> a = b"

   348 proof

   349   assume "- a = - b"

   350   hence "- (- a) = - (- b)" by simp

   351   thus "a = b" by simp

   352 next

   353   assume "a = b"

   354   thus "- a = - b" by simp

   355 qed

   356

   357 lemma neg_equal_0_iff_equal [simp]:

   358   "- a = 0 \<longleftrightarrow> a = 0"

   359 by (subst neg_equal_iff_equal [symmetric], simp)

   360

   361 lemma neg_0_equal_iff_equal [simp]:

   362   "0 = - a \<longleftrightarrow> 0 = a"

   363 by (subst neg_equal_iff_equal [symmetric], simp)

   364

   365 text{*The next two equations can make the simplifier loop!*}

   366

   367 lemma equation_minus_iff:

   368   "a = - b \<longleftrightarrow> b = - a"

   369 proof -

   370   have "- (- a) = - b \<longleftrightarrow> - a = b" by (rule neg_equal_iff_equal)

   371   thus ?thesis by (simp add: eq_commute)

   372 qed

   373

   374 lemma minus_equation_iff:

   375   "- a = b \<longleftrightarrow> - b = a"

   376 proof -

   377   have "- a = - (- b) \<longleftrightarrow> a = -b" by (rule neg_equal_iff_equal)

   378   thus ?thesis by (simp add: eq_commute)

   379 qed

   380

   381 lemma diff_add_cancel: "a - b + b = a"

   382 by (simp add: diff_minus add_assoc)

   383

   384 lemma add_diff_cancel: "a + b - b = a"

   385 by (simp add: diff_minus add_assoc)

   386

   387 declare diff_minus[symmetric, algebra_simps, field_simps]

   388

   389 lemma eq_neg_iff_add_eq_0: "a = - b \<longleftrightarrow> a + b = 0"

   390 proof

   391   assume "a = - b" then show "a + b = 0" by simp

   392 next

   393   assume "a + b = 0"

   394   moreover have "a + (b + - b) = (a + b) + - b"

   395     by (simp only: add_assoc)

   396   ultimately show "a = - b" by simp

   397 qed

   398

   399 end

   400

   401 class ab_group_add = minus + uminus + comm_monoid_add +

   402   assumes ab_left_minus: "- a + a = 0"

   403   assumes ab_diff_minus: "a - b = a + (- b)"

   404 begin

   405

   406 subclass group_add

   407   proof qed (simp_all add: ab_left_minus ab_diff_minus)

   408

   409 subclass cancel_comm_monoid_add

   410 proof

   411   fix a b c :: 'a

   412   assume "a + b = a + c"

   413   then have "- a + a + b = - a + a + c"

   414     unfolding add_assoc by simp

   415   then show "b = c" by simp

   416 qed

   417

   418 lemma uminus_add_conv_diff[algebra_simps, field_simps]:

   419   "- a + b = b - a"

   420 by (simp add:diff_minus add_commute)

   421

   422 lemma minus_add_distrib [simp]:

   423   "- (a + b) = - a + - b"

   424 by (rule minus_unique) (simp add: add_ac)

   425

   426 lemma minus_diff_eq [simp]:

   427   "- (a - b) = b - a"

   428 by (simp add: diff_minus add_commute)

   429

   430 lemma add_diff_eq[algebra_simps, field_simps]: "a + (b - c) = (a + b) - c"

   431 by (simp add: diff_minus add_ac)

   432

   433 lemma diff_add_eq[algebra_simps, field_simps]: "(a - b) + c = (a + c) - b"

   434 by (simp add: diff_minus add_ac)

   435

   436 lemma diff_eq_eq[algebra_simps, field_simps]: "a - b = c \<longleftrightarrow> a = c + b"

   437 by (auto simp add: diff_minus add_assoc)

   438

   439 lemma eq_diff_eq[algebra_simps, field_simps]: "a = c - b \<longleftrightarrow> a + b = c"

   440 by (auto simp add: diff_minus add_assoc)

   441

   442 lemma diff_diff_eq[algebra_simps, field_simps]: "(a - b) - c = a - (b + c)"

   443 by (simp add: diff_minus add_ac)

   444

   445 lemma diff_diff_eq2[algebra_simps, field_simps]: "a - (b - c) = (a + c) - b"

   446 by (simp add: diff_minus add_ac)

   447

   448 lemma eq_iff_diff_eq_0: "a = b \<longleftrightarrow> a - b = 0"

   449 by (simp add: algebra_simps)

   450

   451 (* FIXME: duplicates right_minus_eq from class group_add *)

   452 (* but only this one is declared as a simp rule. *)

   453 lemma diff_eq_0_iff_eq [simp, no_atp]: "a - b = 0 \<longleftrightarrow> a = b"

   454 by (simp add: algebra_simps)

   455

   456 end

   457

   458 subsection {* (Partially) Ordered Groups *}

   459

   460 text {*

   461   The theory of partially ordered groups is taken from the books:

   462   \begin{itemize}

   463   \item \emph{Lattice Theory} by Garret Birkhoff, American Mathematical Society 1979

   464   \item \emph{Partially Ordered Algebraic Systems}, Pergamon Press 1963

   465   \end{itemize}

   466   Most of the used notions can also be looked up in

   467   \begin{itemize}

   468   \item \url{http://www.mathworld.com} by Eric Weisstein et. al.

   469   \item \emph{Algebra I} by van der Waerden, Springer.

   470   \end{itemize}

   471 *}

   472

   473 class ordered_ab_semigroup_add = order + ab_semigroup_add +

   474   assumes add_left_mono: "a \<le> b \<Longrightarrow> c + a \<le> c + b"

   475 begin

   476

   477 lemma add_right_mono:

   478   "a \<le> b \<Longrightarrow> a + c \<le> b + c"

   479 by (simp add: add_commute [of _ c] add_left_mono)

   480

   481 text {* non-strict, in both arguments *}

   482 lemma add_mono:

   483   "a \<le> b \<Longrightarrow> c \<le> d \<Longrightarrow> a + c \<le> b + d"

   484   apply (erule add_right_mono [THEN order_trans])

   485   apply (simp add: add_commute add_left_mono)

   486   done

   487

   488 end

   489

   490 class ordered_cancel_ab_semigroup_add =

   491   ordered_ab_semigroup_add + cancel_ab_semigroup_add

   492 begin

   493

   494 lemma add_strict_left_mono:

   495   "a < b \<Longrightarrow> c + a < c + b"

   496 by (auto simp add: less_le add_left_mono)

   497

   498 lemma add_strict_right_mono:

   499   "a < b \<Longrightarrow> a + c < b + c"

   500 by (simp add: add_commute [of _ c] add_strict_left_mono)

   501

   502 text{*Strict monotonicity in both arguments*}

   503 lemma add_strict_mono:

   504   "a < b \<Longrightarrow> c < d \<Longrightarrow> a + c < b + d"

   505 apply (erule add_strict_right_mono [THEN less_trans])

   506 apply (erule add_strict_left_mono)

   507 done

   508

   509 lemma add_less_le_mono:

   510   "a < b \<Longrightarrow> c \<le> d \<Longrightarrow> a + c < b + d"

   511 apply (erule add_strict_right_mono [THEN less_le_trans])

   512 apply (erule add_left_mono)

   513 done

   514

   515 lemma add_le_less_mono:

   516   "a \<le> b \<Longrightarrow> c < d \<Longrightarrow> a + c < b + d"

   517 apply (erule add_right_mono [THEN le_less_trans])

   518 apply (erule add_strict_left_mono)

   519 done

   520

   521 end

   522

   523 class ordered_ab_semigroup_add_imp_le =

   524   ordered_cancel_ab_semigroup_add +

   525   assumes add_le_imp_le_left: "c + a \<le> c + b \<Longrightarrow> a \<le> b"

   526 begin

   527

   528 lemma add_less_imp_less_left:

   529   assumes less: "c + a < c + b" shows "a < b"

   530 proof -

   531   from less have le: "c + a <= c + b" by (simp add: order_le_less)

   532   have "a <= b"

   533     apply (insert le)

   534     apply (drule add_le_imp_le_left)

   535     by (insert le, drule add_le_imp_le_left, assumption)

   536   moreover have "a \<noteq> b"

   537   proof (rule ccontr)

   538     assume "~(a \<noteq> b)"

   539     then have "a = b" by simp

   540     then have "c + a = c + b" by simp

   541     with less show "False"by simp

   542   qed

   543   ultimately show "a < b" by (simp add: order_le_less)

   544 qed

   545

   546 lemma add_less_imp_less_right:

   547   "a + c < b + c \<Longrightarrow> a < b"

   548 apply (rule add_less_imp_less_left [of c])

   549 apply (simp add: add_commute)

   550 done

   551

   552 lemma add_less_cancel_left [simp]:

   553   "c + a < c + b \<longleftrightarrow> a < b"

   554 by (blast intro: add_less_imp_less_left add_strict_left_mono)

   555

   556 lemma add_less_cancel_right [simp]:

   557   "a + c < b + c \<longleftrightarrow> a < b"

   558 by (blast intro: add_less_imp_less_right add_strict_right_mono)

   559

   560 lemma add_le_cancel_left [simp]:

   561   "c + a \<le> c + b \<longleftrightarrow> a \<le> b"

   562 by (auto, drule add_le_imp_le_left, simp_all add: add_left_mono)

   563

   564 lemma add_le_cancel_right [simp]:

   565   "a + c \<le> b + c \<longleftrightarrow> a \<le> b"

   566 by (simp add: add_commute [of a c] add_commute [of b c])

   567

   568 lemma add_le_imp_le_right:

   569   "a + c \<le> b + c \<Longrightarrow> a \<le> b"

   570 by simp

   571

   572 lemma max_add_distrib_left:

   573   "max x y + z = max (x + z) (y + z)"

   574   unfolding max_def by auto

   575

   576 lemma min_add_distrib_left:

   577   "min x y + z = min (x + z) (y + z)"

   578   unfolding min_def by auto

   579

   580 end

   581

   582 subsection {* Support for reasoning about signs *}

   583

   584 class ordered_comm_monoid_add =

   585   ordered_cancel_ab_semigroup_add + comm_monoid_add

   586 begin

   587

   588 lemma add_pos_nonneg:

   589   assumes "0 < a" and "0 \<le> b" shows "0 < a + b"

   590 proof -

   591   have "0 + 0 < a + b"

   592     using assms by (rule add_less_le_mono)

   593   then show ?thesis by simp

   594 qed

   595

   596 lemma add_pos_pos:

   597   assumes "0 < a" and "0 < b" shows "0 < a + b"

   598 by (rule add_pos_nonneg) (insert assms, auto)

   599

   600 lemma add_nonneg_pos:

   601   assumes "0 \<le> a" and "0 < b" shows "0 < a + b"

   602 proof -

   603   have "0 + 0 < a + b"

   604     using assms by (rule add_le_less_mono)

   605   then show ?thesis by simp

   606 qed

   607

   608 lemma add_nonneg_nonneg [simp]:

   609   assumes "0 \<le> a" and "0 \<le> b" shows "0 \<le> a + b"

   610 proof -

   611   have "0 + 0 \<le> a + b"

   612     using assms by (rule add_mono)

   613   then show ?thesis by simp

   614 qed

   615

   616 lemma add_neg_nonpos:

   617   assumes "a < 0" and "b \<le> 0" shows "a + b < 0"

   618 proof -

   619   have "a + b < 0 + 0"

   620     using assms by (rule add_less_le_mono)

   621   then show ?thesis by simp

   622 qed

   623

   624 lemma add_neg_neg:

   625   assumes "a < 0" and "b < 0" shows "a + b < 0"

   626 by (rule add_neg_nonpos) (insert assms, auto)

   627

   628 lemma add_nonpos_neg:

   629   assumes "a \<le> 0" and "b < 0" shows "a + b < 0"

   630 proof -

   631   have "a + b < 0 + 0"

   632     using assms by (rule add_le_less_mono)

   633   then show ?thesis by simp

   634 qed

   635

   636 lemma add_nonpos_nonpos:

   637   assumes "a \<le> 0" and "b \<le> 0" shows "a + b \<le> 0"

   638 proof -

   639   have "a + b \<le> 0 + 0"

   640     using assms by (rule add_mono)

   641   then show ?thesis by simp

   642 qed

   643

   644 lemmas add_sign_intros =

   645   add_pos_nonneg add_pos_pos add_nonneg_pos add_nonneg_nonneg

   646   add_neg_nonpos add_neg_neg add_nonpos_neg add_nonpos_nonpos

   647

   648 lemma add_nonneg_eq_0_iff:

   649   assumes x: "0 \<le> x" and y: "0 \<le> y"

   650   shows "x + y = 0 \<longleftrightarrow> x = 0 \<and> y = 0"

   651 proof (intro iffI conjI)

   652   have "x = x + 0" by simp

   653   also have "x + 0 \<le> x + y" using y by (rule add_left_mono)

   654   also assume "x + y = 0"

   655   also have "0 \<le> x" using x .

   656   finally show "x = 0" .

   657 next

   658   have "y = 0 + y" by simp

   659   also have "0 + y \<le> x + y" using x by (rule add_right_mono)

   660   also assume "x + y = 0"

   661   also have "0 \<le> y" using y .

   662   finally show "y = 0" .

   663 next

   664   assume "x = 0 \<and> y = 0"

   665   then show "x + y = 0" by simp

   666 qed

   667

   668 end

   669

   670 class ordered_ab_group_add =

   671   ab_group_add + ordered_ab_semigroup_add

   672 begin

   673

   674 subclass ordered_cancel_ab_semigroup_add ..

   675

   676 subclass ordered_ab_semigroup_add_imp_le

   677 proof

   678   fix a b c :: 'a

   679   assume "c + a \<le> c + b"

   680   hence "(-c) + (c + a) \<le> (-c) + (c + b)" by (rule add_left_mono)

   681   hence "((-c) + c) + a \<le> ((-c) + c) + b" by (simp only: add_assoc)

   682   thus "a \<le> b" by simp

   683 qed

   684

   685 subclass ordered_comm_monoid_add ..

   686

   687 lemma max_diff_distrib_left:

   688   shows "max x y - z = max (x - z) (y - z)"

   689 by (simp add: diff_minus, rule max_add_distrib_left)

   690

   691 lemma min_diff_distrib_left:

   692   shows "min x y - z = min (x - z) (y - z)"

   693 by (simp add: diff_minus, rule min_add_distrib_left)

   694

   695 lemma le_imp_neg_le:

   696   assumes "a \<le> b" shows "-b \<le> -a"

   697 proof -

   698   have "-a+a \<le> -a+b" using a \<le> b by (rule add_left_mono)

   699   hence "0 \<le> -a+b" by simp

   700   hence "0 + (-b) \<le> (-a + b) + (-b)" by (rule add_right_mono)

   701   thus ?thesis by (simp add: add_assoc)

   702 qed

   703

   704 lemma neg_le_iff_le [simp]: "- b \<le> - a \<longleftrightarrow> a \<le> b"

   705 proof

   706   assume "- b \<le> - a"

   707   hence "- (- a) \<le> - (- b)" by (rule le_imp_neg_le)

   708   thus "a\<le>b" by simp

   709 next

   710   assume "a\<le>b"

   711   thus "-b \<le> -a" by (rule le_imp_neg_le)

   712 qed

   713

   714 lemma neg_le_0_iff_le [simp]: "- a \<le> 0 \<longleftrightarrow> 0 \<le> a"

   715 by (subst neg_le_iff_le [symmetric], simp)

   716

   717 lemma neg_0_le_iff_le [simp]: "0 \<le> - a \<longleftrightarrow> a \<le> 0"

   718 by (subst neg_le_iff_le [symmetric], simp)

   719

   720 lemma neg_less_iff_less [simp]: "- b < - a \<longleftrightarrow> a < b"

   721 by (force simp add: less_le)

   722

   723 lemma neg_less_0_iff_less [simp]: "- a < 0 \<longleftrightarrow> 0 < a"

   724 by (subst neg_less_iff_less [symmetric], simp)

   725

   726 lemma neg_0_less_iff_less [simp]: "0 < - a \<longleftrightarrow> a < 0"

   727 by (subst neg_less_iff_less [symmetric], simp)

   728

   729 text{*The next several equations can make the simplifier loop!*}

   730

   731 lemma less_minus_iff: "a < - b \<longleftrightarrow> b < - a"

   732 proof -

   733   have "(- (-a) < - b) = (b < - a)" by (rule neg_less_iff_less)

   734   thus ?thesis by simp

   735 qed

   736

   737 lemma minus_less_iff: "- a < b \<longleftrightarrow> - b < a"

   738 proof -

   739   have "(- a < - (-b)) = (- b < a)" by (rule neg_less_iff_less)

   740   thus ?thesis by simp

   741 qed

   742

   743 lemma le_minus_iff: "a \<le> - b \<longleftrightarrow> b \<le> - a"

   744 proof -

   745   have mm: "!! a (b::'a). (-(-a)) < -b \<Longrightarrow> -(-b) < -a" by (simp only: minus_less_iff)

   746   have "(- (- a) <= -b) = (b <= - a)"

   747     apply (auto simp only: le_less)

   748     apply (drule mm)

   749     apply (simp_all)

   750     apply (drule mm[simplified], assumption)

   751     done

   752   then show ?thesis by simp

   753 qed

   754

   755 lemma minus_le_iff: "- a \<le> b \<longleftrightarrow> - b \<le> a"

   756 by (auto simp add: le_less minus_less_iff)

   757

   758 lemma less_iff_diff_less_0: "a < b \<longleftrightarrow> a - b < 0"

   759 proof -

   760   have  "(a < b) = (a + (- b) < b + (-b))"

   761     by (simp only: add_less_cancel_right)

   762   also have "... =  (a - b < 0)" by (simp add: diff_minus)

   763   finally show ?thesis .

   764 qed

   765

   766 lemma diff_less_eq[algebra_simps, field_simps]: "a - b < c \<longleftrightarrow> a < c + b"

   767 apply (subst less_iff_diff_less_0 [of a])

   768 apply (rule less_iff_diff_less_0 [of _ c, THEN ssubst])

   769 apply (simp add: diff_minus add_ac)

   770 done

   771

   772 lemma less_diff_eq[algebra_simps, field_simps]: "a < c - b \<longleftrightarrow> a + b < c"

   773 apply (subst less_iff_diff_less_0 [of "a + b"])

   774 apply (subst less_iff_diff_less_0 [of a])

   775 apply (simp add: diff_minus add_ac)

   776 done

   777

   778 lemma diff_le_eq[algebra_simps, field_simps]: "a - b \<le> c \<longleftrightarrow> a \<le> c + b"

   779 by (auto simp add: le_less diff_less_eq diff_add_cancel add_diff_cancel)

   780

   781 lemma le_diff_eq[algebra_simps, field_simps]: "a \<le> c - b \<longleftrightarrow> a + b \<le> c"

   782 by (auto simp add: le_less less_diff_eq diff_add_cancel add_diff_cancel)

   783

   784 lemma le_iff_diff_le_0: "a \<le> b \<longleftrightarrow> a - b \<le> 0"

   785 by (simp add: algebra_simps)

   786

   787 end

   788

   789 class linordered_ab_semigroup_add =

   790   linorder + ordered_ab_semigroup_add

   791

   792 class linordered_cancel_ab_semigroup_add =

   793   linorder + ordered_cancel_ab_semigroup_add

   794 begin

   795

   796 subclass linordered_ab_semigroup_add ..

   797

   798 subclass ordered_ab_semigroup_add_imp_le

   799 proof

   800   fix a b c :: 'a

   801   assume le: "c + a <= c + b"

   802   show "a <= b"

   803   proof (rule ccontr)

   804     assume w: "~ a \<le> b"

   805     hence "b <= a" by (simp add: linorder_not_le)

   806     hence le2: "c + b <= c + a" by (rule add_left_mono)

   807     have "a = b"

   808       apply (insert le)

   809       apply (insert le2)

   810       apply (drule antisym, simp_all)

   811       done

   812     with w show False

   813       by (simp add: linorder_not_le [symmetric])

   814   qed

   815 qed

   816

   817 end

   818

   819 class linordered_ab_group_add = linorder + ordered_ab_group_add

   820 begin

   821

   822 subclass linordered_cancel_ab_semigroup_add ..

   823

   824 lemma neg_less_eq_nonneg [simp]:

   825   "- a \<le> a \<longleftrightarrow> 0 \<le> a"

   826 proof

   827   assume A: "- a \<le> a" show "0 \<le> a"

   828   proof (rule classical)

   829     assume "\<not> 0 \<le> a"

   830     then have "a < 0" by auto

   831     with A have "- a < 0" by (rule le_less_trans)

   832     then show ?thesis by auto

   833   qed

   834 next

   835   assume A: "0 \<le> a" show "- a \<le> a"

   836   proof (rule order_trans)

   837     show "- a \<le> 0" using A by (simp add: minus_le_iff)

   838   next

   839     show "0 \<le> a" using A .

   840   qed

   841 qed

   842

   843 lemma neg_less_nonneg [simp]:

   844   "- a < a \<longleftrightarrow> 0 < a"

   845 proof

   846   assume A: "- a < a" show "0 < a"

   847   proof (rule classical)

   848     assume "\<not> 0 < a"

   849     then have "a \<le> 0" by auto

   850     with A have "- a < 0" by (rule less_le_trans)

   851     then show ?thesis by auto

   852   qed

   853 next

   854   assume A: "0 < a" show "- a < a"

   855   proof (rule less_trans)

   856     show "- a < 0" using A by (simp add: minus_le_iff)

   857   next

   858     show "0 < a" using A .

   859   qed

   860 qed

   861

   862 lemma less_eq_neg_nonpos [simp]:

   863   "a \<le> - a \<longleftrightarrow> a \<le> 0"

   864 proof

   865   assume A: "a \<le> - a" show "a \<le> 0"

   866   proof (rule classical)

   867     assume "\<not> a \<le> 0"

   868     then have "0 < a" by auto

   869     then have "0 < - a" using A by (rule less_le_trans)

   870     then show ?thesis by auto

   871   qed

   872 next

   873   assume A: "a \<le> 0" show "a \<le> - a"

   874   proof (rule order_trans)

   875     show "0 \<le> - a" using A by (simp add: minus_le_iff)

   876   next

   877     show "a \<le> 0" using A .

   878   qed

   879 qed

   880

   881 lemma equal_neg_zero [simp]:

   882   "a = - a \<longleftrightarrow> a = 0"

   883 proof

   884   assume "a = 0" then show "a = - a" by simp

   885 next

   886   assume A: "a = - a" show "a = 0"

   887   proof (cases "0 \<le> a")

   888     case True with A have "0 \<le> - a" by auto

   889     with le_minus_iff have "a \<le> 0" by simp

   890     with True show ?thesis by (auto intro: order_trans)

   891   next

   892     case False then have B: "a \<le> 0" by auto

   893     with A have "- a \<le> 0" by auto

   894     with B show ?thesis by (auto intro: order_trans)

   895   qed

   896 qed

   897

   898 lemma neg_equal_zero [simp]:

   899   "- a = a \<longleftrightarrow> a = 0"

   900   by (auto dest: sym)

   901

   902 lemma double_zero [simp]:

   903   "a + a = 0 \<longleftrightarrow> a = 0"

   904 proof

   905   assume assm: "a + a = 0"

   906   then have a: "- a = a" by (rule minus_unique)

   907   then show "a = 0" by (simp only: neg_equal_zero)

   908 qed simp

   909

   910 lemma double_zero_sym [simp]:

   911   "0 = a + a \<longleftrightarrow> a = 0"

   912   by (rule, drule sym) simp_all

   913

   914 lemma zero_less_double_add_iff_zero_less_single_add [simp]:

   915   "0 < a + a \<longleftrightarrow> 0 < a"

   916 proof

   917   assume "0 < a + a"

   918   then have "0 - a < a" by (simp only: diff_less_eq)

   919   then have "- a < a" by simp

   920   then show "0 < a" by (simp only: neg_less_nonneg)

   921 next

   922   assume "0 < a"

   923   with this have "0 + 0 < a + a"

   924     by (rule add_strict_mono)

   925   then show "0 < a + a" by simp

   926 qed

   927

   928 lemma zero_le_double_add_iff_zero_le_single_add [simp]:

   929   "0 \<le> a + a \<longleftrightarrow> 0 \<le> a"

   930   by (auto simp add: le_less)

   931

   932 lemma double_add_less_zero_iff_single_add_less_zero [simp]:

   933   "a + a < 0 \<longleftrightarrow> a < 0"

   934 proof -

   935   have "\<not> a + a < 0 \<longleftrightarrow> \<not> a < 0"

   936     by (simp add: not_less)

   937   then show ?thesis by simp

   938 qed

   939

   940 lemma double_add_le_zero_iff_single_add_le_zero [simp]:

   941   "a + a \<le> 0 \<longleftrightarrow> a \<le> 0"

   942 proof -

   943   have "\<not> a + a \<le> 0 \<longleftrightarrow> \<not> a \<le> 0"

   944     by (simp add: not_le)

   945   then show ?thesis by simp

   946 qed

   947

   948 lemma le_minus_self_iff:

   949   "a \<le> - a \<longleftrightarrow> a \<le> 0"

   950 proof -

   951   from add_le_cancel_left [of "- a" "a + a" 0]

   952   have "a \<le> - a \<longleftrightarrow> a + a \<le> 0"

   953     by (simp add: add_assoc [symmetric])

   954   thus ?thesis by simp

   955 qed

   956

   957 lemma minus_le_self_iff:

   958   "- a \<le> a \<longleftrightarrow> 0 \<le> a"

   959 proof -

   960   from add_le_cancel_left [of "- a" 0 "a + a"]

   961   have "- a \<le> a \<longleftrightarrow> 0 \<le> a + a"

   962     by (simp add: add_assoc [symmetric])

   963   thus ?thesis by simp

   964 qed

   965

   966 lemma minus_max_eq_min:

   967   "- max x y = min (-x) (-y)"

   968   by (auto simp add: max_def min_def)

   969

   970 lemma minus_min_eq_max:

   971   "- min x y = max (-x) (-y)"

   972   by (auto simp add: max_def min_def)

   973

   974 end

   975

   976 context ordered_comm_monoid_add

   977 begin

   978

   979 lemma add_increasing:

   980   "0 \<le> a \<Longrightarrow> b \<le> c \<Longrightarrow> b \<le> a + c"

   981   by (insert add_mono [of 0 a b c], simp)

   982

   983 lemma add_increasing2:

   984   "0 \<le> c \<Longrightarrow> b \<le> a \<Longrightarrow> b \<le> a + c"

   985   by (simp add: add_increasing add_commute [of a])

   986

   987 lemma add_strict_increasing:

   988   "0 < a \<Longrightarrow> b \<le> c \<Longrightarrow> b < a + c"

   989   by (insert add_less_le_mono [of 0 a b c], simp)

   990

   991 lemma add_strict_increasing2:

   992   "0 \<le> a \<Longrightarrow> b < c \<Longrightarrow> b < a + c"

   993   by (insert add_le_less_mono [of 0 a b c], simp)

   994

   995 end

   996

   997 class abs =

   998   fixes abs :: "'a \<Rightarrow> 'a"

   999 begin

  1000

  1001 notation (xsymbols)

  1002   abs  ("\<bar>_\<bar>")

  1003

  1004 notation (HTML output)

  1005   abs  ("\<bar>_\<bar>")

  1006

  1007 end

  1008

  1009 class sgn =

  1010   fixes sgn :: "'a \<Rightarrow> 'a"

  1011

  1012 class abs_if = minus + uminus + ord + zero + abs +

  1013   assumes abs_if: "\<bar>a\<bar> = (if a < 0 then - a else a)"

  1014

  1015 class sgn_if = minus + uminus + zero + one + ord + sgn +

  1016   assumes sgn_if: "sgn x = (if x = 0 then 0 else if 0 < x then 1 else - 1)"

  1017 begin

  1018

  1019 lemma sgn0 [simp]: "sgn 0 = 0"

  1020   by (simp add:sgn_if)

  1021

  1022 end

  1023

  1024 class ordered_ab_group_add_abs = ordered_ab_group_add + abs +

  1025   assumes abs_ge_zero [simp]: "\<bar>a\<bar> \<ge> 0"

  1026     and abs_ge_self: "a \<le> \<bar>a\<bar>"

  1027     and abs_leI: "a \<le> b \<Longrightarrow> - a \<le> b \<Longrightarrow> \<bar>a\<bar> \<le> b"

  1028     and abs_minus_cancel [simp]: "\<bar>-a\<bar> = \<bar>a\<bar>"

  1029     and abs_triangle_ineq: "\<bar>a + b\<bar> \<le> \<bar>a\<bar> + \<bar>b\<bar>"

  1030 begin

  1031

  1032 lemma abs_minus_le_zero: "- \<bar>a\<bar> \<le> 0"

  1033   unfolding neg_le_0_iff_le by simp

  1034

  1035 lemma abs_of_nonneg [simp]:

  1036   assumes nonneg: "0 \<le> a" shows "\<bar>a\<bar> = a"

  1037 proof (rule antisym)

  1038   from nonneg le_imp_neg_le have "- a \<le> 0" by simp

  1039   from this nonneg have "- a \<le> a" by (rule order_trans)

  1040   then show "\<bar>a\<bar> \<le> a" by (auto intro: abs_leI)

  1041 qed (rule abs_ge_self)

  1042

  1043 lemma abs_idempotent [simp]: "\<bar>\<bar>a\<bar>\<bar> = \<bar>a\<bar>"

  1044 by (rule antisym)

  1045    (auto intro!: abs_ge_self abs_leI order_trans [of "- \<bar>a\<bar>" 0 "\<bar>a\<bar>"])

  1046

  1047 lemma abs_eq_0 [simp]: "\<bar>a\<bar> = 0 \<longleftrightarrow> a = 0"

  1048 proof -

  1049   have "\<bar>a\<bar> = 0 \<Longrightarrow> a = 0"

  1050   proof (rule antisym)

  1051     assume zero: "\<bar>a\<bar> = 0"

  1052     with abs_ge_self show "a \<le> 0" by auto

  1053     from zero have "\<bar>-a\<bar> = 0" by simp

  1054     with abs_ge_self [of "- a"] have "- a \<le> 0" by auto

  1055     with neg_le_0_iff_le show "0 \<le> a" by auto

  1056   qed

  1057   then show ?thesis by auto

  1058 qed

  1059

  1060 lemma abs_zero [simp]: "\<bar>0\<bar> = 0"

  1061 by simp

  1062

  1063 lemma abs_0_eq [simp, no_atp]: "0 = \<bar>a\<bar> \<longleftrightarrow> a = 0"

  1064 proof -

  1065   have "0 = \<bar>a\<bar> \<longleftrightarrow> \<bar>a\<bar> = 0" by (simp only: eq_ac)

  1066   thus ?thesis by simp

  1067 qed

  1068

  1069 lemma abs_le_zero_iff [simp]: "\<bar>a\<bar> \<le> 0 \<longleftrightarrow> a = 0"

  1070 proof

  1071   assume "\<bar>a\<bar> \<le> 0"

  1072   then have "\<bar>a\<bar> = 0" by (rule antisym) simp

  1073   thus "a = 0" by simp

  1074 next

  1075   assume "a = 0"

  1076   thus "\<bar>a\<bar> \<le> 0" by simp

  1077 qed

  1078

  1079 lemma zero_less_abs_iff [simp]: "0 < \<bar>a\<bar> \<longleftrightarrow> a \<noteq> 0"

  1080 by (simp add: less_le)

  1081

  1082 lemma abs_not_less_zero [simp]: "\<not> \<bar>a\<bar> < 0"

  1083 proof -

  1084   have a: "\<And>x y. x \<le> y \<Longrightarrow> \<not> y < x" by auto

  1085   show ?thesis by (simp add: a)

  1086 qed

  1087

  1088 lemma abs_ge_minus_self: "- a \<le> \<bar>a\<bar>"

  1089 proof -

  1090   have "- a \<le> \<bar>-a\<bar>" by (rule abs_ge_self)

  1091   then show ?thesis by simp

  1092 qed

  1093

  1094 lemma abs_minus_commute:

  1095   "\<bar>a - b\<bar> = \<bar>b - a\<bar>"

  1096 proof -

  1097   have "\<bar>a - b\<bar> = \<bar>- (a - b)\<bar>" by (simp only: abs_minus_cancel)

  1098   also have "... = \<bar>b - a\<bar>" by simp

  1099   finally show ?thesis .

  1100 qed

  1101

  1102 lemma abs_of_pos: "0 < a \<Longrightarrow> \<bar>a\<bar> = a"

  1103 by (rule abs_of_nonneg, rule less_imp_le)

  1104

  1105 lemma abs_of_nonpos [simp]:

  1106   assumes "a \<le> 0" shows "\<bar>a\<bar> = - a"

  1107 proof -

  1108   let ?b = "- a"

  1109   have "- ?b \<le> 0 \<Longrightarrow> \<bar>- ?b\<bar> = - (- ?b)"

  1110   unfolding abs_minus_cancel [of "?b"]

  1111   unfolding neg_le_0_iff_le [of "?b"]

  1112   unfolding minus_minus by (erule abs_of_nonneg)

  1113   then show ?thesis using assms by auto

  1114 qed

  1115

  1116 lemma abs_of_neg: "a < 0 \<Longrightarrow> \<bar>a\<bar> = - a"

  1117 by (rule abs_of_nonpos, rule less_imp_le)

  1118

  1119 lemma abs_le_D1: "\<bar>a\<bar> \<le> b \<Longrightarrow> a \<le> b"

  1120 by (insert abs_ge_self, blast intro: order_trans)

  1121

  1122 lemma abs_le_D2: "\<bar>a\<bar> \<le> b \<Longrightarrow> - a \<le> b"

  1123 by (insert abs_le_D1 [of "- a"], simp)

  1124

  1125 lemma abs_le_iff: "\<bar>a\<bar> \<le> b \<longleftrightarrow> a \<le> b \<and> - a \<le> b"

  1126 by (blast intro: abs_leI dest: abs_le_D1 abs_le_D2)

  1127

  1128 lemma abs_triangle_ineq2: "\<bar>a\<bar> - \<bar>b\<bar> \<le> \<bar>a - b\<bar>"

  1129 proof -

  1130   have "\<bar>a\<bar> = \<bar>b + (a - b)\<bar>"

  1131     by (simp add: algebra_simps add_diff_cancel)

  1132   then have "\<bar>a\<bar> \<le> \<bar>b\<bar> + \<bar>a - b\<bar>"

  1133     by (simp add: abs_triangle_ineq)

  1134   then show ?thesis

  1135     by (simp add: algebra_simps)

  1136 qed

  1137

  1138 lemma abs_triangle_ineq2_sym: "\<bar>a\<bar> - \<bar>b\<bar> \<le> \<bar>b - a\<bar>"

  1139   by (simp only: abs_minus_commute [of b] abs_triangle_ineq2)

  1140

  1141 lemma abs_triangle_ineq3: "\<bar>\<bar>a\<bar> - \<bar>b\<bar>\<bar> \<le> \<bar>a - b\<bar>"

  1142   by (simp add: abs_le_iff abs_triangle_ineq2 abs_triangle_ineq2_sym)

  1143

  1144 lemma abs_triangle_ineq4: "\<bar>a - b\<bar> \<le> \<bar>a\<bar> + \<bar>b\<bar>"

  1145 proof -

  1146   have "\<bar>a - b\<bar> = \<bar>a + - b\<bar>" by (subst diff_minus, rule refl)

  1147   also have "... \<le> \<bar>a\<bar> + \<bar>- b\<bar>" by (rule abs_triangle_ineq)

  1148   finally show ?thesis by simp

  1149 qed

  1150

  1151 lemma abs_diff_triangle_ineq: "\<bar>a + b - (c + d)\<bar> \<le> \<bar>a - c\<bar> + \<bar>b - d\<bar>"

  1152 proof -

  1153   have "\<bar>a + b - (c+d)\<bar> = \<bar>(a-c) + (b-d)\<bar>" by (simp add: diff_minus add_ac)

  1154   also have "... \<le> \<bar>a-c\<bar> + \<bar>b-d\<bar>" by (rule abs_triangle_ineq)

  1155   finally show ?thesis .

  1156 qed

  1157

  1158 lemma abs_add_abs [simp]:

  1159   "\<bar>\<bar>a\<bar> + \<bar>b\<bar>\<bar> = \<bar>a\<bar> + \<bar>b\<bar>" (is "?L = ?R")

  1160 proof (rule antisym)

  1161   show "?L \<ge> ?R" by(rule abs_ge_self)

  1162 next

  1163   have "?L \<le> \<bar>\<bar>a\<bar>\<bar> + \<bar>\<bar>b\<bar>\<bar>" by(rule abs_triangle_ineq)

  1164   also have "\<dots> = ?R" by simp

  1165   finally show "?L \<le> ?R" .

  1166 qed

  1167

  1168 end

  1169

  1170 text {* Needed for abelian cancellation simprocs: *}

  1171

  1172 lemma add_cancel_21: "((x::'a::ab_group_add) + (y + z) = y + u) = (x + z = u)"

  1173 apply (subst add_left_commute)

  1174 apply (subst add_left_cancel)

  1175 apply simp

  1176 done

  1177

  1178 lemma add_cancel_end: "(x + (y + z) = y) = (x = - (z::'a::ab_group_add))"

  1179 apply (subst add_cancel_21[of _ _ _ 0, simplified])

  1180 apply (simp add: add_right_cancel[symmetric, of "x" "-z" "z", simplified])

  1181 done

  1182

  1183 lemma less_eqI: "(x::'a::ordered_ab_group_add) - y = x' - y' \<Longrightarrow> (x < y) = (x' < y')"

  1184 by (simp add: less_iff_diff_less_0[of x y] less_iff_diff_less_0[of x' y'])

  1185

  1186 lemma le_eqI: "(x::'a::ordered_ab_group_add) - y = x' - y' \<Longrightarrow> (y <= x) = (y' <= x')"

  1187 apply (simp add: le_iff_diff_le_0[of y x] le_iff_diff_le_0[of  y' x'])

  1188 apply (simp add: neg_le_iff_le[symmetric, of "y-x" 0] neg_le_iff_le[symmetric, of "y'-x'" 0])

  1189 done

  1190

  1191 lemma eq_eqI: "(x::'a::ab_group_add) - y = x' - y' \<Longrightarrow> (x = y) = (x' = y')"

  1192 by (simp only: eq_iff_diff_eq_0[of x y] eq_iff_diff_eq_0[of x' y'])

  1193

  1194 lemma diff_def: "(x::'a::ab_group_add) - y == x + (-y)"

  1195 by (simp add: diff_minus)

  1196

  1197 lemma le_add_right_mono:

  1198   assumes

  1199   "a <= b + (c::'a::ordered_ab_group_add)"

  1200   "c <= d"

  1201   shows "a <= b + d"

  1202   apply (rule_tac order_trans[where y = "b+c"])

  1203   apply (simp_all add: prems)

  1204   done

  1205

  1206

  1207 subsection {* Tools setup *}

  1208

  1209 lemma add_mono_thms_linordered_semiring [no_atp]:

  1210   fixes i j k :: "'a\<Colon>ordered_ab_semigroup_add"

  1211   shows "i \<le> j \<and> k \<le> l \<Longrightarrow> i + k \<le> j + l"

  1212     and "i = j \<and> k \<le> l \<Longrightarrow> i + k \<le> j + l"

  1213     and "i \<le> j \<and> k = l \<Longrightarrow> i + k \<le> j + l"

  1214     and "i = j \<and> k = l \<Longrightarrow> i + k = j + l"

  1215 by (rule add_mono, clarify+)+

  1216

  1217 lemma add_mono_thms_linordered_field [no_atp]:

  1218   fixes i j k :: "'a\<Colon>ordered_cancel_ab_semigroup_add"

  1219   shows "i < j \<and> k = l \<Longrightarrow> i + k < j + l"

  1220     and "i = j \<and> k < l \<Longrightarrow> i + k < j + l"

  1221     and "i < j \<and> k \<le> l \<Longrightarrow> i + k < j + l"

  1222     and "i \<le> j \<and> k < l \<Longrightarrow> i + k < j + l"

  1223     and "i < j \<and> k < l \<Longrightarrow> i + k < j + l"

  1224 by (auto intro: add_strict_right_mono add_strict_left_mono

  1225   add_less_le_mono add_le_less_mono add_strict_mono)

  1226

  1227 text{*Simplification of @{term "x-y < 0"}, etc.*}

  1228 lemmas diff_less_0_iff_less [simp, no_atp] = less_iff_diff_less_0 [symmetric]

  1229 lemmas diff_le_0_iff_le [simp, no_atp] = le_iff_diff_le_0 [symmetric]

  1230

  1231 ML {*

  1232 structure ab_group_add_cancel = Abel_Cancel

  1233 (

  1234

  1235 (* term order for abelian groups *)

  1236

  1237 fun agrp_ord (Const (a, _)) = find_index (fn a' => a = a')

  1238       [@{const_name Groups.zero}, @{const_name Groups.plus},

  1239         @{const_name Groups.uminus}, @{const_name Groups.minus}]

  1240   | agrp_ord _ = ~1;

  1241

  1242 fun termless_agrp (a, b) = (Term_Ord.term_lpo agrp_ord (a, b) = LESS);

  1243

  1244 local

  1245   val ac1 = mk_meta_eq @{thm add_assoc};

  1246   val ac2 = mk_meta_eq @{thm add_commute};

  1247   val ac3 = mk_meta_eq @{thm add_left_commute};

  1248   fun solve_add_ac thy _ (_ $(Const (@{const_name Groups.plus},_)$ _ $_)$ _) =

  1249         SOME ac1

  1250     | solve_add_ac thy _ (_ $x$ (Const (@{const_name Groups.plus},_) $y$ z)) =

  1251         if termless_agrp (y, x) then SOME ac3 else NONE

  1252     | solve_add_ac thy _ (_ $x$ y) =

  1253         if termless_agrp (y, x) then SOME ac2 else NONE

  1254     | solve_add_ac thy _ _ = NONE

  1255 in

  1256   val add_ac_proc = Simplifier.simproc @{theory}

  1257     "add_ac_proc" ["x + y::'a::ab_semigroup_add"] solve_add_ac;

  1258 end;

  1259

  1260 val eq_reflection = @{thm eq_reflection};

  1261

  1262 val T = @{typ "'a::ab_group_add"};

  1263

  1264 val cancel_ss = HOL_basic_ss settermless termless_agrp

  1265   addsimprocs [add_ac_proc] addsimps

  1266   [@{thm add_0_left}, @{thm add_0_right}, @{thm diff_def},

  1267    @{thm minus_add_distrib}, @{thm minus_minus}, @{thm minus_zero},

  1268    @{thm right_minus}, @{thm left_minus}, @{thm add_minus_cancel},

  1269    @{thm minus_add_cancel}];

  1270

  1271 val sum_pats = [@{cterm "x + y::'a::ab_group_add"}, @{cterm "x - y::'a::ab_group_add"}];

  1272

  1273 val eqI_rules = [@{thm less_eqI}, @{thm le_eqI}, @{thm eq_eqI}];

  1274

  1275 val dest_eqI =

  1276   fst o HOLogic.dest_bin @{const_name "op ="} HOLogic.boolT o HOLogic.dest_Trueprop o concl_of;

  1277

  1278 );

  1279 *}

  1280

  1281 ML {*

  1282   Addsimprocs [ab_group_add_cancel.sum_conv, ab_group_add_cancel.rel_conv];

  1283 *}

  1284

  1285 code_modulename SML

  1286   Groups Arith

  1287

  1288 code_modulename OCaml

  1289   Groups Arith

  1290

  1291 code_modulename Haskell

  1292   Groups Arith

  1293

  1294 end