src/HOL/Groups.thy
 author wenzelm Sun Sep 05 21:41:24 2010 +0200 (2010-09-05) changeset 39134 917b4b6ba3d2 parent 37986 3b3187adf292 child 40368 47c186c8577d permissions -rw-r--r--
turned show_sorts/show_types into proper configuration options;
     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 ("Tools/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 (advanced) {*

   128 let

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

   130     if not (null ts) orelse T = dummyT

   131       orelse not (Config.get ctxt 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

   150 subsection {* Semigroups and Monoids *}

   151

   152 class semigroup_add = plus +

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

   154

   155 sublocale semigroup_add < add!: semigroup plus proof

   156 qed (fact add_assoc)

   157

   158 class ab_semigroup_add = semigroup_add +

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

   160

   161 sublocale ab_semigroup_add < add!: abel_semigroup plus proof

   162 qed (fact add_commute)

   163

   164 context ab_semigroup_add

   165 begin

   166

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

   168

   169 theorems add_ac = add_assoc add_commute add_left_commute

   170

   171 end

   172

   173 theorems add_ac = add_assoc add_commute add_left_commute

   174

   175 class semigroup_mult = times +

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

   177

   178 sublocale semigroup_mult < mult!: semigroup times proof

   179 qed (fact mult_assoc)

   180

   181 class ab_semigroup_mult = semigroup_mult +

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

   183

   184 sublocale ab_semigroup_mult < mult!: abel_semigroup times proof

   185 qed (fact mult_commute)

   186

   187 context ab_semigroup_mult

   188 begin

   189

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

   191

   192 theorems mult_ac = mult_assoc mult_commute mult_left_commute

   193

   194 end

   195

   196 theorems mult_ac = mult_assoc mult_commute mult_left_commute

   197

   198 class monoid_add = zero + semigroup_add +

   199   assumes add_0_left: "0 + a = a"

   200     and add_0_right: "a + 0 = a"

   201

   202 sublocale monoid_add < add!: monoid plus 0 proof

   203 qed (fact add_0_left add_0_right)+

   204

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

   206 by (rule eq_commute)

   207

   208 class comm_monoid_add = zero + ab_semigroup_add +

   209   assumes add_0: "0 + a = a"

   210

   211 sublocale comm_monoid_add < add!: comm_monoid plus 0 proof

   212 qed (insert add_0, simp add: ac_simps)

   213

   214 subclass (in comm_monoid_add) monoid_add proof

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

   216

   217 class monoid_mult = one + semigroup_mult +

   218   assumes mult_1_left: "1 * a  = a"

   219     and mult_1_right: "a * 1 = a"

   220

   221 sublocale monoid_mult < mult!: monoid times 1 proof

   222 qed (fact mult_1_left mult_1_right)+

   223

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

   225 by (rule eq_commute)

   226

   227 class comm_monoid_mult = one + ab_semigroup_mult +

   228   assumes mult_1: "1 * a = a"

   229

   230 sublocale comm_monoid_mult < mult!: comm_monoid times 1 proof

   231 qed (insert mult_1, simp add: ac_simps)

   232

   233 subclass (in comm_monoid_mult) monoid_mult proof

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

   235

   236 class cancel_semigroup_add = semigroup_add +

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

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

   239 begin

   240

   241 lemma add_left_cancel [simp]:

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

   243 by (blast dest: add_left_imp_eq)

   244

   245 lemma add_right_cancel [simp]:

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

   247 by (blast dest: add_right_imp_eq)

   248

   249 end

   250

   251 class cancel_ab_semigroup_add = ab_semigroup_add +

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

   253 begin

   254

   255 subclass cancel_semigroup_add

   256 proof

   257   fix a b c :: 'a

   258   assume "a + b = a + c"

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

   260 next

   261   fix a b c :: 'a

   262   assume "b + a = c + a"

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

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

   265 qed

   266

   267 end

   268

   269 class cancel_comm_monoid_add = cancel_ab_semigroup_add + comm_monoid_add

   270

   271

   272 subsection {* Groups *}

   273

   274 class group_add = minus + uminus + monoid_add +

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

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

   277 begin

   278

   279 lemma minus_unique:

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

   281 proof -

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

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

   284   finally show ?thesis .

   285 qed

   286

   287 lemmas equals_zero_I = minus_unique (* legacy name *)

   288

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

   290 proof -

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

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

   293 qed

   294

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

   296 proof -

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

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

   299 qed

   300

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

   302 proof -

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

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

   305   finally show ?thesis .

   306 qed

   307

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

   309 by (simp add: add_assoc [symmetric])

   310

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

   312 by (simp add: add_assoc [symmetric])

   313

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

   315 proof -

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

   317     by (simp add: add_assoc add_minus_cancel)

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

   319     by (rule minus_unique)

   320 qed

   321

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

   323 proof

   324   assume "a - b = 0"

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

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

   327   finally show "a = b" .

   328 next

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

   330 qed

   331

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

   333 by (simp add: diff_minus)

   334

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

   336 by (simp add: diff_minus)

   337

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

   339 by (simp add: diff_minus)

   340

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

   342 by (simp add: diff_minus)

   343

   344 lemma neg_equal_iff_equal [simp]:

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

   346 proof

   347   assume "- a = - b"

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

   349   thus "a = b" by simp

   350 next

   351   assume "a = b"

   352   thus "- a = - b" by simp

   353 qed

   354

   355 lemma neg_equal_0_iff_equal [simp]:

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

   357 by (subst neg_equal_iff_equal [symmetric], simp)

   358

   359 lemma neg_0_equal_iff_equal [simp]:

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

   361 by (subst neg_equal_iff_equal [symmetric], simp)

   362

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

   364

   365 lemma equation_minus_iff:

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

   367 proof -

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

   369   thus ?thesis by (simp add: eq_commute)

   370 qed

   371

   372 lemma minus_equation_iff:

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

   374 proof -

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

   376   thus ?thesis by (simp add: eq_commute)

   377 qed

   378

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

   380 by (simp add: diff_minus add_assoc)

   381

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

   383 by (simp add: diff_minus add_assoc)

   384

   385 declare diff_minus[symmetric, algebra_simps, field_simps]

   386

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

   388 proof

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

   390 next

   391   assume "a + b = 0"

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

   393     by (simp only: add_assoc)

   394   ultimately show "a = - b" by simp

   395 qed

   396

   397 end

   398

   399 class ab_group_add = minus + uminus + comm_monoid_add +

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

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

   402 begin

   403

   404 subclass group_add

   405   proof qed (simp_all add: ab_left_minus ab_diff_minus)

   406

   407 subclass cancel_comm_monoid_add

   408 proof

   409   fix a b c :: 'a

   410   assume "a + b = a + c"

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

   412     unfolding add_assoc by simp

   413   then show "b = c" by simp

   414 qed

   415

   416 lemma uminus_add_conv_diff[algebra_simps, field_simps]:

   417   "- a + b = b - a"

   418 by (simp add:diff_minus add_commute)

   419

   420 lemma minus_add_distrib [simp]:

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

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

   423

   424 lemma minus_diff_eq [simp]:

   425   "- (a - b) = b - a"

   426 by (simp add: diff_minus add_commute)

   427

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

   429 by (simp add: diff_minus add_ac)

   430

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

   432 by (simp add: diff_minus add_ac)

   433

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

   435 by (auto simp add: diff_minus add_assoc)

   436

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

   438 by (auto simp add: diff_minus add_assoc)

   439

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

   441 by (simp add: diff_minus add_ac)

   442

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

   444 by (simp add: diff_minus add_ac)

   445

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

   447 by (simp add: algebra_simps)

   448

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

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

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

   452 by (simp add: algebra_simps)

   453

   454 lemma diff_eq_diff_eq:

   455   "a - b = c - d \<Longrightarrow> a = b \<longleftrightarrow> c = d"

   456   by (auto simp add: algebra_simps)

   457

   458 end

   459

   460

   461 subsection {* (Partially) Ordered Groups *}

   462

   463 text {*

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

   465   \begin{itemize}

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

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

   468   \end{itemize}

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

   470   \begin{itemize}

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

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

   473   \end{itemize}

   474 *}

   475

   476 class ordered_ab_semigroup_add = order + ab_semigroup_add +

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

   478 begin

   479

   480 lemma add_right_mono:

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

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

   483

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

   485 lemma add_mono:

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

   487   apply (erule add_right_mono [THEN order_trans])

   488   apply (simp add: add_commute add_left_mono)

   489   done

   490

   491 end

   492

   493 class ordered_cancel_ab_semigroup_add =

   494   ordered_ab_semigroup_add + cancel_ab_semigroup_add

   495 begin

   496

   497 lemma add_strict_left_mono:

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

   499 by (auto simp add: less_le add_left_mono)

   500

   501 lemma add_strict_right_mono:

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

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

   504

   505 text{*Strict monotonicity in both arguments*}

   506 lemma add_strict_mono:

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

   508 apply (erule add_strict_right_mono [THEN less_trans])

   509 apply (erule add_strict_left_mono)

   510 done

   511

   512 lemma add_less_le_mono:

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

   514 apply (erule add_strict_right_mono [THEN less_le_trans])

   515 apply (erule add_left_mono)

   516 done

   517

   518 lemma add_le_less_mono:

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

   520 apply (erule add_right_mono [THEN le_less_trans])

   521 apply (erule add_strict_left_mono)

   522 done

   523

   524 end

   525

   526 class ordered_ab_semigroup_add_imp_le =

   527   ordered_cancel_ab_semigroup_add +

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

   529 begin

   530

   531 lemma add_less_imp_less_left:

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

   533 proof -

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

   535   have "a <= b"

   536     apply (insert le)

   537     apply (drule add_le_imp_le_left)

   538     by (insert le, drule add_le_imp_le_left, assumption)

   539   moreover have "a \<noteq> b"

   540   proof (rule ccontr)

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

   542     then have "a = b" by simp

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

   544     with less show "False"by simp

   545   qed

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

   547 qed

   548

   549 lemma add_less_imp_less_right:

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

   551 apply (rule add_less_imp_less_left [of c])

   552 apply (simp add: add_commute)

   553 done

   554

   555 lemma add_less_cancel_left [simp]:

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

   557 by (blast intro: add_less_imp_less_left add_strict_left_mono)

   558

   559 lemma add_less_cancel_right [simp]:

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

   561 by (blast intro: add_less_imp_less_right add_strict_right_mono)

   562

   563 lemma add_le_cancel_left [simp]:

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

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

   566

   567 lemma add_le_cancel_right [simp]:

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

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

   570

   571 lemma add_le_imp_le_right:

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

   573 by simp

   574

   575 lemma max_add_distrib_left:

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

   577   unfolding max_def by auto

   578

   579 lemma min_add_distrib_left:

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

   581   unfolding min_def by auto

   582

   583 end

   584

   585 subsection {* Support for reasoning about signs *}

   586

   587 class ordered_comm_monoid_add =

   588   ordered_cancel_ab_semigroup_add + comm_monoid_add

   589 begin

   590

   591 lemma add_pos_nonneg:

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

   593 proof -

   594   have "0 + 0 < a + b"

   595     using assms by (rule add_less_le_mono)

   596   then show ?thesis by simp

   597 qed

   598

   599 lemma add_pos_pos:

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

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

   602

   603 lemma add_nonneg_pos:

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

   605 proof -

   606   have "0 + 0 < a + b"

   607     using assms by (rule add_le_less_mono)

   608   then show ?thesis by simp

   609 qed

   610

   611 lemma add_nonneg_nonneg [simp]:

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

   613 proof -

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

   615     using assms by (rule add_mono)

   616   then show ?thesis by simp

   617 qed

   618

   619 lemma add_neg_nonpos:

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

   621 proof -

   622   have "a + b < 0 + 0"

   623     using assms by (rule add_less_le_mono)

   624   then show ?thesis by simp

   625 qed

   626

   627 lemma add_neg_neg:

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

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

   630

   631 lemma add_nonpos_neg:

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

   633 proof -

   634   have "a + b < 0 + 0"

   635     using assms by (rule add_le_less_mono)

   636   then show ?thesis by simp

   637 qed

   638

   639 lemma add_nonpos_nonpos:

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

   641 proof -

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

   643     using assms by (rule add_mono)

   644   then show ?thesis by simp

   645 qed

   646

   647 lemmas add_sign_intros =

   648   add_pos_nonneg add_pos_pos add_nonneg_pos add_nonneg_nonneg

   649   add_neg_nonpos add_neg_neg add_nonpos_neg add_nonpos_nonpos

   650

   651 lemma add_nonneg_eq_0_iff:

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

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

   654 proof (intro iffI conjI)

   655   have "x = x + 0" by simp

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

   657   also assume "x + y = 0"

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

   659   finally show "x = 0" .

   660 next

   661   have "y = 0 + y" by simp

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

   663   also assume "x + y = 0"

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

   665   finally show "y = 0" .

   666 next

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

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

   669 qed

   670

   671 end

   672

   673 class ordered_ab_group_add =

   674   ab_group_add + ordered_ab_semigroup_add

   675 begin

   676

   677 subclass ordered_cancel_ab_semigroup_add ..

   678

   679 subclass ordered_ab_semigroup_add_imp_le

   680 proof

   681   fix a b c :: 'a

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

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

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

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

   686 qed

   687

   688 subclass ordered_comm_monoid_add ..

   689

   690 lemma max_diff_distrib_left:

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

   692 by (simp add: diff_minus, rule max_add_distrib_left)

   693

   694 lemma min_diff_distrib_left:

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

   696 by (simp add: diff_minus, rule min_add_distrib_left)

   697

   698 lemma le_imp_neg_le:

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

   700 proof -

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

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

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

   704   thus ?thesis by (simp add: add_assoc)

   705 qed

   706

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

   708 proof

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

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

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

   712 next

   713   assume "a\<le>b"

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

   715 qed

   716

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

   718 by (subst neg_le_iff_le [symmetric], simp)

   719

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

   721 by (subst neg_le_iff_le [symmetric], simp)

   722

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

   724 by (force simp add: less_le)

   725

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

   727 by (subst neg_less_iff_less [symmetric], simp)

   728

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

   730 by (subst neg_less_iff_less [symmetric], simp)

   731

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

   733

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

   735 proof -

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

   737   thus ?thesis by simp

   738 qed

   739

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

   741 proof -

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

   743   thus ?thesis by simp

   744 qed

   745

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

   747 proof -

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

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

   750     apply (auto simp only: le_less)

   751     apply (drule mm)

   752     apply (simp_all)

   753     apply (drule mm[simplified], assumption)

   754     done

   755   then show ?thesis by simp

   756 qed

   757

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

   759 by (auto simp add: le_less minus_less_iff)

   760

   761 lemma diff_less_0_iff_less [simp, no_atp]:

   762   "a - b < 0 \<longleftrightarrow> a < b"

   763 proof -

   764   have "a - b < 0 \<longleftrightarrow> a + (- b) < b + (- b)" by (simp add: diff_minus)

   765   also have "... \<longleftrightarrow> a < b" by (simp only: add_less_cancel_right)

   766   finally show ?thesis .

   767 qed

   768

   769 lemmas less_iff_diff_less_0 = diff_less_0_iff_less [symmetric]

   770

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

   772 apply (subst less_iff_diff_less_0 [of a])

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

   774 apply (simp add: diff_minus add_ac)

   775 done

   776

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

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

   779 apply (subst less_iff_diff_less_0 [of a])

   780 apply (simp add: diff_minus add_ac)

   781 done

   782

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

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

   785

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

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

   788

   789 lemma diff_le_0_iff_le [simp, no_atp]:

   790   "a - b \<le> 0 \<longleftrightarrow> a \<le> b"

   791   by (simp add: algebra_simps)

   792

   793 lemmas le_iff_diff_le_0 = diff_le_0_iff_le [symmetric]

   794

   795 lemma diff_eq_diff_less:

   796   "a - b = c - d \<Longrightarrow> a < b \<longleftrightarrow> c < d"

   797   by (auto simp only: less_iff_diff_less_0 [of a b] less_iff_diff_less_0 [of c d])

   798

   799 lemma diff_eq_diff_less_eq:

   800   "a - b = c - d \<Longrightarrow> a \<le> b \<longleftrightarrow> c \<le> d"

   801   by (auto simp only: le_iff_diff_le_0 [of a b] le_iff_diff_le_0 [of c d])

   802

   803 end

   804

   805 use "Tools/abel_cancel.ML"

   806

   807 simproc_setup abel_cancel_sum

   808   ("a + b::'a::ab_group_add" | "a - b::'a::ab_group_add") =

   809   {* fn phi => Abel_Cancel.sum_proc *}

   810

   811 simproc_setup abel_cancel_relation

   812   ("a < (b::'a::ordered_ab_group_add)" | "a \<le> (b::'a::ordered_ab_group_add)" | "c = (d::'b::ab_group_add)") =

   813   {* fn phi => Abel_Cancel.rel_proc *}

   814

   815 class linordered_ab_semigroup_add =

   816   linorder + ordered_ab_semigroup_add

   817

   818 class linordered_cancel_ab_semigroup_add =

   819   linorder + ordered_cancel_ab_semigroup_add

   820 begin

   821

   822 subclass linordered_ab_semigroup_add ..

   823

   824 subclass ordered_ab_semigroup_add_imp_le

   825 proof

   826   fix a b c :: 'a

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

   828   show "a <= b"

   829   proof (rule ccontr)

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

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

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

   833     have "a = b"

   834       apply (insert le)

   835       apply (insert le2)

   836       apply (drule antisym, simp_all)

   837       done

   838     with w show False

   839       by (simp add: linorder_not_le [symmetric])

   840   qed

   841 qed

   842

   843 end

   844

   845 class linordered_ab_group_add = linorder + ordered_ab_group_add

   846 begin

   847

   848 subclass linordered_cancel_ab_semigroup_add ..

   849

   850 lemma neg_less_eq_nonneg [simp]:

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

   852 proof

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

   854   proof (rule classical)

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

   856     then have "a < 0" by auto

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

   858     then show ?thesis by auto

   859   qed

   860 next

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

   862   proof (rule order_trans)

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

   864   next

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

   866   qed

   867 qed

   868

   869 lemma neg_less_nonneg [simp]:

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

   871 proof

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

   873   proof (rule classical)

   874     assume "\<not> 0 < a"

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

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

   877     then show ?thesis by auto

   878   qed

   879 next

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

   881   proof (rule less_trans)

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

   883   next

   884     show "0 < a" using A .

   885   qed

   886 qed

   887

   888 lemma less_eq_neg_nonpos [simp]:

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

   890 proof

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

   892   proof (rule classical)

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

   894     then have "0 < a" by auto

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

   896     then show ?thesis by auto

   897   qed

   898 next

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

   900   proof (rule order_trans)

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

   902   next

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

   904   qed

   905 qed

   906

   907 lemma equal_neg_zero [simp]:

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

   909 proof

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

   911 next

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

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

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

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

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

   917   next

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

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

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

   921   qed

   922 qed

   923

   924 lemma neg_equal_zero [simp]:

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

   926   by (auto dest: sym)

   927

   928 lemma double_zero [simp]:

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

   930 proof

   931   assume assm: "a + a = 0"

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

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

   934 qed simp

   935

   936 lemma double_zero_sym [simp]:

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

   938   by (rule, drule sym) simp_all

   939

   940 lemma zero_less_double_add_iff_zero_less_single_add [simp]:

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

   942 proof

   943   assume "0 < a + a"

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

   945   then have "- a < a" by simp

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

   947 next

   948   assume "0 < a"

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

   950     by (rule add_strict_mono)

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

   952 qed

   953

   954 lemma zero_le_double_add_iff_zero_le_single_add [simp]:

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

   956   by (auto simp add: le_less)

   957

   958 lemma double_add_less_zero_iff_single_add_less_zero [simp]:

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

   960 proof -

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

   962     by (simp add: not_less)

   963   then show ?thesis by simp

   964 qed

   965

   966 lemma double_add_le_zero_iff_single_add_le_zero [simp]:

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

   968 proof -

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

   970     by (simp add: not_le)

   971   then show ?thesis by simp

   972 qed

   973

   974 lemma le_minus_self_iff:

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

   976 proof -

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

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

   979     by (simp add: add_assoc [symmetric])

   980   thus ?thesis by simp

   981 qed

   982

   983 lemma minus_le_self_iff:

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

   985 proof -

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

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

   988     by (simp add: add_assoc [symmetric])

   989   thus ?thesis by simp

   990 qed

   991

   992 lemma minus_max_eq_min:

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

   994   by (auto simp add: max_def min_def)

   995

   996 lemma minus_min_eq_max:

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

   998   by (auto simp add: max_def min_def)

   999

  1000 end

  1001

  1002 context ordered_comm_monoid_add

  1003 begin

  1004

  1005 lemma add_increasing:

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

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

  1008

  1009 lemma add_increasing2:

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

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

  1012

  1013 lemma add_strict_increasing:

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

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

  1016

  1017 lemma add_strict_increasing2:

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

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

  1020

  1021 end

  1022

  1023 class abs =

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

  1025 begin

  1026

  1027 notation (xsymbols)

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

  1029

  1030 notation (HTML output)

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

  1032

  1033 end

  1034

  1035 class sgn =

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

  1037

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

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

  1040

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

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

  1043 begin

  1044

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

  1046   by (simp add:sgn_if)

  1047

  1048 end

  1049

  1050 class ordered_ab_group_add_abs = ordered_ab_group_add + abs +

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

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

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

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

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

  1056 begin

  1057

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

  1059   unfolding neg_le_0_iff_le by simp

  1060

  1061 lemma abs_of_nonneg [simp]:

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

  1063 proof (rule antisym)

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

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

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

  1067 qed (rule abs_ge_self)

  1068

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

  1070 by (rule antisym)

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

  1072

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

  1074 proof -

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

  1076   proof (rule antisym)

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

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

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

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

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

  1082   qed

  1083   then show ?thesis by auto

  1084 qed

  1085

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

  1087 by simp

  1088

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

  1090 proof -

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

  1092   thus ?thesis by simp

  1093 qed

  1094

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

  1096 proof

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

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

  1099   thus "a = 0" by simp

  1100 next

  1101   assume "a = 0"

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

  1103 qed

  1104

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

  1106 by (simp add: less_le)

  1107

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

  1109 proof -

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

  1111   show ?thesis by (simp add: a)

  1112 qed

  1113

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

  1115 proof -

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

  1117   then show ?thesis by simp

  1118 qed

  1119

  1120 lemma abs_minus_commute:

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

  1122 proof -

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

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

  1125   finally show ?thesis .

  1126 qed

  1127

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

  1129 by (rule abs_of_nonneg, rule less_imp_le)

  1130

  1131 lemma abs_of_nonpos [simp]:

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

  1133 proof -

  1134   let ?b = "- a"

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

  1136   unfolding abs_minus_cancel [of "?b"]

  1137   unfolding neg_le_0_iff_le [of "?b"]

  1138   unfolding minus_minus by (erule abs_of_nonneg)

  1139   then show ?thesis using assms by auto

  1140 qed

  1141

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

  1143 by (rule abs_of_nonpos, rule less_imp_le)

  1144

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

  1146 by (insert abs_ge_self, blast intro: order_trans)

  1147

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

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

  1150

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

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

  1153

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

  1155 proof -

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

  1157     by (simp add: algebra_simps add_diff_cancel)

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

  1159     by (simp add: abs_triangle_ineq)

  1160   then show ?thesis

  1161     by (simp add: algebra_simps)

  1162 qed

  1163

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

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

  1166

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

  1168   by (simp add: abs_le_iff abs_triangle_ineq2 abs_triangle_ineq2_sym)

  1169

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

  1171 proof -

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

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

  1174   finally show ?thesis by simp

  1175 qed

  1176

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

  1178 proof -

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

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

  1181   finally show ?thesis .

  1182 qed

  1183

  1184 lemma abs_add_abs [simp]:

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

  1186 proof (rule antisym)

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

  1188 next

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

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

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

  1192 qed

  1193

  1194 end

  1195

  1196

  1197 subsection {* Tools setup *}

  1198

  1199 lemma add_mono_thms_linordered_semiring [no_atp]:

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

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

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

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

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

  1205 by (rule add_mono, clarify+)+

  1206

  1207 lemma add_mono_thms_linordered_field [no_atp]:

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

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

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

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

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

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

  1214 by (auto intro: add_strict_right_mono add_strict_left_mono

  1215   add_less_le_mono add_le_less_mono add_strict_mono)

  1216

  1217 code_modulename SML

  1218   Groups Arith

  1219

  1220 code_modulename OCaml

  1221   Groups Arith

  1222

  1223 code_modulename Haskell

  1224   Groups Arith

  1225

  1226

  1227 text {* Legacy *}

  1228

  1229 lemmas diff_def = diff_minus

  1230

  1231 end