src/HOL/Groups.thy
 author haftmann Thu Jan 08 18:23:29 2015 +0100 (2015-01-08) changeset 59322 8ccecf1415b0 parent 58889 5b7a9633cfa8 child 59557 ebd8ecacfba6 permissions -rw-r--r--
tuned order
     1 (*  Title:   HOL/Groups.thy

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

     3 *)

     4

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

     6

     7 theory Groups

     8 imports Orderings

     9 begin

    10

    11 subsection {* Dynamic facts *}

    12

    13 named_theorems ac_simps "associativity and commutativity simplification rules"

    14

    15

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

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

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

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

    20 group and ring equalities but also helps with inequalities.

    21

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

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

    24

    25 named_theorems algebra_simps "algebra simplification rules"

    26

    27

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

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

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

    31 more benign @{text algebra_simps}. *}

    32

    33 named_theorems field_simps "algebra simplification rules for fields"

    34

    35

    36 subsection {* Abstract structures *}

    37

    38 text {*

    39   These locales provide basic structures for interpretation into

    40   bigger structures;  extensions require careful thinking, otherwise

    41   undesired effects may occur due to interpretation.

    42 *}

    43

    44 locale semigroup =

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

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

    47

    48 locale abel_semigroup = semigroup +

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

    50 begin

    51

    52 lemma left_commute [ac_simps]:

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

    54 proof -

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

    56     by (simp only: commute)

    57   then show ?thesis

    58     by (simp only: assoc)

    59 qed

    60

    61 end

    62

    63 locale monoid = semigroup +

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

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

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

    67

    68 locale comm_monoid = abel_semigroup +

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

    70   assumes comm_neutral: "a * 1 = a"

    71 begin

    72

    73 sublocale monoid

    74   by default (simp_all add: commute comm_neutral)

    75

    76 end

    77

    78

    79 subsection {* Generic operations *}

    80

    81 class zero =

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

    83

    84 class one =

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

    86

    87 hide_const (open) zero one

    88

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

    90   unfolding Let_def ..

    91

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

    93   unfolding Let_def ..

    94

    95 setup {*

    96   Reorient_Proc.add

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

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

    99       | _ => false)

   100 *}

   101

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

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

   104

   105 typed_print_translation {*

   106   let

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

   108       if null ts andalso Printer.type_emphasis ctxt T then

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

   110           Syntax_Phases.term_of_typ ctxt T

   111       else raise Match);

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

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

   114

   115 class plus =

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

   117

   118 class minus =

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

   120

   121 class uminus =

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

   123

   124 class times =

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

   126

   127

   128 subsection {* Semigroups and Monoids *}

   129

   130 class semigroup_add = plus +

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

   132 begin

   133

   134 sublocale add!: semigroup plus

   135   by default (fact add_assoc)

   136

   137 end

   138

   139 hide_fact add_assoc

   140

   141 class ab_semigroup_add = semigroup_add +

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

   143 begin

   144

   145 sublocale add!: abel_semigroup plus

   146   by default (fact add_commute)

   147

   148 declare add.left_commute [algebra_simps, field_simps]

   149

   150 theorems add_ac = add.assoc add.commute add.left_commute

   151

   152 end

   153

   154 hide_fact add_commute

   155

   156 theorems add_ac = add.assoc add.commute add.left_commute

   157

   158 class semigroup_mult = times +

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

   160 begin

   161

   162 sublocale mult!: semigroup times

   163   by default (fact mult_assoc)

   164

   165 end

   166

   167 hide_fact mult_assoc

   168

   169 class ab_semigroup_mult = semigroup_mult +

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

   171 begin

   172

   173 sublocale mult!: abel_semigroup times

   174   by default (fact mult_commute)

   175

   176 declare mult.left_commute [algebra_simps, field_simps]

   177

   178 theorems mult_ac = mult.assoc mult.commute mult.left_commute

   179

   180 end

   181

   182 hide_fact mult_commute

   183

   184 theorems mult_ac = mult.assoc mult.commute mult.left_commute

   185

   186 class monoid_add = zero + semigroup_add +

   187   assumes add_0_left: "0 + a = a"

   188     and add_0_right: "a + 0 = a"

   189 begin

   190

   191 sublocale add!: monoid plus 0

   192   by default (fact add_0_left add_0_right)+

   193

   194 end

   195

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

   197   by (fact eq_commute)

   198

   199 class comm_monoid_add = zero + ab_semigroup_add +

   200   assumes add_0: "0 + a = a"

   201 begin

   202

   203 sublocale add!: comm_monoid plus 0

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

   205

   206 subclass monoid_add

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

   208

   209 end

   210

   211 class monoid_mult = one + semigroup_mult +

   212   assumes mult_1_left: "1 * a  = a"

   213     and mult_1_right: "a * 1 = a"

   214 begin

   215

   216 sublocale mult!: monoid times 1

   217   by default (fact mult_1_left mult_1_right)+

   218

   219 end

   220

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

   222   by (fact eq_commute)

   223

   224 class comm_monoid_mult = one + ab_semigroup_mult +

   225   assumes mult_1: "1 * a = a"

   226 begin

   227

   228 sublocale mult!: comm_monoid times 1

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

   230

   231 subclass monoid_mult

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

   233

   234 end

   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 class comm_monoid_diff = comm_monoid_add + minus +

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

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

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

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

   276 begin

   277

   278 lemma add_diff_cancel_right [simp]:

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

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

   281

   282 lemma add_diff_cancel_left' [simp]:

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

   284 proof -

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

   286   then show ?thesis by simp

   287 qed

   288

   289 lemma add_diff_cancel_right' [simp]:

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

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

   292

   293 lemma diff_add_zero [simp]:

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

   295 proof -

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

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

   298   finally show ?thesis .

   299 qed

   300

   301 lemma diff_cancel [simp]:

   302   "a - a = 0"

   303 proof -

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

   305   then show ?thesis by simp

   306 qed

   307

   308 lemma diff_right_commute:

   309   "a - c - b = a - b - c"

   310   by (simp add: diff_diff_add add.commute)

   311

   312 lemma add_implies_diff:

   313   assumes "c + b = a"

   314   shows "c = a - b"

   315 proof -

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

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

   318 qed

   319

   320 end

   321

   322

   323 subsection {* Groups *}

   324

   325 class group_add = minus + uminus + monoid_add +

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

   327   assumes add_uminus_conv_diff [simp]: "a + (- b) = a - b"

   328 begin

   329

   330 lemma diff_conv_add_uminus:

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

   332   by simp

   333

   334 lemma minus_unique:

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

   336 proof -

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

   338   also have "\<dots> = b" by (simp add: add.assoc [symmetric])

   339   finally show ?thesis .

   340 qed

   341

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

   343 proof -

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

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

   346 qed

   347

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

   349 proof -

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

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

   352 qed

   353

   354 lemma right_minus: "a + - a = 0"

   355 proof -

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

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

   358   finally show ?thesis .

   359 qed

   360

   361 lemma diff_self [simp]:

   362   "a - a = 0"

   363   using right_minus [of a] by simp

   364

   365 subclass cancel_semigroup_add

   366 proof

   367   fix a b c :: 'a

   368   assume "a + b = a + c"

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

   370     unfolding add.assoc by simp

   371   then show "b = c" by simp

   372 next

   373   fix a b c :: 'a

   374   assume "b + a = c + a"

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

   376   then show "b = c" unfolding add.assoc by simp

   377 qed

   378

   379 lemma minus_add_cancel [simp]:

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

   381   by (simp add: add.assoc [symmetric])

   382

   383 lemma add_minus_cancel [simp]:

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

   385   by (simp add: add.assoc [symmetric])

   386

   387 lemma diff_add_cancel [simp]:

   388   "a - b + b = a"

   389   by (simp only: diff_conv_add_uminus add.assoc) simp

   390

   391 lemma add_diff_cancel [simp]:

   392   "a + b - b = a"

   393   by (simp only: diff_conv_add_uminus add.assoc) simp

   394

   395 lemma minus_add:

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

   397 proof -

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

   399     by (simp only: add.assoc add_minus_cancel) simp

   400   then show "- (a + b) = - b + - a"

   401     by (rule minus_unique)

   402 qed

   403

   404 lemma right_minus_eq [simp]:

   405   "a - b = 0 \<longleftrightarrow> a = b"

   406 proof

   407   assume "a - b = 0"

   408   have "a = (a - b) + b" by (simp add: add.assoc)

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

   410   finally show "a = b" .

   411 next

   412   assume "a = b" thus "a - b = 0" by simp

   413 qed

   414

   415 lemma eq_iff_diff_eq_0:

   416   "a = b \<longleftrightarrow> a - b = 0"

   417   by (fact right_minus_eq [symmetric])

   418

   419 lemma diff_0 [simp]:

   420   "0 - a = - a"

   421   by (simp only: diff_conv_add_uminus add_0_left)

   422

   423 lemma diff_0_right [simp]:

   424   "a - 0 = a"

   425   by (simp only: diff_conv_add_uminus minus_zero add_0_right)

   426

   427 lemma diff_minus_eq_add [simp]:

   428   "a - - b = a + b"

   429   by (simp only: diff_conv_add_uminus minus_minus)

   430

   431 lemma neg_equal_iff_equal [simp]:

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

   433 proof

   434   assume "- a = - b"

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

   436   thus "a = b" by simp

   437 next

   438   assume "a = b"

   439   thus "- a = - b" by simp

   440 qed

   441

   442 lemma neg_equal_0_iff_equal [simp]:

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

   444   by (subst neg_equal_iff_equal [symmetric]) simp

   445

   446 lemma neg_0_equal_iff_equal [simp]:

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

   448   by (subst neg_equal_iff_equal [symmetric]) simp

   449

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

   451

   452 lemma equation_minus_iff:

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

   454 proof -

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

   456   thus ?thesis by (simp add: eq_commute)

   457 qed

   458

   459 lemma minus_equation_iff:

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

   461 proof -

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

   463   thus ?thesis by (simp add: eq_commute)

   464 qed

   465

   466 lemma eq_neg_iff_add_eq_0:

   467   "a = - b \<longleftrightarrow> a + b = 0"

   468 proof

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

   470 next

   471   assume "a + b = 0"

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

   473     by (simp only: add.assoc)

   474   ultimately show "a = - b" by simp

   475 qed

   476

   477 lemma add_eq_0_iff2:

   478   "a + b = 0 \<longleftrightarrow> a = - b"

   479   by (fact eq_neg_iff_add_eq_0 [symmetric])

   480

   481 lemma neg_eq_iff_add_eq_0:

   482   "- a = b \<longleftrightarrow> a + b = 0"

   483   by (auto simp add: add_eq_0_iff2)

   484

   485 lemma add_eq_0_iff:

   486   "a + b = 0 \<longleftrightarrow> b = - a"

   487   by (auto simp add: neg_eq_iff_add_eq_0 [symmetric])

   488

   489 lemma minus_diff_eq [simp]:

   490   "- (a - b) = b - a"

   491   by (simp only: neg_eq_iff_add_eq_0 diff_conv_add_uminus add.assoc minus_add_cancel) simp

   492

   493 lemma add_diff_eq [algebra_simps, field_simps]:

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

   495   by (simp only: diff_conv_add_uminus add.assoc)

   496

   497 lemma diff_add_eq_diff_diff_swap:

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

   499   by (simp only: diff_conv_add_uminus add.assoc minus_add)

   500

   501 lemma diff_eq_eq [algebra_simps, field_simps]:

   502   "a - b = c \<longleftrightarrow> a = c + b"

   503   by auto

   504

   505 lemma eq_diff_eq [algebra_simps, field_simps]:

   506   "a = c - b \<longleftrightarrow> a + b = c"

   507   by auto

   508

   509 lemma diff_diff_eq2 [algebra_simps, field_simps]:

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

   511   by (simp only: diff_conv_add_uminus add.assoc) simp

   512

   513 lemma diff_eq_diff_eq:

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

   515   by (simp only: eq_iff_diff_eq_0 [of a b] eq_iff_diff_eq_0 [of c d])

   516

   517 end

   518

   519 class ab_group_add = minus + uminus + comm_monoid_add +

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

   521   assumes ab_add_uminus_conv_diff: "a - b = a + (- b)"

   522 begin

   523

   524 subclass group_add

   525   proof qed (simp_all add: ab_left_minus ab_add_uminus_conv_diff)

   526

   527 subclass cancel_comm_monoid_add

   528 proof

   529   fix a b c :: 'a

   530   assume "a + b = a + c"

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

   532     by (simp only: add.assoc)

   533   then show "b = c" by simp

   534 qed

   535

   536 lemma uminus_add_conv_diff [simp]:

   537   "- a + b = b - a"

   538   by (simp add: add.commute)

   539

   540 lemma minus_add_distrib [simp]:

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

   542   by (simp add: algebra_simps)

   543

   544 lemma diff_add_eq [algebra_simps, field_simps]:

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

   546   by (simp add: algebra_simps)

   547

   548 lemma diff_diff_eq [algebra_simps, field_simps]:

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

   550   by (simp add: algebra_simps)

   551

   552 lemma diff_add_eq_diff_diff:

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

   554   using diff_add_eq_diff_diff_swap [of a c b] by (simp add: add.commute)

   555

   556 lemma add_diff_cancel_left [simp]:

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

   558   by (simp add: algebra_simps)

   559

   560 end

   561

   562

   563 subsection {* (Partially) Ordered Groups *}

   564

   565 text {*

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

   567   \begin{itemize}

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

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

   570   \end{itemize}

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

   572   \begin{itemize}

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

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

   575   \end{itemize}

   576 *}

   577

   578 class ordered_ab_semigroup_add = order + ab_semigroup_add +

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

   580 begin

   581

   582 lemma add_right_mono:

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

   584 by (simp add: add.commute [of _ c] add_left_mono)

   585

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

   587 lemma add_mono:

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

   589   apply (erule add_right_mono [THEN order_trans])

   590   apply (simp add: add.commute add_left_mono)

   591   done

   592

   593 end

   594

   595 class ordered_cancel_ab_semigroup_add =

   596   ordered_ab_semigroup_add + cancel_ab_semigroup_add

   597 begin

   598

   599 lemma add_strict_left_mono:

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

   601 by (auto simp add: less_le add_left_mono)

   602

   603 lemma add_strict_right_mono:

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

   605 by (simp add: add.commute [of _ c] add_strict_left_mono)

   606

   607 text{*Strict monotonicity in both arguments*}

   608 lemma add_strict_mono:

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

   610 apply (erule add_strict_right_mono [THEN less_trans])

   611 apply (erule add_strict_left_mono)

   612 done

   613

   614 lemma add_less_le_mono:

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

   616 apply (erule add_strict_right_mono [THEN less_le_trans])

   617 apply (erule add_left_mono)

   618 done

   619

   620 lemma add_le_less_mono:

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

   622 apply (erule add_right_mono [THEN le_less_trans])

   623 apply (erule add_strict_left_mono)

   624 done

   625

   626 end

   627

   628 class ordered_ab_semigroup_add_imp_le =

   629   ordered_cancel_ab_semigroup_add +

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

   631 begin

   632

   633 lemma add_less_imp_less_left:

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

   635 proof -

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

   637   have "a <= b"

   638     apply (insert le)

   639     apply (drule add_le_imp_le_left)

   640     by (insert le, drule add_le_imp_le_left, assumption)

   641   moreover have "a \<noteq> b"

   642   proof (rule ccontr)

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

   644     then have "a = b" by simp

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

   646     with less show "False"by simp

   647   qed

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

   649 qed

   650

   651 lemma add_less_imp_less_right:

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

   653 apply (rule add_less_imp_less_left [of c])

   654 apply (simp add: add.commute)

   655 done

   656

   657 lemma add_less_cancel_left [simp]:

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

   659   by (blast intro: add_less_imp_less_left add_strict_left_mono)

   660

   661 lemma add_less_cancel_right [simp]:

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

   663   by (blast intro: add_less_imp_less_right add_strict_right_mono)

   664

   665 lemma add_le_cancel_left [simp]:

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

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

   668

   669 lemma add_le_cancel_right [simp]:

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

   671   by (simp add: add.commute [of a c] add.commute [of b c])

   672

   673 lemma add_le_imp_le_right:

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

   675 by simp

   676

   677 lemma max_add_distrib_left:

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

   679   unfolding max_def by auto

   680

   681 lemma min_add_distrib_left:

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

   683   unfolding min_def by auto

   684

   685 lemma max_add_distrib_right:

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

   687   unfolding max_def by auto

   688

   689 lemma min_add_distrib_right:

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

   691   unfolding min_def by auto

   692

   693 end

   694

   695 class ordered_cancel_comm_monoid_diff = comm_monoid_diff + ordered_ab_semigroup_add_imp_le +

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

   697 begin

   698

   699 context

   700   fixes a b

   701   assumes "a \<le> b"

   702 begin

   703

   704 lemma add_diff_inverse:

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

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

   707

   708 lemma add_diff_assoc:

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

   710   using a \<le> b by (auto simp add: le_iff_add add.left_commute [of c])

   711

   712 lemma add_diff_assoc2:

   713   "b - a + c = b + c - a"

   714   using a \<le> b by (auto simp add: le_iff_add add.assoc)

   715

   716 lemma diff_add_assoc:

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

   718   using a \<le> b by (simp add: add.commute add_diff_assoc)

   719

   720 lemma diff_add_assoc2:

   721   "b + c - a = b - a + c"

   722   using a \<le> bby (simp add: add.commute add_diff_assoc)

   723

   724 lemma diff_diff_right:

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

   726   by (simp add: add_diff_inverse add_diff_cancel_left [of a c "b - a", symmetric] add.commute)

   727

   728 lemma diff_add:

   729   "b - a + a = b"

   730   by (simp add: add.commute add_diff_inverse)

   731

   732 lemma le_add_diff:

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

   734   by (auto simp add: add.commute diff_add_assoc2 le_iff_add)

   735

   736 lemma le_imp_diff_is_add:

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

   738   by (auto simp add: add.commute add_diff_inverse)

   739

   740 lemma le_diff_conv2:

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

   742 proof

   743   assume ?P

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

   745   then show ?Q by (simp add: add_diff_inverse add.commute)

   746 next

   747   assume ?Q

   748   then have "a + c \<le> a + (b - a)" by (simp add: add_diff_inverse add.commute)

   749   then show ?P by simp

   750 qed

   751

   752 end

   753

   754 end

   755

   756

   757 subsection {* Support for reasoning about signs *}

   758

   759 class ordered_comm_monoid_add =

   760   ordered_cancel_ab_semigroup_add + comm_monoid_add

   761 begin

   762

   763 lemma add_pos_nonneg:

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

   765 proof -

   766   have "0 + 0 < a + b"

   767     using assms by (rule add_less_le_mono)

   768   then show ?thesis by simp

   769 qed

   770

   771 lemma add_pos_pos:

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

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

   774

   775 lemma add_nonneg_pos:

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

   777 proof -

   778   have "0 + 0 < a + b"

   779     using assms by (rule add_le_less_mono)

   780   then show ?thesis by simp

   781 qed

   782

   783 lemma add_nonneg_nonneg [simp]:

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

   785 proof -

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

   787     using assms by (rule add_mono)

   788   then show ?thesis by simp

   789 qed

   790

   791 lemma add_neg_nonpos:

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

   793 proof -

   794   have "a + b < 0 + 0"

   795     using assms by (rule add_less_le_mono)

   796   then show ?thesis by simp

   797 qed

   798

   799 lemma add_neg_neg:

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

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

   802

   803 lemma add_nonpos_neg:

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

   805 proof -

   806   have "a + b < 0 + 0"

   807     using assms by (rule add_le_less_mono)

   808   then show ?thesis by simp

   809 qed

   810

   811 lemma add_nonpos_nonpos:

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

   813 proof -

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

   815     using assms by (rule add_mono)

   816   then show ?thesis by simp

   817 qed

   818

   819 lemmas add_sign_intros =

   820   add_pos_nonneg add_pos_pos add_nonneg_pos add_nonneg_nonneg

   821   add_neg_nonpos add_neg_neg add_nonpos_neg add_nonpos_nonpos

   822

   823 lemma add_nonneg_eq_0_iff:

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

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

   826 proof (intro iffI conjI)

   827   have "x = x + 0" by simp

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

   829   also assume "x + y = 0"

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

   831   finally show "x = 0" .

   832 next

   833   have "y = 0 + y" by simp

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

   835   also assume "x + y = 0"

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

   837   finally show "y = 0" .

   838 next

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

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

   841 qed

   842

   843 lemma add_increasing:

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

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

   846

   847 lemma add_increasing2:

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

   849   by (simp add: add_increasing add.commute [of a])

   850

   851 lemma add_strict_increasing:

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

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

   854

   855 lemma add_strict_increasing2:

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

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

   858

   859 end

   860

   861 class ordered_ab_group_add =

   862   ab_group_add + ordered_ab_semigroup_add

   863 begin

   864

   865 subclass ordered_cancel_ab_semigroup_add ..

   866

   867 subclass ordered_ab_semigroup_add_imp_le

   868 proof

   869   fix a b c :: 'a

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

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

   872   hence "((-c) + c) + a \<le> ((-c) + c) + b" by (simp only: add.assoc)

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

   874 qed

   875

   876 subclass ordered_comm_monoid_add ..

   877

   878 lemma add_less_same_cancel1 [simp]:

   879   "b + a < b \<longleftrightarrow> a < 0"

   880   using add_less_cancel_left [of _ _ 0] by simp

   881

   882 lemma add_less_same_cancel2 [simp]:

   883   "a + b < b \<longleftrightarrow> a < 0"

   884   using add_less_cancel_right [of _ _ 0] by simp

   885

   886 lemma less_add_same_cancel1 [simp]:

   887   "a < a + b \<longleftrightarrow> 0 < b"

   888   using add_less_cancel_left [of _ 0] by simp

   889

   890 lemma less_add_same_cancel2 [simp]:

   891   "a < b + a \<longleftrightarrow> 0 < b"

   892   using add_less_cancel_right [of 0] by simp

   893

   894 lemma add_le_same_cancel1 [simp]:

   895   "b + a \<le> b \<longleftrightarrow> a \<le> 0"

   896   using add_le_cancel_left [of _ _ 0] by simp

   897

   898 lemma add_le_same_cancel2 [simp]:

   899   "a + b \<le> b \<longleftrightarrow> a \<le> 0"

   900   using add_le_cancel_right [of _ _ 0] by simp

   901

   902 lemma le_add_same_cancel1 [simp]:

   903   "a \<le> a + b \<longleftrightarrow> 0 \<le> b"

   904   using add_le_cancel_left [of _ 0] by simp

   905

   906 lemma le_add_same_cancel2 [simp]:

   907   "a \<le> b + a \<longleftrightarrow> 0 \<le> b"

   908   using add_le_cancel_right [of 0] by simp

   909

   910 lemma max_diff_distrib_left:

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

   912   using max_add_distrib_left [of x y "- z"] by simp

   913

   914 lemma min_diff_distrib_left:

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

   916   using min_add_distrib_left [of x y "- z"] by simp

   917

   918 lemma le_imp_neg_le:

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

   920 proof -

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

   922   then have "0 \<le> -a+b" by simp

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

   924   then show ?thesis by (simp add: algebra_simps)

   925 qed

   926

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

   928 proof

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

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

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

   932 next

   933   assume "a\<le>b"

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

   935 qed

   936

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

   938 by (subst neg_le_iff_le [symmetric], simp)

   939

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

   941 by (subst neg_le_iff_le [symmetric], simp)

   942

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

   944 by (force simp add: less_le)

   945

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

   947 by (subst neg_less_iff_less [symmetric], simp)

   948

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

   950 by (subst neg_less_iff_less [symmetric], simp)

   951

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

   953

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

   955 proof -

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

   957   thus ?thesis by simp

   958 qed

   959

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

   961 proof -

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

   963   thus ?thesis by simp

   964 qed

   965

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

   967 proof -

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

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

   970     apply (auto simp only: le_less)

   971     apply (drule mm)

   972     apply (simp_all)

   973     apply (drule mm[simplified], assumption)

   974     done

   975   then show ?thesis by simp

   976 qed

   977

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

   979 by (auto simp add: le_less minus_less_iff)

   980

   981 lemma diff_less_0_iff_less [simp]:

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

   983 proof -

   984   have "a - b < 0 \<longleftrightarrow> a + (- b) < b + (- b)" by simp

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

   986   finally show ?thesis .

   987 qed

   988

   989 lemmas less_iff_diff_less_0 = diff_less_0_iff_less [symmetric]

   990

   991 lemma diff_less_eq [algebra_simps, field_simps]:

   992   "a - b < c \<longleftrightarrow> a < c + b"

   993 apply (subst less_iff_diff_less_0 [of a])

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

   995 apply (simp add: algebra_simps)

   996 done

   997

   998 lemma less_diff_eq[algebra_simps, field_simps]:

   999   "a < c - b \<longleftrightarrow> a + b < c"

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

  1001 apply (subst less_iff_diff_less_0 [of a])

  1002 apply (simp add: algebra_simps)

  1003 done

  1004

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

  1006 by (auto simp add: le_less diff_less_eq )

  1007

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

  1009 by (auto simp add: le_less less_diff_eq)

  1010

  1011 lemma diff_le_0_iff_le [simp]:

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

  1013   by (simp add: algebra_simps)

  1014

  1015 lemmas le_iff_diff_le_0 = diff_le_0_iff_le [symmetric]

  1016

  1017 lemma diff_eq_diff_less:

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

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

  1020

  1021 lemma diff_eq_diff_less_eq:

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

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

  1024

  1025 lemma diff_mono: "a \<le> b \<Longrightarrow> d \<le> c \<Longrightarrow> a - c \<le> b - d"

  1026   by (simp add: field_simps add_mono)

  1027

  1028 lemma diff_left_mono: "b \<le> a \<Longrightarrow> c - a \<le> c - b"

  1029   by (simp add: field_simps)

  1030

  1031 lemma diff_right_mono: "a \<le> b \<Longrightarrow> a - c \<le> b - c"

  1032   by (simp add: field_simps)

  1033

  1034 lemma diff_strict_mono: "a < b \<Longrightarrow> d < c \<Longrightarrow> a - c < b - d"

  1035   by (simp add: field_simps add_strict_mono)

  1036

  1037 lemma diff_strict_left_mono: "b < a \<Longrightarrow> c - a < c - b"

  1038   by (simp add: field_simps)

  1039

  1040 lemma diff_strict_right_mono: "a < b \<Longrightarrow> a - c < b - c"

  1041   by (simp add: field_simps)

  1042

  1043 end

  1044

  1045 ML_file "Tools/group_cancel.ML"

  1046

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

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

  1049

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

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

  1052

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

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

  1055

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

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

  1058

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

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

  1061

  1062 class linordered_ab_semigroup_add =

  1063   linorder + ordered_ab_semigroup_add

  1064

  1065 class linordered_cancel_ab_semigroup_add =

  1066   linorder + ordered_cancel_ab_semigroup_add

  1067 begin

  1068

  1069 subclass linordered_ab_semigroup_add ..

  1070

  1071 subclass ordered_ab_semigroup_add_imp_le

  1072 proof

  1073   fix a b c :: 'a

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

  1075   show "a <= b"

  1076   proof (rule ccontr)

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

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

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

  1080     have "a = b"

  1081       apply (insert le)

  1082       apply (insert le2)

  1083       apply (drule antisym, simp_all)

  1084       done

  1085     with w show False

  1086       by (simp add: linorder_not_le [symmetric])

  1087   qed

  1088 qed

  1089

  1090 end

  1091

  1092 class linordered_ab_group_add = linorder + ordered_ab_group_add

  1093 begin

  1094

  1095 subclass linordered_cancel_ab_semigroup_add ..

  1096

  1097 lemma equal_neg_zero [simp]:

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

  1099 proof

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

  1101 next

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

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

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

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

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

  1107   next

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

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

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

  1111   qed

  1112 qed

  1113

  1114 lemma neg_equal_zero [simp]:

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

  1116   by (auto dest: sym)

  1117

  1118 lemma neg_less_eq_nonneg [simp]:

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

  1120 proof

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

  1122   proof (rule classical)

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

  1124     then have "a < 0" by auto

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

  1126     then show ?thesis by auto

  1127   qed

  1128 next

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

  1130   proof (rule order_trans)

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

  1132   next

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

  1134   qed

  1135 qed

  1136

  1137 lemma neg_less_pos [simp]:

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

  1139   by (auto simp add: less_le)

  1140

  1141 lemma less_eq_neg_nonpos [simp]:

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

  1143   using neg_less_eq_nonneg [of "- a"] by simp

  1144

  1145 lemma less_neg_neg [simp]:

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

  1147   using neg_less_pos [of "- a"] by simp

  1148

  1149 lemma double_zero [simp]:

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

  1151 proof

  1152   assume assm: "a + a = 0"

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

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

  1155 qed simp

  1156

  1157 lemma double_zero_sym [simp]:

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

  1159   by (rule, drule sym) simp_all

  1160

  1161 lemma zero_less_double_add_iff_zero_less_single_add [simp]:

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

  1163 proof

  1164   assume "0 < a + a"

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

  1166   then have "- a < a" by simp

  1167   then show "0 < a" by simp

  1168 next

  1169   assume "0 < a"

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

  1171     by (rule add_strict_mono)

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

  1173 qed

  1174

  1175 lemma zero_le_double_add_iff_zero_le_single_add [simp]:

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

  1177   by (auto simp add: le_less)

  1178

  1179 lemma double_add_less_zero_iff_single_add_less_zero [simp]:

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

  1181 proof -

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

  1183     by (simp add: not_less)

  1184   then show ?thesis by simp

  1185 qed

  1186

  1187 lemma double_add_le_zero_iff_single_add_le_zero [simp]:

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

  1189 proof -

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

  1191     by (simp add: not_le)

  1192   then show ?thesis by simp

  1193 qed

  1194

  1195 lemma minus_max_eq_min:

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

  1197   by (auto simp add: max_def min_def)

  1198

  1199 lemma minus_min_eq_max:

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

  1201   by (auto simp add: max_def min_def)

  1202

  1203 end

  1204

  1205 class abs =

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

  1207 begin

  1208

  1209 notation (xsymbols)

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

  1211

  1212 notation (HTML output)

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

  1214

  1215 end

  1216

  1217 class sgn =

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

  1219

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

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

  1222

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

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

  1225 begin

  1226

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

  1228   by (simp add:sgn_if)

  1229

  1230 end

  1231

  1232 class ordered_ab_group_add_abs = ordered_ab_group_add + abs +

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

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

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

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

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

  1238 begin

  1239

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

  1241   unfolding neg_le_0_iff_le by simp

  1242

  1243 lemma abs_of_nonneg [simp]:

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

  1245 proof (rule antisym)

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

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

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

  1249 qed (rule abs_ge_self)

  1250

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

  1252 by (rule antisym)

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

  1254

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

  1256 proof -

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

  1258   proof (rule antisym)

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

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

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

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

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

  1264   qed

  1265   then show ?thesis by auto

  1266 qed

  1267

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

  1269 by simp

  1270

  1271 lemma abs_0_eq [simp]: "0 = \<bar>a\<bar> \<longleftrightarrow> a = 0"

  1272 proof -

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

  1274   thus ?thesis by simp

  1275 qed

  1276

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

  1278 proof

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

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

  1281   thus "a = 0" by simp

  1282 next

  1283   assume "a = 0"

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

  1285 qed

  1286

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

  1288 by (simp add: less_le)

  1289

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

  1291 proof -

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

  1293   show ?thesis by (simp add: a)

  1294 qed

  1295

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

  1297 proof -

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

  1299   then show ?thesis by simp

  1300 qed

  1301

  1302 lemma abs_minus_commute:

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

  1304 proof -

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

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

  1307   finally show ?thesis .

  1308 qed

  1309

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

  1311 by (rule abs_of_nonneg, rule less_imp_le)

  1312

  1313 lemma abs_of_nonpos [simp]:

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

  1315 proof -

  1316   let ?b = "- a"

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

  1318   unfolding abs_minus_cancel [of "?b"]

  1319   unfolding neg_le_0_iff_le [of "?b"]

  1320   unfolding minus_minus by (erule abs_of_nonneg)

  1321   then show ?thesis using assms by auto

  1322 qed

  1323

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

  1325 by (rule abs_of_nonpos, rule less_imp_le)

  1326

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

  1328 by (insert abs_ge_self, blast intro: order_trans)

  1329

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

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

  1332

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

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

  1335

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

  1337 proof -

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

  1339     by (simp add: algebra_simps)

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

  1341     by (simp add: abs_triangle_ineq)

  1342   then show ?thesis

  1343     by (simp add: algebra_simps)

  1344 qed

  1345

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

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

  1348

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

  1350   by (simp add: abs_le_iff abs_triangle_ineq2 abs_triangle_ineq2_sym)

  1351

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

  1353 proof -

  1354   have "\<bar>a - b\<bar> = \<bar>a + - b\<bar>" by (simp add: algebra_simps)

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

  1356   finally show ?thesis by simp

  1357 qed

  1358

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

  1360 proof -

  1361   have "\<bar>a + b - (c+d)\<bar> = \<bar>(a-c) + (b-d)\<bar>" by (simp add: algebra_simps)

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

  1363   finally show ?thesis .

  1364 qed

  1365

  1366 lemma abs_add_abs [simp]:

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

  1368 proof (rule antisym)

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

  1370 next

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

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

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

  1374 qed

  1375

  1376 end

  1377

  1378

  1379 subsection {* Tools setup *}

  1380

  1381 lemma add_mono_thms_linordered_semiring:

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

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

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

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

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

  1387 by (rule add_mono, clarify+)+

  1388

  1389 lemma add_mono_thms_linordered_field:

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

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

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

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

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

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

  1396 by (auto intro: add_strict_right_mono add_strict_left_mono

  1397   add_less_le_mono add_le_less_mono add_strict_mono)

  1398

  1399 code_identifier

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

  1401

  1402 end

  1403