src/HOL/Groups.thy
 author haftmann Sun Jun 23 21:16:07 2013 +0200 (2013-06-23) changeset 52435 6646bb548c6b parent 52289 83ce5d2841e7 child 54147 97a8ff4e4ac9 permissions -rw-r--r--
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
     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 begin

    10

    11 subsection {* Fact collections *}

    12

    13 ML {*

    14 structure Ac_Simps = Named_Thms

    15 (

    16   val name = @{binding ac_simps}

    17   val description = "associativity and commutativity simplification rules"

    18 )

    19 *}

    20

    21 setup Ac_Simps.setup

    22

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

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

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

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

    27 group and ring equalities but also helps with inequalities.

    28

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

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

    31

    32 ML {*

    33 structure Algebra_Simps = Named_Thms

    34 (

    35   val name = @{binding algebra_simps}

    36   val description = "algebra simplification rules"

    37 )

    38 *}

    39

    40 setup Algebra_Simps.setup

    41

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

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

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

    45 more benign @{text algebra_simps}. *}

    46

    47 ML {*

    48 structure Field_Simps = Named_Thms

    49 (

    50   val name = @{binding field_simps}

    51   val description = "algebra simplification rules for fields"

    52 )

    53 *}

    54

    55 setup Field_Simps.setup

    56

    57

    58 subsection {* Abstract structures *}

    59

    60 text {*

    61   These locales provide basic structures for interpretation into

    62   bigger structures;  extensions require careful thinking, otherwise

    63   undesired effects may occur due to interpretation.

    64 *}

    65

    66 locale semigroup =

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

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

    69

    70 locale abel_semigroup = semigroup +

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

    72 begin

    73

    74 lemma left_commute [ac_simps]:

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

    76 proof -

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

    78     by (simp only: commute)

    79   then show ?thesis

    80     by (simp only: assoc)

    81 qed

    82

    83 end

    84

    85 locale monoid = semigroup +

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

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

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

    89

    90 locale comm_monoid = abel_semigroup +

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

    92   assumes comm_neutral: "a * 1 = a"

    93

    94 sublocale comm_monoid < monoid

    95   by default (simp_all add: commute comm_neutral)

    96

    97

    98 subsection {* Generic operations *}

    99

   100 class zero =

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

   102

   103 class one =

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

   105

   106 hide_const (open) zero one

   107

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

   109   unfolding Let_def ..

   110

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

   112   unfolding Let_def ..

   113

   114 setup {*

   115   Reorient_Proc.add

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

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

   118       | _ => false)

   119 *}

   120

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

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

   123

   124 typed_print_translation {*

   125   let

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

   127       if null ts andalso Printer.type_emphasis ctxt T then

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

   129           Syntax_Phases.term_of_typ ctxt T

   130       else raise Match);

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

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

   133

   134 class plus =

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

   136

   137 class minus =

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

   139

   140 class uminus =

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

   142

   143 class times =

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

   145

   146

   147 subsection {* Semigroups and Monoids *}

   148

   149 class semigroup_add = plus +

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

   151

   152 sublocale semigroup_add < add!: semigroup plus

   153   by default (fact add_assoc)

   154

   155 class ab_semigroup_add = semigroup_add +

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

   157

   158 sublocale ab_semigroup_add < add!: abel_semigroup plus

   159   by default (fact add_commute)

   160

   161 context ab_semigroup_add

   162 begin

   163

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

   165

   166 theorems add_ac = add_assoc add_commute add_left_commute

   167

   168 end

   169

   170 theorems add_ac = add_assoc add_commute add_left_commute

   171

   172 class semigroup_mult = times +

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

   174

   175 sublocale semigroup_mult < mult!: semigroup times

   176   by default (fact mult_assoc)

   177

   178 class ab_semigroup_mult = semigroup_mult +

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

   180

   181 sublocale ab_semigroup_mult < mult!: abel_semigroup times

   182   by default (fact mult_commute)

   183

   184 context ab_semigroup_mult

   185 begin

   186

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

   188

   189 theorems mult_ac = mult_assoc mult_commute mult_left_commute

   190

   191 end

   192

   193 theorems mult_ac = mult_assoc mult_commute mult_left_commute

   194

   195 class monoid_add = zero + semigroup_add +

   196   assumes add_0_left: "0 + a = a"

   197     and add_0_right: "a + 0 = a"

   198

   199 sublocale monoid_add < add!: monoid plus 0

   200   by default (fact add_0_left add_0_right)+

   201

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

   203 by (rule eq_commute)

   204

   205 class comm_monoid_add = zero + ab_semigroup_add +

   206   assumes add_0: "0 + a = a"

   207

   208 sublocale comm_monoid_add < add!: comm_monoid plus 0

   209   by default (insert add_0, simp add: ac_simps)

   210

   211 subclass (in comm_monoid_add) monoid_add

   212   by default (fact add.left_neutral add.right_neutral)+

   213

   214 class comm_monoid_diff = comm_monoid_add + minus +

   215   assumes diff_zero [simp]: "a - 0 = a"

   216     and zero_diff [simp]: "0 - a = 0"

   217     and add_diff_cancel_left [simp]: "(c + a) - (c + b) = a - b"

   218     and diff_diff_add: "a - b - c = a - (b + c)"

   219 begin

   220

   221 lemma add_diff_cancel_right [simp]:

   222   "(a + c) - (b + c) = a - b"

   223   using add_diff_cancel_left [symmetric] by (simp add: add.commute)

   224

   225 lemma add_diff_cancel_left' [simp]:

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

   227 proof -

   228   have "(b + a) - (b + 0) = a" by (simp only: add_diff_cancel_left diff_zero)

   229   then show ?thesis by simp

   230 qed

   231

   232 lemma add_diff_cancel_right' [simp]:

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

   234   using add_diff_cancel_left' [symmetric] by (simp add: add.commute)

   235

   236 lemma diff_add_zero [simp]:

   237   "a - (a + b) = 0"

   238 proof -

   239   have "a - (a + b) = (a + 0) - (a + b)" by simp

   240   also have "\<dots> = 0" by (simp only: add_diff_cancel_left zero_diff)

   241   finally show ?thesis .

   242 qed

   243

   244 lemma diff_cancel [simp]:

   245   "a - a = 0"

   246 proof -

   247   have "(a + 0) - (a + 0) = 0" by (simp only: add_diff_cancel_left diff_zero)

   248   then show ?thesis by simp

   249 qed

   250

   251 lemma diff_right_commute:

   252   "a - c - b = a - b - c"

   253   by (simp add: diff_diff_add add.commute)

   254

   255 lemma add_implies_diff:

   256   assumes "c + b = a"

   257   shows "c = a - b"

   258 proof -

   259   from assms have "(b + c) - (b + 0) = a - b" by (simp add: add.commute)

   260   then show "c = a - b" by simp

   261 qed

   262

   263 end

   264

   265 class monoid_mult = one + semigroup_mult +

   266   assumes mult_1_left: "1 * a  = a"

   267     and mult_1_right: "a * 1 = a"

   268

   269 sublocale monoid_mult < mult!: monoid times 1

   270   by default (fact mult_1_left mult_1_right)+

   271

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

   273 by (rule eq_commute)

   274

   275 class comm_monoid_mult = one + ab_semigroup_mult +

   276   assumes mult_1: "1 * a = a"

   277

   278 sublocale comm_monoid_mult < mult!: comm_monoid times 1

   279   by default (insert mult_1, simp add: ac_simps)

   280

   281 subclass (in comm_monoid_mult) monoid_mult

   282   by default (fact mult.left_neutral mult.right_neutral)+

   283

   284 class cancel_semigroup_add = semigroup_add +

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

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

   287 begin

   288

   289 lemma add_left_cancel [simp]:

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

   291 by (blast dest: add_left_imp_eq)

   292

   293 lemma add_right_cancel [simp]:

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

   295 by (blast dest: add_right_imp_eq)

   296

   297 end

   298

   299 class cancel_ab_semigroup_add = ab_semigroup_add +

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

   301 begin

   302

   303 subclass cancel_semigroup_add

   304 proof

   305   fix a b c :: 'a

   306   assume "a + b = a + c"

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

   308 next

   309   fix a b c :: 'a

   310   assume "b + a = c + a"

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

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

   313 qed

   314

   315 end

   316

   317 class cancel_comm_monoid_add = cancel_ab_semigroup_add + comm_monoid_add

   318

   319

   320 subsection {* Groups *}

   321

   322 class group_add = minus + uminus + monoid_add +

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

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

   325 begin

   326

   327 lemma minus_unique:

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

   329 proof -

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

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

   332   finally show ?thesis .

   333 qed

   334

   335 lemmas equals_zero_I = minus_unique (* legacy name *)

   336

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

   338 proof -

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

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

   341 qed

   342

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

   344 proof -

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

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

   347 qed

   348

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

   350 proof -

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

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

   353   finally show ?thesis .

   354 qed

   355

   356 subclass cancel_semigroup_add

   357 proof

   358   fix a b c :: 'a

   359   assume "a + b = a + c"

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

   361     unfolding add_assoc by simp

   362   then show "b = c" by simp

   363 next

   364   fix a b c :: 'a

   365   assume "b + a = c + a"

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

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

   368 qed

   369

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

   371 by (simp add: add_assoc [symmetric])

   372

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

   374 by (simp add: add_assoc [symmetric])

   375

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

   377 proof -

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

   379     by (simp add: add_assoc add_minus_cancel)

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

   381     by (rule minus_unique)

   382 qed

   383

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

   385 proof

   386   assume "a - b = 0"

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

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

   389   finally show "a = b" .

   390 next

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

   392 qed

   393

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

   395 by (simp add: diff_minus)

   396

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

   398 by (simp add: diff_minus)

   399

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

   401 by (simp add: diff_minus)

   402

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

   404 by (simp add: diff_minus)

   405

   406 lemma neg_equal_iff_equal [simp]:

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

   408 proof

   409   assume "- a = - b"

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

   411   thus "a = b" by simp

   412 next

   413   assume "a = b"

   414   thus "- a = - b" by simp

   415 qed

   416

   417 lemma neg_equal_0_iff_equal [simp]:

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

   419 by (subst neg_equal_iff_equal [symmetric], simp)

   420

   421 lemma neg_0_equal_iff_equal [simp]:

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

   423 by (subst neg_equal_iff_equal [symmetric], simp)

   424

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

   426

   427 lemma equation_minus_iff:

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

   429 proof -

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

   431   thus ?thesis by (simp add: eq_commute)

   432 qed

   433

   434 lemma minus_equation_iff:

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

   436 proof -

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

   438   thus ?thesis by (simp add: eq_commute)

   439 qed

   440

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

   442 by (simp add: diff_minus add_assoc)

   443

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

   445 by (simp add: diff_minus add_assoc)

   446

   447 declare diff_minus[symmetric, algebra_simps, field_simps]

   448

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

   450 proof

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

   452 next

   453   assume "a + b = 0"

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

   455     by (simp only: add_assoc)

   456   ultimately show "a = - b" by simp

   457 qed

   458

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

   460   unfolding eq_neg_iff_add_eq_0 [symmetric]

   461   by (rule equation_minus_iff)

   462

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

   464   by (simp add: diff_minus minus_add)

   465

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

   467   by (simp add: diff_minus add_assoc)

   468

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

   470   by (auto simp add: diff_minus add_assoc)

   471

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

   473   by (auto simp add: diff_minus add_assoc)

   474

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

   476   by (simp add: diff_minus minus_add add_assoc)

   477

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

   479   by (fact right_minus_eq [symmetric])

   480

   481 lemma diff_eq_diff_eq:

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

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

   484

   485 end

   486

   487 class ab_group_add = minus + uminus + comm_monoid_add +

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

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

   490 begin

   491

   492 subclass group_add

   493   proof qed (simp_all add: ab_left_minus ab_diff_minus)

   494

   495 subclass cancel_comm_monoid_add

   496 proof

   497   fix a b c :: 'a

   498   assume "a + b = a + c"

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

   500     unfolding add_assoc by simp

   501   then show "b = c" by simp

   502 qed

   503

   504 lemma uminus_add_conv_diff[algebra_simps, field_simps]:

   505   "- a + b = b - a"

   506 by (simp add:diff_minus add_commute)

   507

   508 lemma minus_add_distrib [simp]:

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

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

   511

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

   513 by (simp add: diff_minus add_ac)

   514

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

   516 by (simp add: diff_minus add_ac)

   517

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

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

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

   521   by (rule right_minus_eq)

   522

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

   524   by (simp add: diff_minus add_ac)

   525

   526 end

   527

   528

   529 subsection {* (Partially) Ordered Groups *}

   530

   531 text {*

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

   533   \begin{itemize}

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

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

   536   \end{itemize}

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

   538   \begin{itemize}

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

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

   541   \end{itemize}

   542 *}

   543

   544 class ordered_ab_semigroup_add = order + ab_semigroup_add +

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

   546 begin

   547

   548 lemma add_right_mono:

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

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

   551

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

   553 lemma add_mono:

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

   555   apply (erule add_right_mono [THEN order_trans])

   556   apply (simp add: add_commute add_left_mono)

   557   done

   558

   559 end

   560

   561 class ordered_cancel_ab_semigroup_add =

   562   ordered_ab_semigroup_add + cancel_ab_semigroup_add

   563 begin

   564

   565 lemma add_strict_left_mono:

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

   567 by (auto simp add: less_le add_left_mono)

   568

   569 lemma add_strict_right_mono:

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

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

   572

   573 text{*Strict monotonicity in both arguments*}

   574 lemma add_strict_mono:

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

   576 apply (erule add_strict_right_mono [THEN less_trans])

   577 apply (erule add_strict_left_mono)

   578 done

   579

   580 lemma add_less_le_mono:

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

   582 apply (erule add_strict_right_mono [THEN less_le_trans])

   583 apply (erule add_left_mono)

   584 done

   585

   586 lemma add_le_less_mono:

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

   588 apply (erule add_right_mono [THEN le_less_trans])

   589 apply (erule add_strict_left_mono)

   590 done

   591

   592 end

   593

   594 class ordered_ab_semigroup_add_imp_le =

   595   ordered_cancel_ab_semigroup_add +

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

   597 begin

   598

   599 lemma add_less_imp_less_left:

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

   601 proof -

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

   603   have "a <= b"

   604     apply (insert le)

   605     apply (drule add_le_imp_le_left)

   606     by (insert le, drule add_le_imp_le_left, assumption)

   607   moreover have "a \<noteq> b"

   608   proof (rule ccontr)

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

   610     then have "a = b" by simp

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

   612     with less show "False"by simp

   613   qed

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

   615 qed

   616

   617 lemma add_less_imp_less_right:

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

   619 apply (rule add_less_imp_less_left [of c])

   620 apply (simp add: add_commute)

   621 done

   622

   623 lemma add_less_cancel_left [simp]:

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

   625 by (blast intro: add_less_imp_less_left add_strict_left_mono)

   626

   627 lemma add_less_cancel_right [simp]:

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

   629 by (blast intro: add_less_imp_less_right add_strict_right_mono)

   630

   631 lemma add_le_cancel_left [simp]:

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

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

   634

   635 lemma add_le_cancel_right [simp]:

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

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

   638

   639 lemma add_le_imp_le_right:

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

   641 by simp

   642

   643 lemma max_add_distrib_left:

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

   645   unfolding max_def by auto

   646

   647 lemma min_add_distrib_left:

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

   649   unfolding min_def by auto

   650

   651 lemma max_add_distrib_right:

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

   653   unfolding max_def by auto

   654

   655 lemma min_add_distrib_right:

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

   657   unfolding min_def by auto

   658

   659 end

   660

   661 class ordered_cancel_comm_monoid_diff = comm_monoid_diff + ordered_ab_semigroup_add_imp_le +

   662   assumes le_iff_add: "a \<le> b \<longleftrightarrow> (\<exists>c. b = a + c)"

   663 begin

   664

   665 context

   666   fixes a b

   667   assumes "a \<le> b"

   668 begin

   669

   670 lemma add_diff_inverse:

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

   672   using a \<le> b by (auto simp add: le_iff_add)

   673

   674 lemma add_diff_assoc:

   675   "c + (b - a) = c + b - a"

   676   using a \<le> b by (auto simp add: le_iff_add add_left_commute [of c])

   677

   678 lemma add_diff_assoc2:

   679   "b - a + c = b + c - a"

   680   using a \<le> b by (auto simp add: le_iff_add add_assoc)

   681

   682 lemma diff_add_assoc:

   683   "c + b - a = c + (b - a)"

   684   using a \<le> b by (simp add: add_commute add_diff_assoc)

   685

   686 lemma diff_add_assoc2:

   687   "b + c - a = b - a + c"

   688   using a \<le> bby (simp add: add_commute add_diff_assoc)

   689

   690 lemma diff_diff_right:

   691   "c - (b - a) = c + a - b"

   692   by (simp add: add_diff_inverse add_diff_cancel_left [of a c "b - a", symmetric] add_commute)

   693

   694 lemma diff_add:

   695   "b - a + a = b"

   696   by (simp add: add_commute add_diff_inverse)

   697

   698 lemma le_add_diff:

   699   "c \<le> b + c - a"

   700   by (auto simp add: add_commute diff_add_assoc2 le_iff_add)

   701

   702 lemma le_imp_diff_is_add:

   703   "a \<le> b \<Longrightarrow> b - a = c \<longleftrightarrow> b = c + a"

   704   by (auto simp add: add_commute add_diff_inverse)

   705

   706 lemma le_diff_conv2:

   707   "c \<le> b - a \<longleftrightarrow> c + a \<le> b" (is "?P \<longleftrightarrow> ?Q")

   708 proof

   709   assume ?P

   710   then have "c + a \<le> b - a + a" by (rule add_right_mono)

   711   then show ?Q by (simp add: add_diff_inverse add_commute)

   712 next

   713   assume ?Q

   714   then have "a + c \<le> a + (b - a)" by (simp add: add_diff_inverse add_commute)

   715   then show ?P by simp

   716 qed

   717

   718 end

   719

   720 end

   721

   722

   723 subsection {* Support for reasoning about signs *}

   724

   725 class ordered_comm_monoid_add =

   726   ordered_cancel_ab_semigroup_add + comm_monoid_add

   727 begin

   728

   729 lemma add_pos_nonneg:

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

   731 proof -

   732   have "0 + 0 < a + b"

   733     using assms by (rule add_less_le_mono)

   734   then show ?thesis by simp

   735 qed

   736

   737 lemma add_pos_pos:

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

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

   740

   741 lemma add_nonneg_pos:

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

   743 proof -

   744   have "0 + 0 < a + b"

   745     using assms by (rule add_le_less_mono)

   746   then show ?thesis by simp

   747 qed

   748

   749 lemma add_nonneg_nonneg [simp]:

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

   751 proof -

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

   753     using assms by (rule add_mono)

   754   then show ?thesis by simp

   755 qed

   756

   757 lemma add_neg_nonpos:

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

   759 proof -

   760   have "a + b < 0 + 0"

   761     using assms by (rule add_less_le_mono)

   762   then show ?thesis by simp

   763 qed

   764

   765 lemma add_neg_neg:

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

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

   768

   769 lemma add_nonpos_neg:

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

   771 proof -

   772   have "a + b < 0 + 0"

   773     using assms by (rule add_le_less_mono)

   774   then show ?thesis by simp

   775 qed

   776

   777 lemma add_nonpos_nonpos:

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

   779 proof -

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

   781     using assms by (rule add_mono)

   782   then show ?thesis by simp

   783 qed

   784

   785 lemmas add_sign_intros =

   786   add_pos_nonneg add_pos_pos add_nonneg_pos add_nonneg_nonneg

   787   add_neg_nonpos add_neg_neg add_nonpos_neg add_nonpos_nonpos

   788

   789 lemma add_nonneg_eq_0_iff:

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

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

   792 proof (intro iffI conjI)

   793   have "x = x + 0" by simp

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

   795   also assume "x + y = 0"

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

   797   finally show "x = 0" .

   798 next

   799   have "y = 0 + y" by simp

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

   801   also assume "x + y = 0"

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

   803   finally show "y = 0" .

   804 next

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

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

   807 qed

   808

   809 end

   810

   811 class ordered_ab_group_add =

   812   ab_group_add + ordered_ab_semigroup_add

   813 begin

   814

   815 subclass ordered_cancel_ab_semigroup_add ..

   816

   817 subclass ordered_ab_semigroup_add_imp_le

   818 proof

   819   fix a b c :: 'a

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

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

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

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

   824 qed

   825

   826 subclass ordered_comm_monoid_add ..

   827

   828 lemma max_diff_distrib_left:

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

   830 by (simp add: diff_minus, rule max_add_distrib_left)

   831

   832 lemma min_diff_distrib_left:

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

   834 by (simp add: diff_minus, rule min_add_distrib_left)

   835

   836 lemma le_imp_neg_le:

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

   838 proof -

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

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

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

   842   thus ?thesis by (simp add: add_assoc)

   843 qed

   844

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

   846 proof

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

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

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

   850 next

   851   assume "a\<le>b"

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

   853 qed

   854

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

   856 by (subst neg_le_iff_le [symmetric], simp)

   857

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

   859 by (subst neg_le_iff_le [symmetric], simp)

   860

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

   862 by (force simp add: less_le)

   863

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

   865 by (subst neg_less_iff_less [symmetric], simp)

   866

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

   868 by (subst neg_less_iff_less [symmetric], simp)

   869

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

   871

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

   873 proof -

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

   875   thus ?thesis by simp

   876 qed

   877

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

   879 proof -

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

   881   thus ?thesis by simp

   882 qed

   883

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

   885 proof -

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

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

   888     apply (auto simp only: le_less)

   889     apply (drule mm)

   890     apply (simp_all)

   891     apply (drule mm[simplified], assumption)

   892     done

   893   then show ?thesis by simp

   894 qed

   895

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

   897 by (auto simp add: le_less minus_less_iff)

   898

   899 lemma diff_less_0_iff_less [simp, no_atp]:

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

   901 proof -

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

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

   904   finally show ?thesis .

   905 qed

   906

   907 lemmas less_iff_diff_less_0 = diff_less_0_iff_less [symmetric]

   908

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

   910 apply (subst less_iff_diff_less_0 [of a])

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

   912 apply (simp add: diff_minus add_ac)

   913 done

   914

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

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

   917 apply (subst less_iff_diff_less_0 [of a])

   918 apply (simp add: diff_minus add_ac)

   919 done

   920

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

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

   923

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

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

   926

   927 lemma diff_le_0_iff_le [simp, no_atp]:

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

   929   by (simp add: algebra_simps)

   930

   931 lemmas le_iff_diff_le_0 = diff_le_0_iff_le [symmetric]

   932

   933 lemma diff_eq_diff_less:

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

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

   936

   937 lemma diff_eq_diff_less_eq:

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

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

   940

   941 end

   942

   943 ML_file "Tools/group_cancel.ML"

   944

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

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

   947

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

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

   950

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

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

   953

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

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

   956

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

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

   959

   960 class linordered_ab_semigroup_add =

   961   linorder + ordered_ab_semigroup_add

   962

   963 class linordered_cancel_ab_semigroup_add =

   964   linorder + ordered_cancel_ab_semigroup_add

   965 begin

   966

   967 subclass linordered_ab_semigroup_add ..

   968

   969 subclass ordered_ab_semigroup_add_imp_le

   970 proof

   971   fix a b c :: 'a

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

   973   show "a <= b"

   974   proof (rule ccontr)

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

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

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

   978     have "a = b"

   979       apply (insert le)

   980       apply (insert le2)

   981       apply (drule antisym, simp_all)

   982       done

   983     with w show False

   984       by (simp add: linorder_not_le [symmetric])

   985   qed

   986 qed

   987

   988 end

   989

   990 class linordered_ab_group_add = linorder + ordered_ab_group_add

   991 begin

   992

   993 subclass linordered_cancel_ab_semigroup_add ..

   994

   995 lemma neg_less_eq_nonneg [simp]:

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

   997 proof

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

   999   proof (rule classical)

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

  1001     then have "a < 0" by auto

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

  1003     then show ?thesis by auto

  1004   qed

  1005 next

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

  1007   proof (rule order_trans)

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

  1009   next

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

  1011   qed

  1012 qed

  1013

  1014 lemma neg_less_nonneg [simp]:

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

  1016 proof

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

  1018   proof (rule classical)

  1019     assume "\<not> 0 < a"

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

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

  1022     then show ?thesis by auto

  1023   qed

  1024 next

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

  1026   proof (rule less_trans)

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

  1028   next

  1029     show "0 < a" using A .

  1030   qed

  1031 qed

  1032

  1033 lemma less_eq_neg_nonpos [simp]:

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

  1035 proof

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

  1037   proof (rule classical)

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

  1039     then have "0 < a" by auto

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

  1041     then show ?thesis by auto

  1042   qed

  1043 next

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

  1045   proof (rule order_trans)

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

  1047   next

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

  1049   qed

  1050 qed

  1051

  1052 lemma equal_neg_zero [simp]:

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

  1054 proof

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

  1056 next

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

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

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

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

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

  1062   next

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

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

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

  1066   qed

  1067 qed

  1068

  1069 lemma neg_equal_zero [simp]:

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

  1071   by (auto dest: sym)

  1072

  1073 lemma double_zero [simp]:

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

  1075 proof

  1076   assume assm: "a + a = 0"

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

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

  1079 qed simp

  1080

  1081 lemma double_zero_sym [simp]:

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

  1083   by (rule, drule sym) simp_all

  1084

  1085 lemma zero_less_double_add_iff_zero_less_single_add [simp]:

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

  1087 proof

  1088   assume "0 < a + a"

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

  1090   then have "- a < a" by simp

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

  1092 next

  1093   assume "0 < a"

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

  1095     by (rule add_strict_mono)

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

  1097 qed

  1098

  1099 lemma zero_le_double_add_iff_zero_le_single_add [simp]:

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

  1101   by (auto simp add: le_less)

  1102

  1103 lemma double_add_less_zero_iff_single_add_less_zero [simp]:

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

  1105 proof -

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

  1107     by (simp add: not_less)

  1108   then show ?thesis by simp

  1109 qed

  1110

  1111 lemma double_add_le_zero_iff_single_add_le_zero [simp]:

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

  1113 proof -

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

  1115     by (simp add: not_le)

  1116   then show ?thesis by simp

  1117 qed

  1118

  1119 lemma le_minus_self_iff:

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

  1121 proof -

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

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

  1124     by (simp add: add_assoc [symmetric])

  1125   thus ?thesis by simp

  1126 qed

  1127

  1128 lemma minus_le_self_iff:

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

  1130 proof -

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

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

  1133     by (simp add: add_assoc [symmetric])

  1134   thus ?thesis by simp

  1135 qed

  1136

  1137 lemma minus_max_eq_min:

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

  1139   by (auto simp add: max_def min_def)

  1140

  1141 lemma minus_min_eq_max:

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

  1143   by (auto simp add: max_def min_def)

  1144

  1145 end

  1146

  1147 context ordered_comm_monoid_add

  1148 begin

  1149

  1150 lemma add_increasing:

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

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

  1153

  1154 lemma add_increasing2:

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

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

  1157

  1158 lemma add_strict_increasing:

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

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

  1161

  1162 lemma add_strict_increasing2:

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

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

  1165

  1166 end

  1167

  1168 class abs =

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

  1170 begin

  1171

  1172 notation (xsymbols)

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

  1174

  1175 notation (HTML output)

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

  1177

  1178 end

  1179

  1180 class sgn =

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

  1182

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

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

  1185

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

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

  1188 begin

  1189

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

  1191   by (simp add:sgn_if)

  1192

  1193 end

  1194

  1195 class ordered_ab_group_add_abs = ordered_ab_group_add + abs +

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

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

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

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

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

  1201 begin

  1202

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

  1204   unfolding neg_le_0_iff_le by simp

  1205

  1206 lemma abs_of_nonneg [simp]:

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

  1208 proof (rule antisym)

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

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

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

  1212 qed (rule abs_ge_self)

  1213

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

  1215 by (rule antisym)

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

  1217

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

  1219 proof -

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

  1221   proof (rule antisym)

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

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

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

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

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

  1227   qed

  1228   then show ?thesis by auto

  1229 qed

  1230

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

  1232 by simp

  1233

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

  1235 proof -

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

  1237   thus ?thesis by simp

  1238 qed

  1239

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

  1241 proof

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

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

  1244   thus "a = 0" by simp

  1245 next

  1246   assume "a = 0"

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

  1248 qed

  1249

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

  1251 by (simp add: less_le)

  1252

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

  1254 proof -

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

  1256   show ?thesis by (simp add: a)

  1257 qed

  1258

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

  1260 proof -

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

  1262   then show ?thesis by simp

  1263 qed

  1264

  1265 lemma abs_minus_commute:

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

  1267 proof -

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

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

  1270   finally show ?thesis .

  1271 qed

  1272

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

  1274 by (rule abs_of_nonneg, rule less_imp_le)

  1275

  1276 lemma abs_of_nonpos [simp]:

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

  1278 proof -

  1279   let ?b = "- a"

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

  1281   unfolding abs_minus_cancel [of "?b"]

  1282   unfolding neg_le_0_iff_le [of "?b"]

  1283   unfolding minus_minus by (erule abs_of_nonneg)

  1284   then show ?thesis using assms by auto

  1285 qed

  1286

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

  1288 by (rule abs_of_nonpos, rule less_imp_le)

  1289

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

  1291 by (insert abs_ge_self, blast intro: order_trans)

  1292

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

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

  1295

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

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

  1298

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

  1300 proof -

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

  1302     by (simp add: algebra_simps add_diff_cancel)

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

  1304     by (simp add: abs_triangle_ineq)

  1305   then show ?thesis

  1306     by (simp add: algebra_simps)

  1307 qed

  1308

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

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

  1311

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

  1313   by (simp add: abs_le_iff abs_triangle_ineq2 abs_triangle_ineq2_sym)

  1314

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

  1316 proof -

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

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

  1319   finally show ?thesis by simp

  1320 qed

  1321

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

  1323 proof -

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

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

  1326   finally show ?thesis .

  1327 qed

  1328

  1329 lemma abs_add_abs [simp]:

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

  1331 proof (rule antisym)

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

  1333 next

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

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

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

  1337 qed

  1338

  1339 end

  1340

  1341

  1342 subsection {* Tools setup *}

  1343

  1344 lemma add_mono_thms_linordered_semiring [no_atp]:

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

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

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

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

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

  1350 by (rule add_mono, clarify+)+

  1351

  1352 lemma add_mono_thms_linordered_field [no_atp]:

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

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

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

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

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

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

  1359 by (auto intro: add_strict_right_mono add_strict_left_mono

  1360   add_less_le_mono add_le_less_mono add_strict_mono)

  1361

  1362 code_identifier

  1363   code_module Groups \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith

  1364

  1365

  1366 text {* Legacy *}

  1367

  1368 lemmas diff_def = diff_minus

  1369

  1370 end

  1371