src/HOL/Groups.thy
 author wenzelm Fri Oct 28 23:41:16 2011 +0200 (2011-10-28) changeset 45294 3c5d3d286055 parent 44848 f4d0b060c7ca child 45548 3e2722d66169 permissions -rw-r--r--
tuned Named_Thms: proper binding;
     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 (

    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

   288 lemmas equals_zero_I = minus_unique (* legacy name *)

   289

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

   291 proof -

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

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

   294 qed

   295

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

   297 proof -

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

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

   300 qed

   301

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

   303 proof -

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

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

   306   finally show ?thesis .

   307 qed

   308

   309 subclass cancel_semigroup_add

   310 proof

   311   fix a b c :: 'a

   312   assume "a + b = a + c"

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

   314     unfolding add_assoc by simp

   315   then show "b = c" by simp

   316 next

   317   fix a b c :: 'a

   318   assume "b + a = c + a"

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

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

   321 qed

   322

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

   324 by (simp add: add_assoc [symmetric])

   325

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

   327 by (simp add: add_assoc [symmetric])

   328

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

   330 proof -

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

   332     by (simp add: add_assoc add_minus_cancel)

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

   334     by (rule minus_unique)

   335 qed

   336

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

   338 proof

   339   assume "a - b = 0"

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

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

   342   finally show "a = b" .

   343 next

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

   345 qed

   346

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

   348 by (simp add: diff_minus)

   349

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

   351 by (simp add: diff_minus)

   352

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

   354 by (simp add: diff_minus)

   355

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

   357 by (simp add: diff_minus)

   358

   359 lemma neg_equal_iff_equal [simp]:

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

   361 proof

   362   assume "- a = - b"

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

   364   thus "a = b" by simp

   365 next

   366   assume "a = b"

   367   thus "- a = - b" by simp

   368 qed

   369

   370 lemma neg_equal_0_iff_equal [simp]:

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

   372 by (subst neg_equal_iff_equal [symmetric], simp)

   373

   374 lemma neg_0_equal_iff_equal [simp]:

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

   376 by (subst neg_equal_iff_equal [symmetric], simp)

   377

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

   379

   380 lemma equation_minus_iff:

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

   382 proof -

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

   384   thus ?thesis by (simp add: eq_commute)

   385 qed

   386

   387 lemma minus_equation_iff:

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

   389 proof -

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

   391   thus ?thesis by (simp add: eq_commute)

   392 qed

   393

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

   395 by (simp add: diff_minus add_assoc)

   396

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

   398 by (simp add: diff_minus add_assoc)

   399

   400 declare diff_minus[symmetric, algebra_simps, field_simps]

   401

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

   403 proof

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

   405 next

   406   assume "a + b = 0"

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

   408     by (simp only: add_assoc)

   409   ultimately show "a = - b" by simp

   410 qed

   411

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

   413   unfolding eq_neg_iff_add_eq_0 [symmetric]

   414   by (rule equation_minus_iff)

   415

   416 end

   417

   418 class ab_group_add = minus + uminus + comm_monoid_add +

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

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

   421 begin

   422

   423 subclass group_add

   424   proof qed (simp_all add: ab_left_minus ab_diff_minus)

   425

   426 subclass cancel_comm_monoid_add

   427 proof

   428   fix a b c :: 'a

   429   assume "a + b = a + c"

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

   431     unfolding add_assoc by simp

   432   then show "b = c" by simp

   433 qed

   434

   435 lemma uminus_add_conv_diff[algebra_simps, field_simps]:

   436   "- a + b = b - a"

   437 by (simp add:diff_minus add_commute)

   438

   439 lemma minus_add_distrib [simp]:

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

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

   442

   443 lemma minus_diff_eq [simp]:

   444   "- (a - b) = b - a"

   445 by (simp add: diff_minus add_commute)

   446

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

   448 by (simp add: diff_minus add_ac)

   449

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

   451 by (simp add: diff_minus add_ac)

   452

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

   454 by (auto simp add: diff_minus add_assoc)

   455

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

   457 by (auto simp add: diff_minus add_assoc)

   458

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

   460 by (simp add: diff_minus add_ac)

   461

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

   463 by (simp add: diff_minus add_ac)

   464

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

   466 by (simp add: algebra_simps)

   467

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

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

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

   471   by (rule right_minus_eq)

   472

   473 lemma diff_eq_diff_eq:

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

   475   by (auto simp add: algebra_simps)

   476

   477 end

   478

   479

   480 subsection {* (Partially) Ordered Groups *}

   481

   482 text {*

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

   484   \begin{itemize}

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

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

   487   \end{itemize}

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

   489   \begin{itemize}

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

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

   492   \end{itemize}

   493 *}

   494

   495 class ordered_ab_semigroup_add = order + ab_semigroup_add +

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

   497 begin

   498

   499 lemma add_right_mono:

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

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

   502

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

   504 lemma add_mono:

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

   506   apply (erule add_right_mono [THEN order_trans])

   507   apply (simp add: add_commute add_left_mono)

   508   done

   509

   510 end

   511

   512 class ordered_cancel_ab_semigroup_add =

   513   ordered_ab_semigroup_add + cancel_ab_semigroup_add

   514 begin

   515

   516 lemma add_strict_left_mono:

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

   518 by (auto simp add: less_le add_left_mono)

   519

   520 lemma add_strict_right_mono:

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

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

   523

   524 text{*Strict monotonicity in both arguments*}

   525 lemma add_strict_mono:

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

   527 apply (erule add_strict_right_mono [THEN less_trans])

   528 apply (erule add_strict_left_mono)

   529 done

   530

   531 lemma add_less_le_mono:

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

   533 apply (erule add_strict_right_mono [THEN less_le_trans])

   534 apply (erule add_left_mono)

   535 done

   536

   537 lemma add_le_less_mono:

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

   539 apply (erule add_right_mono [THEN le_less_trans])

   540 apply (erule add_strict_left_mono)

   541 done

   542

   543 end

   544

   545 class ordered_ab_semigroup_add_imp_le =

   546   ordered_cancel_ab_semigroup_add +

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

   548 begin

   549

   550 lemma add_less_imp_less_left:

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

   552 proof -

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

   554   have "a <= b"

   555     apply (insert le)

   556     apply (drule add_le_imp_le_left)

   557     by (insert le, drule add_le_imp_le_left, assumption)

   558   moreover have "a \<noteq> b"

   559   proof (rule ccontr)

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

   561     then have "a = b" by simp

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

   563     with less show "False"by simp

   564   qed

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

   566 qed

   567

   568 lemma add_less_imp_less_right:

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

   570 apply (rule add_less_imp_less_left [of c])

   571 apply (simp add: add_commute)

   572 done

   573

   574 lemma add_less_cancel_left [simp]:

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

   576 by (blast intro: add_less_imp_less_left add_strict_left_mono)

   577

   578 lemma add_less_cancel_right [simp]:

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

   580 by (blast intro: add_less_imp_less_right add_strict_right_mono)

   581

   582 lemma add_le_cancel_left [simp]:

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

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

   585

   586 lemma add_le_cancel_right [simp]:

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

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

   589

   590 lemma add_le_imp_le_right:

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

   592 by simp

   593

   594 lemma max_add_distrib_left:

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

   596   unfolding max_def by auto

   597

   598 lemma min_add_distrib_left:

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

   600   unfolding min_def by auto

   601

   602 lemma max_add_distrib_right:

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

   604   unfolding max_def by auto

   605

   606 lemma min_add_distrib_right:

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

   608   unfolding min_def by auto

   609

   610 end

   611

   612 subsection {* Support for reasoning about signs *}

   613

   614 class ordered_comm_monoid_add =

   615   ordered_cancel_ab_semigroup_add + comm_monoid_add

   616 begin

   617

   618 lemma add_pos_nonneg:

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

   620 proof -

   621   have "0 + 0 < a + b"

   622     using assms by (rule add_less_le_mono)

   623   then show ?thesis by simp

   624 qed

   625

   626 lemma add_pos_pos:

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

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

   629

   630 lemma add_nonneg_pos:

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

   632 proof -

   633   have "0 + 0 < a + b"

   634     using assms by (rule add_le_less_mono)

   635   then show ?thesis by simp

   636 qed

   637

   638 lemma add_nonneg_nonneg [simp]:

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

   640 proof -

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

   642     using assms by (rule add_mono)

   643   then show ?thesis by simp

   644 qed

   645

   646 lemma add_neg_nonpos:

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

   648 proof -

   649   have "a + b < 0 + 0"

   650     using assms by (rule add_less_le_mono)

   651   then show ?thesis by simp

   652 qed

   653

   654 lemma add_neg_neg:

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

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

   657

   658 lemma add_nonpos_neg:

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

   660 proof -

   661   have "a + b < 0 + 0"

   662     using assms by (rule add_le_less_mono)

   663   then show ?thesis by simp

   664 qed

   665

   666 lemma add_nonpos_nonpos:

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

   668 proof -

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

   670     using assms by (rule add_mono)

   671   then show ?thesis by simp

   672 qed

   673

   674 lemmas add_sign_intros =

   675   add_pos_nonneg add_pos_pos add_nonneg_pos add_nonneg_nonneg

   676   add_neg_nonpos add_neg_neg add_nonpos_neg add_nonpos_nonpos

   677

   678 lemma add_nonneg_eq_0_iff:

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

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

   681 proof (intro iffI conjI)

   682   have "x = x + 0" by simp

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

   684   also assume "x + y = 0"

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

   686   finally show "x = 0" .

   687 next

   688   have "y = 0 + y" by simp

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

   690   also assume "x + y = 0"

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

   692   finally show "y = 0" .

   693 next

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

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

   696 qed

   697

   698 end

   699

   700 class ordered_ab_group_add =

   701   ab_group_add + ordered_ab_semigroup_add

   702 begin

   703

   704 subclass ordered_cancel_ab_semigroup_add ..

   705

   706 subclass ordered_ab_semigroup_add_imp_le

   707 proof

   708   fix a b c :: 'a

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

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

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

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

   713 qed

   714

   715 subclass ordered_comm_monoid_add ..

   716

   717 lemma max_diff_distrib_left:

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

   719 by (simp add: diff_minus, rule max_add_distrib_left)

   720

   721 lemma min_diff_distrib_left:

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

   723 by (simp add: diff_minus, rule min_add_distrib_left)

   724

   725 lemma le_imp_neg_le:

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

   727 proof -

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

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

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

   731   thus ?thesis by (simp add: add_assoc)

   732 qed

   733

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

   735 proof

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

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

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

   739 next

   740   assume "a\<le>b"

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

   742 qed

   743

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

   745 by (subst neg_le_iff_le [symmetric], simp)

   746

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

   748 by (subst neg_le_iff_le [symmetric], simp)

   749

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

   751 by (force simp add: less_le)

   752

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

   754 by (subst neg_less_iff_less [symmetric], simp)

   755

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

   757 by (subst neg_less_iff_less [symmetric], simp)

   758

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

   760

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

   762 proof -

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

   764   thus ?thesis by simp

   765 qed

   766

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

   768 proof -

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

   770   thus ?thesis by simp

   771 qed

   772

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

   774 proof -

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

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

   777     apply (auto simp only: le_less)

   778     apply (drule mm)

   779     apply (simp_all)

   780     apply (drule mm[simplified], assumption)

   781     done

   782   then show ?thesis by simp

   783 qed

   784

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

   786 by (auto simp add: le_less minus_less_iff)

   787

   788 lemma diff_less_0_iff_less [simp, no_atp]:

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

   790 proof -

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

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

   793   finally show ?thesis .

   794 qed

   795

   796 lemmas less_iff_diff_less_0 = diff_less_0_iff_less [symmetric]

   797

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

   799 apply (subst less_iff_diff_less_0 [of a])

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

   801 apply (simp add: diff_minus add_ac)

   802 done

   803

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

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

   806 apply (subst less_iff_diff_less_0 [of a])

   807 apply (simp add: diff_minus add_ac)

   808 done

   809

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

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

   812

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

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

   815

   816 lemma diff_le_0_iff_le [simp, no_atp]:

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

   818   by (simp add: algebra_simps)

   819

   820 lemmas le_iff_diff_le_0 = diff_le_0_iff_le [symmetric]

   821

   822 lemma diff_eq_diff_less:

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

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

   825

   826 lemma diff_eq_diff_less_eq:

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

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

   829

   830 end

   831

   832 use "Tools/abel_cancel.ML"

   833

   834 simproc_setup abel_cancel_sum

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

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

   837

   838 simproc_setup abel_cancel_relation

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

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

   841

   842 class linordered_ab_semigroup_add =

   843   linorder + ordered_ab_semigroup_add

   844

   845 class linordered_cancel_ab_semigroup_add =

   846   linorder + ordered_cancel_ab_semigroup_add

   847 begin

   848

   849 subclass linordered_ab_semigroup_add ..

   850

   851 subclass ordered_ab_semigroup_add_imp_le

   852 proof

   853   fix a b c :: 'a

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

   855   show "a <= b"

   856   proof (rule ccontr)

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

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

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

   860     have "a = b"

   861       apply (insert le)

   862       apply (insert le2)

   863       apply (drule antisym, simp_all)

   864       done

   865     with w show False

   866       by (simp add: linorder_not_le [symmetric])

   867   qed

   868 qed

   869

   870 end

   871

   872 class linordered_ab_group_add = linorder + ordered_ab_group_add

   873 begin

   874

   875 subclass linordered_cancel_ab_semigroup_add ..

   876

   877 lemma neg_less_eq_nonneg [simp]:

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

   879 proof

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

   881   proof (rule classical)

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

   883     then have "a < 0" by auto

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

   885     then show ?thesis by auto

   886   qed

   887 next

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

   889   proof (rule order_trans)

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

   891   next

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

   893   qed

   894 qed

   895

   896 lemma neg_less_nonneg [simp]:

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

   898 proof

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

   900   proof (rule classical)

   901     assume "\<not> 0 < a"

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

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

   904     then show ?thesis by auto

   905   qed

   906 next

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

   908   proof (rule less_trans)

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

   910   next

   911     show "0 < a" using A .

   912   qed

   913 qed

   914

   915 lemma less_eq_neg_nonpos [simp]:

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

   917 proof

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

   919   proof (rule classical)

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

   921     then have "0 < a" by auto

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

   923     then show ?thesis by auto

   924   qed

   925 next

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

   927   proof (rule order_trans)

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

   929   next

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

   931   qed

   932 qed

   933

   934 lemma equal_neg_zero [simp]:

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

   936 proof

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

   938 next

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

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

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

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

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

   944   next

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

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

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

   948   qed

   949 qed

   950

   951 lemma neg_equal_zero [simp]:

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

   953   by (auto dest: sym)

   954

   955 lemma double_zero [simp]:

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

   957 proof

   958   assume assm: "a + a = 0"

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

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

   961 qed simp

   962

   963 lemma double_zero_sym [simp]:

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

   965   by (rule, drule sym) simp_all

   966

   967 lemma zero_less_double_add_iff_zero_less_single_add [simp]:

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

   969 proof

   970   assume "0 < a + a"

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

   972   then have "- a < a" by simp

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

   974 next

   975   assume "0 < a"

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

   977     by (rule add_strict_mono)

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

   979 qed

   980

   981 lemma zero_le_double_add_iff_zero_le_single_add [simp]:

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

   983   by (auto simp add: le_less)

   984

   985 lemma double_add_less_zero_iff_single_add_less_zero [simp]:

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

   987 proof -

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

   989     by (simp add: not_less)

   990   then show ?thesis by simp

   991 qed

   992

   993 lemma double_add_le_zero_iff_single_add_le_zero [simp]:

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

   995 proof -

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

   997     by (simp add: not_le)

   998   then show ?thesis by simp

   999 qed

  1000

  1001 lemma le_minus_self_iff:

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

  1003 proof -

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

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

  1006     by (simp add: add_assoc [symmetric])

  1007   thus ?thesis by simp

  1008 qed

  1009

  1010 lemma minus_le_self_iff:

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

  1012 proof -

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

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

  1015     by (simp add: add_assoc [symmetric])

  1016   thus ?thesis by simp

  1017 qed

  1018

  1019 lemma minus_max_eq_min:

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

  1021   by (auto simp add: max_def min_def)

  1022

  1023 lemma minus_min_eq_max:

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

  1025   by (auto simp add: max_def min_def)

  1026

  1027 end

  1028

  1029 context ordered_comm_monoid_add

  1030 begin

  1031

  1032 lemma add_increasing:

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

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

  1035

  1036 lemma add_increasing2:

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

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

  1039

  1040 lemma add_strict_increasing:

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

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

  1043

  1044 lemma add_strict_increasing2:

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

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

  1047

  1048 end

  1049

  1050 class abs =

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

  1052 begin

  1053

  1054 notation (xsymbols)

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

  1056

  1057 notation (HTML output)

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

  1059

  1060 end

  1061

  1062 class sgn =

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

  1064

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

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

  1067

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

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

  1070 begin

  1071

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

  1073   by (simp add:sgn_if)

  1074

  1075 end

  1076

  1077 class ordered_ab_group_add_abs = ordered_ab_group_add + abs +

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

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

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

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

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

  1083 begin

  1084

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

  1086   unfolding neg_le_0_iff_le by simp

  1087

  1088 lemma abs_of_nonneg [simp]:

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

  1090 proof (rule antisym)

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

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

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

  1094 qed (rule abs_ge_self)

  1095

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

  1097 by (rule antisym)

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

  1099

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

  1101 proof -

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

  1103   proof (rule antisym)

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

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

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

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

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

  1109   qed

  1110   then show ?thesis by auto

  1111 qed

  1112

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

  1114 by simp

  1115

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

  1117 proof -

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

  1119   thus ?thesis by simp

  1120 qed

  1121

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

  1123 proof

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

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

  1126   thus "a = 0" by simp

  1127 next

  1128   assume "a = 0"

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

  1130 qed

  1131

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

  1133 by (simp add: less_le)

  1134

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

  1136 proof -

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

  1138   show ?thesis by (simp add: a)

  1139 qed

  1140

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

  1142 proof -

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

  1144   then show ?thesis by simp

  1145 qed

  1146

  1147 lemma abs_minus_commute:

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

  1149 proof -

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

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

  1152   finally show ?thesis .

  1153 qed

  1154

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

  1156 by (rule abs_of_nonneg, rule less_imp_le)

  1157

  1158 lemma abs_of_nonpos [simp]:

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

  1160 proof -

  1161   let ?b = "- a"

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

  1163   unfolding abs_minus_cancel [of "?b"]

  1164   unfolding neg_le_0_iff_le [of "?b"]

  1165   unfolding minus_minus by (erule abs_of_nonneg)

  1166   then show ?thesis using assms by auto

  1167 qed

  1168

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

  1170 by (rule abs_of_nonpos, rule less_imp_le)

  1171

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

  1173 by (insert abs_ge_self, blast intro: order_trans)

  1174

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

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

  1177

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

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

  1180

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

  1182 proof -

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

  1184     by (simp add: algebra_simps add_diff_cancel)

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

  1186     by (simp add: abs_triangle_ineq)

  1187   then show ?thesis

  1188     by (simp add: algebra_simps)

  1189 qed

  1190

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

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

  1193

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

  1195   by (simp add: abs_le_iff abs_triangle_ineq2 abs_triangle_ineq2_sym)

  1196

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

  1198 proof -

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

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

  1201   finally show ?thesis by simp

  1202 qed

  1203

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

  1205 proof -

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

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

  1208   finally show ?thesis .

  1209 qed

  1210

  1211 lemma abs_add_abs [simp]:

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

  1213 proof (rule antisym)

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

  1215 next

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

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

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

  1219 qed

  1220

  1221 end

  1222

  1223

  1224 subsection {* Tools setup *}

  1225

  1226 lemma add_mono_thms_linordered_semiring [no_atp]:

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

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

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

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

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

  1232 by (rule add_mono, clarify+)+

  1233

  1234 lemma add_mono_thms_linordered_field [no_atp]:

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

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

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

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

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

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

  1241 by (auto intro: add_strict_right_mono add_strict_left_mono

  1242   add_less_le_mono add_le_less_mono add_strict_mono)

  1243

  1244 code_modulename SML

  1245   Groups Arith

  1246

  1247 code_modulename OCaml

  1248   Groups Arith

  1249

  1250 code_modulename Haskell

  1251   Groups Arith

  1252

  1253

  1254 text {* Legacy *}

  1255

  1256 lemmas diff_def = diff_minus

  1257

  1258 end