src/HOL/Groups.thy
 author huffman Fri Jul 27 15:42:39 2012 +0200 (2012-07-27) changeset 48556 62a3fbf9d35b parent 45548 3e2722d66169 child 48891 c0eafbd55de3 permissions -rw-r--r--
replace abel_cancel simprocs with functionally equivalent, but simpler and faster ones
     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/group_cancel.ML")

    10 begin

    11

    12 subsection {* Fact collections *}

    13

    14 ML {*

    15 structure Ac_Simps = Named_Thms

    16 (

    17   val name = @{binding ac_simps}

    18   val description = "associativity and commutativity simplification rules"

    19 )

    20 *}

    21

    22 setup Ac_Simps.setup

    23

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

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

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

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

    28 group and ring equalities but also helps with inequalities.

    29

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

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

    32

    33 ML {*

    34 structure Algebra_Simps = Named_Thms

    35 (

    36   val name = @{binding algebra_simps}

    37   val description = "algebra simplification rules"

    38 )

    39 *}

    40

    41 setup Algebra_Simps.setup

    42

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

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

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

    46 more benign @{text algebra_simps}. *}

    47

    48 ML {*

    49 structure Field_Simps = Named_Thms

    50 (

    51   val name = @{binding field_simps}

    52   val description = "algebra simplification rules for fields"

    53 )

    54 *}

    55

    56 setup Field_Simps.setup

    57

    58

    59 subsection {* Abstract structures *}

    60

    61 text {*

    62   These locales provide basic structures for interpretation into

    63   bigger structures;  extensions require careful thinking, otherwise

    64   undesired effects may occur due to interpretation.

    65 *}

    66

    67 locale semigroup =

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

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

    70

    71 locale abel_semigroup = semigroup +

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

    73 begin

    74

    75 lemma left_commute [ac_simps]:

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

    77 proof -

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

    79     by (simp only: commute)

    80   then show ?thesis

    81     by (simp only: assoc)

    82 qed

    83

    84 end

    85

    86 locale monoid = semigroup +

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

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

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

    90

    91 locale comm_monoid = abel_semigroup +

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

    93   assumes comm_neutral: "a * 1 = a"

    94

    95 sublocale comm_monoid < monoid proof

    96 qed (simp_all add: commute comm_neutral)

    97

    98

    99 subsection {* Generic operations *}

   100

   101 class zero =

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

   103

   104 class one =

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

   106

   107 hide_const (open) zero one

   108

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

   110   unfolding Let_def ..

   111

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

   113   unfolding Let_def ..

   114

   115 setup {*

   116   Reorient_Proc.add

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

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

   119       | _ => false)

   120 *}

   121

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

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

   124

   125 typed_print_translation (advanced) {*

   126   let

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

   128       if not (null ts) orelse T = dummyT

   129         orelse not (Config.get ctxt show_types) andalso can Term.dest_Type T

   130       then raise Match

   131       else

   132         Syntax.const @{syntax_const "_constrain"} $Syntax.const c$

   133           Syntax_Phases.term_of_typ ctxt 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 subclass cancel_semigroup_add

   309 proof

   310   fix a b c :: 'a

   311   assume "a + b = a + c"

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

   313     unfolding add_assoc by simp

   314   then show "b = c" by simp

   315 next

   316   fix a b c :: 'a

   317   assume "b + a = c + a"

   318   then have "b + a + - a = c + a  + - a" by simp

   319   then show "b = c" unfolding add_assoc by simp

   320 qed

   321

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

   323 by (simp add: add_assoc [symmetric])

   324

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

   326 by (simp add: add_assoc [symmetric])

   327

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

   329 proof -

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

   331     by (simp add: add_assoc add_minus_cancel)

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

   333     by (rule minus_unique)

   334 qed

   335

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

   337 proof

   338   assume "a - b = 0"

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

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

   341   finally show "a = b" .

   342 next

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

   344 qed

   345

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

   347 by (simp add: diff_minus)

   348

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

   350 by (simp add: diff_minus)

   351

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

   353 by (simp add: diff_minus)

   354

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

   356 by (simp add: diff_minus)

   357

   358 lemma neg_equal_iff_equal [simp]:

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

   360 proof

   361   assume "- a = - b"

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

   363   thus "a = b" by simp

   364 next

   365   assume "a = b"

   366   thus "- a = - b" by simp

   367 qed

   368

   369 lemma neg_equal_0_iff_equal [simp]:

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

   371 by (subst neg_equal_iff_equal [symmetric], simp)

   372

   373 lemma neg_0_equal_iff_equal [simp]:

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

   375 by (subst neg_equal_iff_equal [symmetric], simp)

   376

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

   378

   379 lemma equation_minus_iff:

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

   381 proof -

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

   383   thus ?thesis by (simp add: eq_commute)

   384 qed

   385

   386 lemma minus_equation_iff:

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

   388 proof -

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

   390   thus ?thesis by (simp add: eq_commute)

   391 qed

   392

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

   394 by (simp add: diff_minus add_assoc)

   395

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

   397 by (simp add: diff_minus add_assoc)

   398

   399 declare diff_minus[symmetric, algebra_simps, field_simps]

   400

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

   402 proof

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

   404 next

   405   assume "a + b = 0"

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

   407     by (simp only: add_assoc)

   408   ultimately show "a = - b" by simp

   409 qed

   410

   411 lemma add_eq_0_iff: "x + y = 0 \<longleftrightarrow> y = - x"

   412   unfolding eq_neg_iff_add_eq_0 [symmetric]

   413   by (rule equation_minus_iff)

   414

   415 lemma minus_diff_eq [simp]: "- (a - b) = b - a"

   416   by (simp add: diff_minus minus_add)

   417

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

   419   by (simp add: diff_minus add_assoc)

   420

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

   422   by (auto simp add: diff_minus add_assoc)

   423

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

   425   by (auto simp add: diff_minus add_assoc)

   426

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

   428   by (simp add: diff_minus minus_add add_assoc)

   429

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

   431   by (fact right_minus_eq [symmetric])

   432

   433 lemma diff_eq_diff_eq:

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

   435   by (simp add: eq_iff_diff_eq_0 [of a b] eq_iff_diff_eq_0 [of c d])

   436

   437 end

   438

   439 class ab_group_add = minus + uminus + comm_monoid_add +

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

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

   442 begin

   443

   444 subclass group_add

   445   proof qed (simp_all add: ab_left_minus ab_diff_minus)

   446

   447 subclass cancel_comm_monoid_add

   448 proof

   449   fix a b c :: 'a

   450   assume "a + b = a + c"

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

   452     unfolding add_assoc by simp

   453   then show "b = c" by simp

   454 qed

   455

   456 lemma uminus_add_conv_diff[algebra_simps, field_simps]:

   457   "- a + b = b - a"

   458 by (simp add:diff_minus add_commute)

   459

   460 lemma minus_add_distrib [simp]:

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

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

   463

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

   465 by (simp add: diff_minus add_ac)

   466

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

   468 by (simp add: diff_minus add_ac)

   469

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

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

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

   473   by (rule right_minus_eq)

   474

   475 lemma add_diff_cancel_left: "(c + a) - (c + b) = a - b"

   476   by (simp add: diff_minus add_ac)

   477

   478 end

   479

   480

   481 subsection {* (Partially) Ordered Groups *}

   482

   483 text {*

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

   485   \begin{itemize}

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

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

   488   \end{itemize}

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

   490   \begin{itemize}

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

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

   493   \end{itemize}

   494 *}

   495

   496 class ordered_ab_semigroup_add = order + ab_semigroup_add +

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

   498 begin

   499

   500 lemma add_right_mono:

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

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

   503

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

   505 lemma add_mono:

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

   507   apply (erule add_right_mono [THEN order_trans])

   508   apply (simp add: add_commute add_left_mono)

   509   done

   510

   511 end

   512

   513 class ordered_cancel_ab_semigroup_add =

   514   ordered_ab_semigroup_add + cancel_ab_semigroup_add

   515 begin

   516

   517 lemma add_strict_left_mono:

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

   519 by (auto simp add: less_le add_left_mono)

   520

   521 lemma add_strict_right_mono:

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

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

   524

   525 text{*Strict monotonicity in both arguments*}

   526 lemma add_strict_mono:

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

   528 apply (erule add_strict_right_mono [THEN less_trans])

   529 apply (erule add_strict_left_mono)

   530 done

   531

   532 lemma add_less_le_mono:

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

   534 apply (erule add_strict_right_mono [THEN less_le_trans])

   535 apply (erule add_left_mono)

   536 done

   537

   538 lemma add_le_less_mono:

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

   540 apply (erule add_right_mono [THEN le_less_trans])

   541 apply (erule add_strict_left_mono)

   542 done

   543

   544 end

   545

   546 class ordered_ab_semigroup_add_imp_le =

   547   ordered_cancel_ab_semigroup_add +

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

   549 begin

   550

   551 lemma add_less_imp_less_left:

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

   553 proof -

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

   555   have "a <= b"

   556     apply (insert le)

   557     apply (drule add_le_imp_le_left)

   558     by (insert le, drule add_le_imp_le_left, assumption)

   559   moreover have "a \<noteq> b"

   560   proof (rule ccontr)

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

   562     then have "a = b" by simp

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

   564     with less show "False"by simp

   565   qed

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

   567 qed

   568

   569 lemma add_less_imp_less_right:

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

   571 apply (rule add_less_imp_less_left [of c])

   572 apply (simp add: add_commute)

   573 done

   574

   575 lemma add_less_cancel_left [simp]:

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

   577 by (blast intro: add_less_imp_less_left add_strict_left_mono)

   578

   579 lemma add_less_cancel_right [simp]:

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

   581 by (blast intro: add_less_imp_less_right add_strict_right_mono)

   582

   583 lemma add_le_cancel_left [simp]:

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

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

   586

   587 lemma add_le_cancel_right [simp]:

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

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

   590

   591 lemma add_le_imp_le_right:

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

   593 by simp

   594

   595 lemma max_add_distrib_left:

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

   597   unfolding max_def by auto

   598

   599 lemma min_add_distrib_left:

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

   601   unfolding min_def by auto

   602

   603 lemma max_add_distrib_right:

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

   605   unfolding max_def by auto

   606

   607 lemma min_add_distrib_right:

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

   609   unfolding min_def by auto

   610

   611 end

   612

   613 subsection {* Support for reasoning about signs *}

   614

   615 class ordered_comm_monoid_add =

   616   ordered_cancel_ab_semigroup_add + comm_monoid_add

   617 begin

   618

   619 lemma add_pos_nonneg:

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

   621 proof -

   622   have "0 + 0 < a + b"

   623     using assms by (rule add_less_le_mono)

   624   then show ?thesis by simp

   625 qed

   626

   627 lemma add_pos_pos:

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

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

   630

   631 lemma add_nonneg_pos:

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

   633 proof -

   634   have "0 + 0 < a + b"

   635     using assms by (rule add_le_less_mono)

   636   then show ?thesis by simp

   637 qed

   638

   639 lemma add_nonneg_nonneg [simp]:

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

   641 proof -

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

   643     using assms by (rule add_mono)

   644   then show ?thesis by simp

   645 qed

   646

   647 lemma add_neg_nonpos:

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

   649 proof -

   650   have "a + b < 0 + 0"

   651     using assms by (rule add_less_le_mono)

   652   then show ?thesis by simp

   653 qed

   654

   655 lemma add_neg_neg:

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

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

   658

   659 lemma add_nonpos_neg:

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

   661 proof -

   662   have "a + b < 0 + 0"

   663     using assms by (rule add_le_less_mono)

   664   then show ?thesis by simp

   665 qed

   666

   667 lemma add_nonpos_nonpos:

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

   669 proof -

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

   671     using assms by (rule add_mono)

   672   then show ?thesis by simp

   673 qed

   674

   675 lemmas add_sign_intros =

   676   add_pos_nonneg add_pos_pos add_nonneg_pos add_nonneg_nonneg

   677   add_neg_nonpos add_neg_neg add_nonpos_neg add_nonpos_nonpos

   678

   679 lemma add_nonneg_eq_0_iff:

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

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

   682 proof (intro iffI conjI)

   683   have "x = x + 0" by simp

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

   685   also assume "x + y = 0"

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

   687   finally show "x = 0" .

   688 next

   689   have "y = 0 + y" by simp

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

   691   also assume "x + y = 0"

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

   693   finally show "y = 0" .

   694 next

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

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

   697 qed

   698

   699 end

   700

   701 class ordered_ab_group_add =

   702   ab_group_add + ordered_ab_semigroup_add

   703 begin

   704

   705 subclass ordered_cancel_ab_semigroup_add ..

   706

   707 subclass ordered_ab_semigroup_add_imp_le

   708 proof

   709   fix a b c :: 'a

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

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

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

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

   714 qed

   715

   716 subclass ordered_comm_monoid_add ..

   717

   718 lemma max_diff_distrib_left:

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

   720 by (simp add: diff_minus, rule max_add_distrib_left)

   721

   722 lemma min_diff_distrib_left:

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

   724 by (simp add: diff_minus, rule min_add_distrib_left)

   725

   726 lemma le_imp_neg_le:

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

   728 proof -

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

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

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

   732   thus ?thesis by (simp add: add_assoc)

   733 qed

   734

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

   736 proof

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

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

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

   740 next

   741   assume "a\<le>b"

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

   743 qed

   744

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

   746 by (subst neg_le_iff_le [symmetric], simp)

   747

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

   749 by (subst neg_le_iff_le [symmetric], simp)

   750

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

   752 by (force simp add: less_le)

   753

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

   755 by (subst neg_less_iff_less [symmetric], simp)

   756

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

   758 by (subst neg_less_iff_less [symmetric], simp)

   759

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

   761

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

   763 proof -

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

   765   thus ?thesis by simp

   766 qed

   767

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

   769 proof -

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

   771   thus ?thesis by simp

   772 qed

   773

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

   775 proof -

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

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

   778     apply (auto simp only: le_less)

   779     apply (drule mm)

   780     apply (simp_all)

   781     apply (drule mm[simplified], assumption)

   782     done

   783   then show ?thesis by simp

   784 qed

   785

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

   787 by (auto simp add: le_less minus_less_iff)

   788

   789 lemma diff_less_0_iff_less [simp, no_atp]:

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

   791 proof -

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

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

   794   finally show ?thesis .

   795 qed

   796

   797 lemmas less_iff_diff_less_0 = diff_less_0_iff_less [symmetric]

   798

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

   800 apply (subst less_iff_diff_less_0 [of a])

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

   802 apply (simp add: diff_minus add_ac)

   803 done

   804

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

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

   807 apply (subst less_iff_diff_less_0 [of a])

   808 apply (simp add: diff_minus add_ac)

   809 done

   810

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

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

   813

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

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

   816

   817 lemma diff_le_0_iff_le [simp, no_atp]:

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

   819   by (simp add: algebra_simps)

   820

   821 lemmas le_iff_diff_le_0 = diff_le_0_iff_le [symmetric]

   822

   823 lemma diff_eq_diff_less:

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

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

   826

   827 lemma diff_eq_diff_less_eq:

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

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

   830

   831 end

   832

   833 use "Tools/group_cancel.ML"

   834

   835 simproc_setup group_cancel_add ("a + b::'a::ab_group_add") =

   836   {* fn phi => fn ss => try Group_Cancel.cancel_add_conv *}

   837

   838 simproc_setup group_cancel_diff ("a - b::'a::ab_group_add") =

   839   {* fn phi => fn ss => try Group_Cancel.cancel_diff_conv *}

   840

   841 simproc_setup group_cancel_eq ("a = (b::'a::ab_group_add)") =

   842   {* fn phi => fn ss => try Group_Cancel.cancel_eq_conv *}

   843

   844 simproc_setup group_cancel_le ("a \<le> (b::'a::ordered_ab_group_add)") =

   845   {* fn phi => fn ss => try Group_Cancel.cancel_le_conv *}

   846

   847 simproc_setup group_cancel_less ("a < (b::'a::ordered_ab_group_add)") =

   848   {* fn phi => fn ss => try Group_Cancel.cancel_less_conv *}

   849

   850 class linordered_ab_semigroup_add =

   851   linorder + ordered_ab_semigroup_add

   852

   853 class linordered_cancel_ab_semigroup_add =

   854   linorder + ordered_cancel_ab_semigroup_add

   855 begin

   856

   857 subclass linordered_ab_semigroup_add ..

   858

   859 subclass ordered_ab_semigroup_add_imp_le

   860 proof

   861   fix a b c :: 'a

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

   863   show "a <= b"

   864   proof (rule ccontr)

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

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

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

   868     have "a = b"

   869       apply (insert le)

   870       apply (insert le2)

   871       apply (drule antisym, simp_all)

   872       done

   873     with w show False

   874       by (simp add: linorder_not_le [symmetric])

   875   qed

   876 qed

   877

   878 end

   879

   880 class linordered_ab_group_add = linorder + ordered_ab_group_add

   881 begin

   882

   883 subclass linordered_cancel_ab_semigroup_add ..

   884

   885 lemma neg_less_eq_nonneg [simp]:

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

   887 proof

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

   889   proof (rule classical)

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

   891     then have "a < 0" by auto

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

   893     then show ?thesis by auto

   894   qed

   895 next

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

   897   proof (rule order_trans)

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

   899   next

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

   901   qed

   902 qed

   903

   904 lemma neg_less_nonneg [simp]:

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

   906 proof

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

   908   proof (rule classical)

   909     assume "\<not> 0 < a"

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

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

   912     then show ?thesis by auto

   913   qed

   914 next

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

   916   proof (rule less_trans)

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

   918   next

   919     show "0 < a" using A .

   920   qed

   921 qed

   922

   923 lemma less_eq_neg_nonpos [simp]:

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

   925 proof

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

   927   proof (rule classical)

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

   929     then have "0 < a" by auto

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

   931     then show ?thesis by auto

   932   qed

   933 next

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

   935   proof (rule order_trans)

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

   937   next

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

   939   qed

   940 qed

   941

   942 lemma equal_neg_zero [simp]:

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

   944 proof

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

   946 next

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

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

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

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

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

   952   next

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

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

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

   956   qed

   957 qed

   958

   959 lemma neg_equal_zero [simp]:

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

   961   by (auto dest: sym)

   962

   963 lemma double_zero [simp]:

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

   965 proof

   966   assume assm: "a + a = 0"

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

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

   969 qed simp

   970

   971 lemma double_zero_sym [simp]:

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

   973   by (rule, drule sym) simp_all

   974

   975 lemma zero_less_double_add_iff_zero_less_single_add [simp]:

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

   977 proof

   978   assume "0 < a + a"

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

   980   then have "- a < a" by simp

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

   982 next

   983   assume "0 < a"

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

   985     by (rule add_strict_mono)

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

   987 qed

   988

   989 lemma zero_le_double_add_iff_zero_le_single_add [simp]:

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

   991   by (auto simp add: le_less)

   992

   993 lemma double_add_less_zero_iff_single_add_less_zero [simp]:

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

   995 proof -

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

   997     by (simp add: not_less)

   998   then show ?thesis by simp

   999 qed

  1000

  1001 lemma double_add_le_zero_iff_single_add_le_zero [simp]:

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

  1003 proof -

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

  1005     by (simp add: not_le)

  1006   then show ?thesis by simp

  1007 qed

  1008

  1009 lemma le_minus_self_iff:

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

  1011 proof -

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

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

  1014     by (simp add: add_assoc [symmetric])

  1015   thus ?thesis by simp

  1016 qed

  1017

  1018 lemma minus_le_self_iff:

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

  1020 proof -

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

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

  1023     by (simp add: add_assoc [symmetric])

  1024   thus ?thesis by simp

  1025 qed

  1026

  1027 lemma minus_max_eq_min:

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

  1029   by (auto simp add: max_def min_def)

  1030

  1031 lemma minus_min_eq_max:

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

  1033   by (auto simp add: max_def min_def)

  1034

  1035 end

  1036

  1037 context ordered_comm_monoid_add

  1038 begin

  1039

  1040 lemma add_increasing:

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

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

  1043

  1044 lemma add_increasing2:

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

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

  1047

  1048 lemma add_strict_increasing:

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

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

  1051

  1052 lemma add_strict_increasing2:

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

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

  1055

  1056 end

  1057

  1058 class abs =

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

  1060 begin

  1061

  1062 notation (xsymbols)

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

  1064

  1065 notation (HTML output)

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

  1067

  1068 end

  1069

  1070 class sgn =

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

  1072

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

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

  1075

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

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

  1078 begin

  1079

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

  1081   by (simp add:sgn_if)

  1082

  1083 end

  1084

  1085 class ordered_ab_group_add_abs = ordered_ab_group_add + abs +

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

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

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

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

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

  1091 begin

  1092

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

  1094   unfolding neg_le_0_iff_le by simp

  1095

  1096 lemma abs_of_nonneg [simp]:

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

  1098 proof (rule antisym)

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

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

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

  1102 qed (rule abs_ge_self)

  1103

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

  1105 by (rule antisym)

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

  1107

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

  1109 proof -

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

  1111   proof (rule antisym)

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

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

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

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

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

  1117   qed

  1118   then show ?thesis by auto

  1119 qed

  1120

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

  1122 by simp

  1123

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

  1125 proof -

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

  1127   thus ?thesis by simp

  1128 qed

  1129

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

  1131 proof

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

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

  1134   thus "a = 0" by simp

  1135 next

  1136   assume "a = 0"

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

  1138 qed

  1139

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

  1141 by (simp add: less_le)

  1142

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

  1144 proof -

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

  1146   show ?thesis by (simp add: a)

  1147 qed

  1148

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

  1150 proof -

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

  1152   then show ?thesis by simp

  1153 qed

  1154

  1155 lemma abs_minus_commute:

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

  1157 proof -

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

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

  1160   finally show ?thesis .

  1161 qed

  1162

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

  1164 by (rule abs_of_nonneg, rule less_imp_le)

  1165

  1166 lemma abs_of_nonpos [simp]:

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

  1168 proof -

  1169   let ?b = "- a"

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

  1171   unfolding abs_minus_cancel [of "?b"]

  1172   unfolding neg_le_0_iff_le [of "?b"]

  1173   unfolding minus_minus by (erule abs_of_nonneg)

  1174   then show ?thesis using assms by auto

  1175 qed

  1176

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

  1178 by (rule abs_of_nonpos, rule less_imp_le)

  1179

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

  1181 by (insert abs_ge_self, blast intro: order_trans)

  1182

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

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

  1185

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

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

  1188

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

  1190 proof -

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

  1192     by (simp add: algebra_simps add_diff_cancel)

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

  1194     by (simp add: abs_triangle_ineq)

  1195   then show ?thesis

  1196     by (simp add: algebra_simps)

  1197 qed

  1198

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

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

  1201

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

  1203   by (simp add: abs_le_iff abs_triangle_ineq2 abs_triangle_ineq2_sym)

  1204

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

  1206 proof -

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

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

  1209   finally show ?thesis by simp

  1210 qed

  1211

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

  1213 proof -

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

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

  1216   finally show ?thesis .

  1217 qed

  1218

  1219 lemma abs_add_abs [simp]:

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

  1221 proof (rule antisym)

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

  1223 next

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

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

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

  1227 qed

  1228

  1229 end

  1230

  1231

  1232 subsection {* Tools setup *}

  1233

  1234 lemma add_mono_thms_linordered_semiring [no_atp]:

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

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

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

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

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

  1240 by (rule add_mono, clarify+)+

  1241

  1242 lemma add_mono_thms_linordered_field [no_atp]:

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

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

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

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

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

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

  1249 by (auto intro: add_strict_right_mono add_strict_left_mono

  1250   add_less_le_mono add_le_less_mono add_strict_mono)

  1251

  1252 code_modulename SML

  1253   Groups Arith

  1254

  1255 code_modulename OCaml

  1256   Groups Arith

  1257

  1258 code_modulename Haskell

  1259   Groups Arith

  1260

  1261

  1262 text {* Legacy *}

  1263

  1264 lemmas diff_def = diff_minus

  1265

  1266 end