src/HOL/Groups.thy
 author hoelzl Fri Feb 12 16:09:07 2016 +0100 (2016-02-12) changeset 62377 ace69956d018 parent 62376 85f38d5f8807 child 62378 85ed00c1fe7c permissions -rw-r--r--
     1 (*  Title:   HOL/Groups.thy

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

     3 *)

     4

     5 section \<open>Groups, also combined with orderings\<close>

     6

     7 theory Groups

     8 imports Orderings

     9 begin

    10

    11 subsection \<open>Dynamic facts\<close>

    12

    13 named_theorems ac_simps "associativity and commutativity simplification rules"

    14

    15

    16 text\<open>The rewrites accumulated in \<open>algebra_simps\<close> 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 \<open>field_simps\<close>.\<close>

    24

    25 named_theorems algebra_simps "algebra simplification rules"

    26

    27

    28 text\<open>Lemmas \<open>field_simps\<close> 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 \<open>algebra_simps\<close>.\<close>

    32

    33 named_theorems field_simps "algebra simplification rules for fields"

    34

    35

    36 subsection \<open>Abstract structures\<close>

    37

    38 text \<open>

    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 \<close>

    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 standard (simp_all add: commute comm_neutral)

    75

    76 end

    77

    78

    79 subsection \<open>Generic operations\<close>

    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 \<open>

    96   Reorient_Proc.add

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

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

    99       | _ => false)

   100 \<close>

   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 \<open>

   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 \<close> \<comment> \<open>show types that are presumably too general\<close>

   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 \<open>Semigroups and Monoids\<close>

   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 standard (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 standard (fact add_commute)

   147

   148 declare add.left_commute [algebra_simps, field_simps]

   149

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

   151

   152 end

   153

   154 hide_fact add_commute

   155

   156 lemmas 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 standard (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 standard (fact mult_commute)

   175

   176 declare mult.left_commute [algebra_simps, field_simps]

   177

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

   179

   180 end

   181

   182 hide_fact mult_commute

   183

   184 lemmas 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 standard (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 subclass monoid_add

   204   by standard (simp_all add: add_0 add.commute [of _ 0])

   205

   206 sublocale add: comm_monoid plus 0

   207   by standard (simp add: ac_simps)

   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 standard (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 subclass monoid_mult

   229   by standard (simp_all add: mult_1 mult.commute [of _ 1])

   230

   231 sublocale mult: comm_monoid times 1

   232   by standard (simp add: ac_simps)

   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 + minus +

   252   assumes add_diff_cancel_left' [simp]: "(a + b) - a = b"

   253   assumes diff_diff_add [algebra_simps, field_simps]: "a - b - c = a - (b + c)"

   254 begin

   255

   256 lemma add_diff_cancel_right' [simp]:

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

   258   using add_diff_cancel_left' [of b a] by (simp add: ac_simps)

   259

   260 subclass cancel_semigroup_add

   261 proof

   262   fix a b c :: 'a

   263   assume "a + b = a + c"

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

   265     by simp

   266   then show "b = c"

   267     by simp

   268 next

   269   fix a b c :: 'a

   270   assume "b + a = c + a"

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

   272     by simp

   273   then show "b = c"

   274     by simp

   275 qed

   276

   277 lemma add_diff_cancel_left [simp]:

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

   279   unfolding diff_diff_add [symmetric] by simp

   280

   281 lemma add_diff_cancel_right [simp]:

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

   283   using add_diff_cancel_left [symmetric] by (simp add: ac_simps)

   284

   285 lemma diff_right_commute:

   286   "a - c - b = a - b - c"

   287   by (simp add: diff_diff_add add.commute)

   288

   289 end

   290

   291 class cancel_comm_monoid_add = cancel_ab_semigroup_add + comm_monoid_add

   292 begin

   293

   294 lemma diff_zero [simp]:

   295   "a - 0 = a"

   296   using add_diff_cancel_right' [of a 0] by simp

   297

   298 lemma diff_cancel [simp]:

   299   "a - a = 0"

   300 proof -

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

   302   then show ?thesis by simp

   303 qed

   304

   305 lemma add_implies_diff:

   306   assumes "c + b = a"

   307   shows "c = a - b"

   308 proof -

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

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

   311 qed

   312

   313 end

   314

   315 class comm_monoid_diff = cancel_comm_monoid_add +

   316   assumes zero_diff [simp]: "0 - a = 0"

   317 begin

   318

   319 lemma diff_add_zero [simp]:

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

   321 proof -

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

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

   324   finally show ?thesis .

   325 qed

   326

   327 end

   328

   329

   330 subsection \<open>Groups\<close>

   331

   332 class group_add = minus + uminus + monoid_add +

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

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

   335 begin

   336

   337 lemma diff_conv_add_uminus:

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

   339   by simp

   340

   341 lemma minus_unique:

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

   343 proof -

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

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

   346   finally show ?thesis .

   347 qed

   348

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

   350 proof -

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

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

   353 qed

   354

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

   356 proof -

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

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

   359 qed

   360

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

   362 proof -

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

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

   365   finally show ?thesis .

   366 qed

   367

   368 lemma diff_self [simp]:

   369   "a - a = 0"

   370   using right_minus [of a] by simp

   371

   372 subclass cancel_semigroup_add

   373 proof

   374   fix a b c :: 'a

   375   assume "a + b = a + c"

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

   377     unfolding add.assoc by simp

   378   then show "b = c" by simp

   379 next

   380   fix a b c :: 'a

   381   assume "b + a = c + a"

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

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

   384 qed

   385

   386 lemma minus_add_cancel [simp]:

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

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

   389

   390 lemma add_minus_cancel [simp]:

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

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

   393

   394 lemma diff_add_cancel [simp]:

   395   "a - b + b = a"

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

   397

   398 lemma add_diff_cancel [simp]:

   399   "a + b - b = a"

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

   401

   402 lemma minus_add:

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

   404 proof -

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

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

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

   408     by (rule minus_unique)

   409 qed

   410

   411 lemma right_minus_eq [simp]:

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

   413 proof

   414   assume "a - b = 0"

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

   416   also have "\<dots> = b" using \<open>a - b = 0\<close> by simp

   417   finally show "a = b" .

   418 next

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

   420 qed

   421

   422 lemma eq_iff_diff_eq_0:

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

   424   by (fact right_minus_eq [symmetric])

   425

   426 lemma diff_0 [simp]:

   427   "0 - a = - a"

   428   by (simp only: diff_conv_add_uminus add_0_left)

   429

   430 lemma diff_0_right [simp]:

   431   "a - 0 = a"

   432   by (simp only: diff_conv_add_uminus minus_zero add_0_right)

   433

   434 lemma diff_minus_eq_add [simp]:

   435   "a - - b = a + b"

   436   by (simp only: diff_conv_add_uminus minus_minus)

   437

   438 lemma neg_equal_iff_equal [simp]:

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

   440 proof

   441   assume "- a = - b"

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

   443   thus "a = b" by simp

   444 next

   445   assume "a = b"

   446   thus "- a = - b" by simp

   447 qed

   448

   449 lemma neg_equal_0_iff_equal [simp]:

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

   451   by (subst neg_equal_iff_equal [symmetric]) simp

   452

   453 lemma neg_0_equal_iff_equal [simp]:

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

   455   by (subst neg_equal_iff_equal [symmetric]) simp

   456

   457 text\<open>The next two equations can make the simplifier loop!\<close>

   458

   459 lemma equation_minus_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 minus_equation_iff:

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

   468 proof -

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

   470   thus ?thesis by (simp add: eq_commute)

   471 qed

   472

   473 lemma eq_neg_iff_add_eq_0:

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

   475 proof

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

   477 next

   478   assume "a + b = 0"

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

   480     by (simp only: add.assoc)

   481   ultimately show "a = - b" by simp

   482 qed

   483

   484 lemma add_eq_0_iff2:

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

   486   by (fact eq_neg_iff_add_eq_0 [symmetric])

   487

   488 lemma neg_eq_iff_add_eq_0:

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

   490   by (auto simp add: add_eq_0_iff2)

   491

   492 lemma add_eq_0_iff:

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

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

   495

   496 lemma minus_diff_eq [simp]:

   497   "- (a - b) = b - a"

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

   499

   500 lemma add_diff_eq [algebra_simps, field_simps]:

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

   502   by (simp only: diff_conv_add_uminus add.assoc)

   503

   504 lemma diff_add_eq_diff_diff_swap:

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

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

   507

   508 lemma diff_eq_eq [algebra_simps, field_simps]:

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

   510   by auto

   511

   512 lemma eq_diff_eq [algebra_simps, field_simps]:

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

   514   by auto

   515

   516 lemma diff_diff_eq2 [algebra_simps, field_simps]:

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

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

   519

   520 lemma diff_eq_diff_eq:

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

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

   523

   524 end

   525

   526 class ab_group_add = minus + uminus + comm_monoid_add +

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

   528   assumes ab_diff_conv_add_uminus: "a - b = a + (- b)"

   529 begin

   530

   531 subclass group_add

   532   proof qed (simp_all add: ab_left_minus ab_diff_conv_add_uminus)

   533

   534 subclass cancel_comm_monoid_add

   535 proof

   536   fix a b c :: 'a

   537   have "b + a - a = b"

   538     by simp

   539   then show "a + b - a = b"

   540     by (simp add: ac_simps)

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

   542     by (simp add: algebra_simps)

   543 qed

   544

   545 lemma uminus_add_conv_diff [simp]:

   546   "- a + b = b - a"

   547   by (simp add: add.commute)

   548

   549 lemma minus_add_distrib [simp]:

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

   551   by (simp add: algebra_simps)

   552

   553 lemma diff_add_eq [algebra_simps, field_simps]:

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

   555   by (simp add: algebra_simps)

   556

   557 end

   558

   559

   560 subsection \<open>(Partially) Ordered Groups\<close>

   561

   562 text \<open>

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

   564   \begin{itemize}

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

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

   567   \end{itemize}

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

   569   \begin{itemize}

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

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

   572   \end{itemize}

   573 \<close>

   574

   575 class ordered_ab_semigroup_add = order + ab_semigroup_add +

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

   577 begin

   578

   579 lemma add_right_mono:

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

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

   582

   583 text \<open>non-strict, in both arguments\<close>

   584 lemma add_mono:

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

   586   apply (erule add_right_mono [THEN order_trans])

   587   apply (simp add: add.commute add_left_mono)

   588   done

   589

   590 end

   591

   592 text\<open>Strict monotonicity in both arguments\<close>

   593 class strict_ordered_ab_semigroup_add = ordered_ab_semigroup_add +

   594   assumes add_strict_mono: "a < b \<Longrightarrow> c < d \<Longrightarrow> a + c < b + d"

   595

   596 class ordered_cancel_ab_semigroup_add =

   597   ordered_ab_semigroup_add + cancel_ab_semigroup_add

   598 begin

   599

   600 lemma add_strict_left_mono:

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

   602 by (auto simp add: less_le add_left_mono)

   603

   604 lemma add_strict_right_mono:

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

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

   607

   608 subclass strict_ordered_ab_semigroup_add

   609   apply standard

   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 = ordered_cancel_ab_semigroup_add +

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

   630 begin

   631

   632 lemma add_less_imp_less_left:

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

   634 proof -

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

   636   have "a <= b"

   637     apply (insert le)

   638     apply (drule add_le_imp_le_left)

   639     by (insert le, drule add_le_imp_le_left, assumption)

   640   moreover have "a \<noteq> b"

   641   proof (rule ccontr)

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

   643     then have "a = b" by simp

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

   645     with less show "False"by simp

   646   qed

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

   648 qed

   649

   650 lemma add_less_imp_less_right:

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

   652 apply (rule add_less_imp_less_left [of c])

   653 apply (simp add: add.commute)

   654 done

   655

   656 lemma add_less_cancel_left [simp]:

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

   658   by (blast intro: add_less_imp_less_left add_strict_left_mono)

   659

   660 lemma add_less_cancel_right [simp]:

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

   662   by (blast intro: add_less_imp_less_right add_strict_right_mono)

   663

   664 lemma add_le_cancel_left [simp]:

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

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

   667

   668 lemma add_le_cancel_right [simp]:

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

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

   671

   672 lemma add_le_imp_le_right:

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

   674 by simp

   675

   676 lemma max_add_distrib_left:

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

   678   unfolding max_def by auto

   679

   680 lemma min_add_distrib_left:

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

   682   unfolding min_def by auto

   683

   684 lemma max_add_distrib_right:

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

   686   unfolding max_def by auto

   687

   688 lemma min_add_distrib_right:

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

   690   unfolding min_def by auto

   691

   692 end

   693

   694 subsection \<open>Support for reasoning about signs\<close>

   695

   696 class ordered_comm_monoid_add = comm_monoid_add + ordered_ab_semigroup_add

   697 begin

   698

   699 lemma add_nonneg_nonneg [simp]:

   700   "0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 \<le> a + b"

   701   using add_mono[of 0 a 0 b] by simp

   702

   703 lemma add_nonpos_nonpos:

   704   "a \<le> 0 \<Longrightarrow> b \<le> 0 \<Longrightarrow> a + b \<le> 0"

   705   using add_mono[of a 0 b 0] by simp

   706

   707 lemma add_nonneg_eq_0_iff:

   708   "0 \<le> x \<Longrightarrow> 0 \<le> y \<Longrightarrow> x + y = 0 \<longleftrightarrow> x = 0 \<and> y = 0"

   709   using add_left_mono[of 0 y x] add_right_mono[of 0 x y] by auto

   710

   711 lemma add_nonpos_eq_0_iff:

   712   "x \<le> 0 \<Longrightarrow> y \<le> 0 \<Longrightarrow> x + y = 0 \<longleftrightarrow> x = 0 \<and> y = 0"

   713   using add_left_mono[of y 0 x] add_right_mono[of x 0 y] by auto

   714

   715 lemma add_increasing:

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

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

   718

   719 lemma add_increasing2:

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

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

   722

   723 lemma add_decreasing:

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

   725   using add_mono[of a 0 c b] by simp

   726

   727 lemma add_decreasing2:

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

   729   using add_mono[of a b c 0] by simp

   730

   731 lemma add_pos_nonneg: "0 < a \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 < a + b"

   732   using less_le_trans[of 0 a "a + b"] by (simp add: add_increasing2)

   733

   734 lemma add_pos_pos: "0 < a \<Longrightarrow> 0 < b \<Longrightarrow> 0 < a + b"

   735   by (intro add_pos_nonneg less_imp_le)

   736

   737 lemma add_nonneg_pos: "0 \<le> a \<Longrightarrow> 0 < b \<Longrightarrow> 0 < a + b"

   738   using add_pos_nonneg[of b a] by (simp add: add_commute)

   739

   740 lemma add_neg_nonpos: "a < 0 \<Longrightarrow> b \<le> 0 \<Longrightarrow> a + b < 0"

   741   using le_less_trans[of "a + b" a 0] by (simp add: add_decreasing2)

   742

   743 lemma add_neg_neg: "a < 0 \<Longrightarrow> b < 0 \<Longrightarrow> a + b < 0"

   744   by (intro add_neg_nonpos less_imp_le)

   745

   746 lemma add_nonpos_neg: "a \<le> 0 \<Longrightarrow> b < 0 \<Longrightarrow> a + b < 0"

   747   using add_neg_nonpos[of b a] by (simp add: add_commute)

   748

   749 lemmas add_sign_intros =

   750   add_pos_nonneg add_pos_pos add_nonneg_pos add_nonneg_nonneg

   751   add_neg_nonpos add_neg_neg add_nonpos_neg add_nonpos_nonpos

   752

   753 end

   754

   755 class strict_ordered_comm_monoid_add = comm_monoid_add + strict_ordered_ab_semigroup_add

   756

   757 class ordered_cancel_comm_monoid_add = ordered_comm_monoid_add + cancel_ab_semigroup_add

   758 begin

   759

   760 subclass ordered_cancel_ab_semigroup_add ..

   761 subclass strict_ordered_comm_monoid_add ..

   762

   763 lemma add_strict_increasing:

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

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

   766

   767 lemma add_strict_increasing2:

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

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

   770

   771 end

   772

   773 class ordered_ab_group_add = ab_group_add + ordered_ab_semigroup_add

   774 begin

   775

   776 subclass ordered_cancel_ab_semigroup_add ..

   777

   778 subclass ordered_ab_semigroup_add_imp_le

   779 proof

   780   fix a b c :: 'a

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

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

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

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

   785 qed

   786

   787 subclass ordered_cancel_comm_monoid_add ..

   788

   789 lemma add_less_same_cancel1 [simp]:

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

   791   using add_less_cancel_left [of _ _ 0] by simp

   792

   793 lemma add_less_same_cancel2 [simp]:

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

   795   using add_less_cancel_right [of _ _ 0] by simp

   796

   797 lemma less_add_same_cancel1 [simp]:

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

   799   using add_less_cancel_left [of _ 0] by simp

   800

   801 lemma less_add_same_cancel2 [simp]:

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

   803   using add_less_cancel_right [of 0] by simp

   804

   805 lemma add_le_same_cancel1 [simp]:

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

   807   using add_le_cancel_left [of _ _ 0] by simp

   808

   809 lemma add_le_same_cancel2 [simp]:

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

   811   using add_le_cancel_right [of _ _ 0] by simp

   812

   813 lemma le_add_same_cancel1 [simp]:

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

   815   using add_le_cancel_left [of _ 0] by simp

   816

   817 lemma le_add_same_cancel2 [simp]:

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

   819   using add_le_cancel_right [of 0] by simp

   820

   821 lemma max_diff_distrib_left:

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

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

   824

   825 lemma min_diff_distrib_left:

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

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

   828

   829 lemma le_imp_neg_le:

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

   831 proof -

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

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

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

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

   836 qed

   837

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

   839 proof

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

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

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

   843 next

   844   assume "a\<le>b"

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

   846 qed

   847

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

   849 by (subst neg_le_iff_le [symmetric], simp)

   850

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

   852 by (subst neg_le_iff_le [symmetric], simp)

   853

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

   855 by (force simp add: less_le)

   856

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

   858 by (subst neg_less_iff_less [symmetric], simp)

   859

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

   861 by (subst neg_less_iff_less [symmetric], simp)

   862

   863 text\<open>The next several equations can make the simplifier loop!\<close>

   864

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

   866 proof -

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

   868   thus ?thesis by simp

   869 qed

   870

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

   872 proof -

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

   874   thus ?thesis by simp

   875 qed

   876

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

   878 proof -

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

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

   881     apply (auto simp only: le_less)

   882     apply (drule mm)

   883     apply (simp_all)

   884     apply (drule mm[simplified], assumption)

   885     done

   886   then show ?thesis by simp

   887 qed

   888

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

   890 by (auto simp add: le_less minus_less_iff)

   891

   892 lemma diff_less_0_iff_less [simp]:

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

   894 proof -

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

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

   897   finally show ?thesis .

   898 qed

   899

   900 lemmas less_iff_diff_less_0 = diff_less_0_iff_less [symmetric]

   901

   902 lemma diff_less_eq [algebra_simps, field_simps]:

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

   904 apply (subst less_iff_diff_less_0 [of a])

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

   906 apply (simp add: algebra_simps)

   907 done

   908

   909 lemma less_diff_eq[algebra_simps, field_simps]:

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

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

   912 apply (subst less_iff_diff_less_0 [of a])

   913 apply (simp add: algebra_simps)

   914 done

   915

   916 lemma diff_gt_0_iff_gt [simp]:

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

   918   by (simp add: less_diff_eq)

   919

   920 lemma diff_le_eq [algebra_simps, field_simps]:

   921   "a - b \<le> c \<longleftrightarrow> a \<le> c + b"

   922   by (auto simp add: le_less diff_less_eq )

   923

   924 lemma le_diff_eq [algebra_simps, field_simps]:

   925   "a \<le> c - b \<longleftrightarrow> a + b \<le> c"

   926   by (auto simp add: le_less less_diff_eq)

   927

   928 lemma diff_le_0_iff_le [simp]:

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

   930   by (simp add: algebra_simps)

   931

   932 lemmas le_iff_diff_le_0 = diff_le_0_iff_le [symmetric]

   933

   934 lemma diff_ge_0_iff_ge [simp]:

   935   "a - b \<ge> 0 \<longleftrightarrow> a \<ge> b"

   936   by (simp add: le_diff_eq)

   937

   938 lemma diff_eq_diff_less:

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

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

   941

   942 lemma diff_eq_diff_less_eq:

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

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

   945

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

   947   by (simp add: field_simps add_mono)

   948

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

   950   by (simp add: field_simps)

   951

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

   953   by (simp add: field_simps)

   954

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

   956   by (simp add: field_simps add_strict_mono)

   957

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

   959   by (simp add: field_simps)

   960

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

   962   by (simp add: field_simps)

   963

   964 end

   965

   966 ML_file "Tools/group_cancel.ML"

   967

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

   969   \<open>fn phi => fn ss => try Group_Cancel.cancel_add_conv\<close>

   970

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

   972   \<open>fn phi => fn ss => try Group_Cancel.cancel_diff_conv\<close>

   973

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

   975   \<open>fn phi => fn ss => try Group_Cancel.cancel_eq_conv\<close>

   976

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

   978   \<open>fn phi => fn ss => try Group_Cancel.cancel_le_conv\<close>

   979

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

   981   \<open>fn phi => fn ss => try Group_Cancel.cancel_less_conv\<close>

   982

   983 class linordered_ab_semigroup_add =

   984   linorder + ordered_ab_semigroup_add

   985

   986 class linordered_cancel_ab_semigroup_add =

   987   linorder + ordered_cancel_ab_semigroup_add

   988 begin

   989

   990 subclass linordered_ab_semigroup_add ..

   991

   992 subclass ordered_ab_semigroup_add_imp_le

   993 proof

   994   fix a b c :: 'a

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

   996   show "a <= b"

   997   proof (rule ccontr)

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

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

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

  1001     have "a = b"

  1002       apply (insert le)

  1003       apply (insert le2)

  1004       apply (drule antisym, simp_all)

  1005       done

  1006     with w show False

  1007       by (simp add: linorder_not_le [symmetric])

  1008   qed

  1009 qed

  1010

  1011 end

  1012

  1013 class linordered_ab_group_add = linorder + ordered_ab_group_add

  1014 begin

  1015

  1016 subclass linordered_cancel_ab_semigroup_add ..

  1017

  1018 lemma equal_neg_zero [simp]:

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

  1020 proof

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

  1022 next

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

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

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

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

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

  1028   next

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

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

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

  1032   qed

  1033 qed

  1034

  1035 lemma neg_equal_zero [simp]:

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

  1037   by (auto dest: sym)

  1038

  1039 lemma neg_less_eq_nonneg [simp]:

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

  1041 proof

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

  1043   proof (rule classical)

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

  1045     then have "a < 0" by auto

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

  1047     then show ?thesis by auto

  1048   qed

  1049 next

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

  1051   proof (rule order_trans)

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

  1053   next

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

  1055   qed

  1056 qed

  1057

  1058 lemma neg_less_pos [simp]:

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

  1060   by (auto simp add: less_le)

  1061

  1062 lemma less_eq_neg_nonpos [simp]:

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

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

  1065

  1066 lemma less_neg_neg [simp]:

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

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

  1069

  1070 lemma double_zero [simp]:

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

  1072 proof

  1073   assume assm: "a + a = 0"

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

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

  1076 qed simp

  1077

  1078 lemma double_zero_sym [simp]:

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

  1080   by (rule, drule sym) simp_all

  1081

  1082 lemma zero_less_double_add_iff_zero_less_single_add [simp]:

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

  1084 proof

  1085   assume "0 < a + a"

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

  1087   then have "- a < a" by simp

  1088   then show "0 < a" by simp

  1089 next

  1090   assume "0 < a"

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

  1092     by (rule add_strict_mono)

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

  1094 qed

  1095

  1096 lemma zero_le_double_add_iff_zero_le_single_add [simp]:

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

  1098   by (auto simp add: le_less)

  1099

  1100 lemma double_add_less_zero_iff_single_add_less_zero [simp]:

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

  1102 proof -

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

  1104     by (simp add: not_less)

  1105   then show ?thesis by simp

  1106 qed

  1107

  1108 lemma double_add_le_zero_iff_single_add_le_zero [simp]:

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

  1110 proof -

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

  1112     by (simp add: not_le)

  1113   then show ?thesis by simp

  1114 qed

  1115

  1116 lemma minus_max_eq_min:

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

  1118   by (auto simp add: max_def min_def)

  1119

  1120 lemma minus_min_eq_max:

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

  1122   by (auto simp add: max_def min_def)

  1123

  1124 end

  1125

  1126 class abs =

  1127   fixes abs :: "'a \<Rightarrow> 'a"  ("\<bar>_\<bar>")

  1128

  1129 class sgn =

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

  1131

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

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

  1134

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

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

  1137 begin

  1138

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

  1140   by (simp add:sgn_if)

  1141

  1142 end

  1143

  1144 class ordered_ab_group_add_abs = ordered_ab_group_add + abs +

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

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

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

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

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

  1150 begin

  1151

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

  1153   unfolding neg_le_0_iff_le by simp

  1154

  1155 lemma abs_of_nonneg [simp]:

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

  1157 proof (rule antisym)

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

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

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

  1161 qed (rule abs_ge_self)

  1162

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

  1164 by (rule antisym)

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

  1166

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

  1168 proof -

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

  1170   proof (rule antisym)

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

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

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

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

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

  1176   qed

  1177   then show ?thesis by auto

  1178 qed

  1179

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

  1181 by simp

  1182

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

  1184 proof -

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

  1186   thus ?thesis by simp

  1187 qed

  1188

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

  1190 proof

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

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

  1193   thus "a = 0" by simp

  1194 next

  1195   assume "a = 0"

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

  1197 qed

  1198

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

  1200 by (simp add: less_le)

  1201

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

  1203 proof -

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

  1205   show ?thesis by (simp add: a)

  1206 qed

  1207

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

  1209 proof -

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

  1211   then show ?thesis by simp

  1212 qed

  1213

  1214 lemma abs_minus_commute:

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

  1216 proof -

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

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

  1219   finally show ?thesis .

  1220 qed

  1221

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

  1223 by (rule abs_of_nonneg, rule less_imp_le)

  1224

  1225 lemma abs_of_nonpos [simp]:

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

  1227 proof -

  1228   let ?b = "- a"

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

  1230   unfolding abs_minus_cancel [of "?b"]

  1231   unfolding neg_le_0_iff_le [of "?b"]

  1232   unfolding minus_minus by (erule abs_of_nonneg)

  1233   then show ?thesis using assms by auto

  1234 qed

  1235

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

  1237 by (rule abs_of_nonpos, rule less_imp_le)

  1238

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

  1240 by (insert abs_ge_self, blast intro: order_trans)

  1241

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

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

  1244

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

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

  1247

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

  1249 proof -

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

  1251     by (simp add: algebra_simps)

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

  1253     by (simp add: abs_triangle_ineq)

  1254   then show ?thesis

  1255     by (simp add: algebra_simps)

  1256 qed

  1257

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

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

  1260

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

  1262   by (simp add: abs_le_iff abs_triangle_ineq2 abs_triangle_ineq2_sym)

  1263

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

  1265 proof -

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

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

  1268   finally show ?thesis by simp

  1269 qed

  1270

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

  1272 proof -

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

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

  1275   finally show ?thesis .

  1276 qed

  1277

  1278 lemma abs_add_abs [simp]:

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

  1280 proof (rule antisym)

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

  1282 next

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

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

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

  1286 qed

  1287

  1288 end

  1289

  1290 lemma dense_eq0_I:

  1291   fixes x::"'a::{dense_linorder,ordered_ab_group_add_abs}"

  1292   shows "(\<And>e. 0 < e \<Longrightarrow> \<bar>x\<bar> \<le> e) ==> x = 0"

  1293   apply (cases "\<bar>x\<bar> = 0", simp)

  1294   apply (simp only: zero_less_abs_iff [symmetric])

  1295   apply (drule dense)

  1296   apply (auto simp add: not_less [symmetric])

  1297   done

  1298

  1299 hide_fact (open) ab_diff_conv_add_uminus add_0 mult_1 ab_left_minus

  1300

  1301 lemmas add_0 = add_0_left \<comment> \<open>FIXME duplicate\<close>

  1302 lemmas mult_1 = mult_1_left \<comment> \<open>FIXME duplicate\<close>

  1303 lemmas ab_left_minus = left_minus \<comment> \<open>FIXME duplicate\<close>

  1304 lemmas diff_diff_eq = diff_diff_add \<comment> \<open>FIXME duplicate\<close>

  1305

  1306 subsection \<open>Canonically ordered monoids\<close>

  1307

  1308 text \<open>Canonically ordered monoids are never groups.\<close>

  1309

  1310 class canonically_ordered_monoid_add = comm_monoid_add + order +

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

  1312 begin

  1313

  1314 lemma zero_le: "0 \<le> x"

  1315   by (auto simp: le_iff_add)

  1316

  1317 subclass ordered_comm_monoid_add

  1318   proof qed (auto simp: le_iff_add add_ac)

  1319

  1320 lemma add_eq_0_iff_both_eq_0: "x + y = 0 \<longleftrightarrow> x = 0 \<and> y = 0"

  1321   by (intro add_nonneg_eq_0_iff zero_le)

  1322

  1323 end

  1324

  1325 class ordered_cancel_comm_monoid_diff =

  1326   canonically_ordered_monoid_add + comm_monoid_diff + ordered_ab_semigroup_add_imp_le

  1327 begin

  1328

  1329 context

  1330   fixes a b

  1331   assumes "a \<le> b"

  1332 begin

  1333

  1334 lemma add_diff_inverse:

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

  1336   using \<open>a \<le> b\<close> by (auto simp add: le_iff_add)

  1337

  1338 lemma add_diff_assoc:

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

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

  1341

  1342 lemma add_diff_assoc2:

  1343   "b - a + c = b + c - a"

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

  1345

  1346 lemma diff_add_assoc:

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

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

  1349

  1350 lemma diff_add_assoc2:

  1351   "b + c - a = b - a + c"

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

  1353

  1354 lemma diff_diff_right:

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

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

  1357

  1358 lemma diff_add:

  1359   "b - a + a = b"

  1360   by (simp add: add.commute add_diff_inverse)

  1361

  1362 lemma le_add_diff:

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

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

  1365

  1366 lemma le_imp_diff_is_add:

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

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

  1369

  1370 lemma le_diff_conv2:

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

  1372 proof

  1373   assume ?P

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

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

  1376 next

  1377   assume ?Q

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

  1379   then show ?P by simp

  1380 qed

  1381

  1382 end

  1383

  1384 end

  1385

  1386 subsection \<open>Tools setup\<close>

  1387

  1388 lemma add_mono_thms_linordered_semiring:

  1389   fixes i j k :: "'a::ordered_ab_semigroup_add"

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

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

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

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

  1394 by (rule add_mono, clarify+)+

  1395

  1396 lemma add_mono_thms_linordered_field:

  1397   fixes i j k :: "'a::ordered_cancel_ab_semigroup_add"

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

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

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

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

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

  1403 by (auto intro: add_strict_right_mono add_strict_left_mono

  1404   add_less_le_mono add_le_less_mono add_strict_mono)

  1405

  1406 code_identifier

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

  1408

  1409 end