src/HOL/Groups.thy
author hoelzl
Wed Feb 10 18:43:19 2016 +0100 (2016-02-10)
changeset 62376 85f38d5f8807
parent 62348 9a5f43dac883
child 62377 ace69956d018
permissions -rw-r--r--
Rename ordered_comm_monoid_add to ordered_cancel_comm_monoid_add. Introduce ordreed_comm_monoid_add, canonically_ordered_comm_monoid and dioid. Setup nat, entat and ennreal as dioids.
     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 class ordered_cancel_ab_semigroup_add =
   593   ordered_ab_semigroup_add + cancel_ab_semigroup_add
   594 begin
   595 
   596 lemma add_strict_left_mono:
   597   "a < b \<Longrightarrow> c + a < c + b"
   598 by (auto simp add: less_le add_left_mono)
   599 
   600 lemma add_strict_right_mono:
   601   "a < b \<Longrightarrow> a + c < b + c"
   602 by (simp add: add.commute [of _ c] add_strict_left_mono)
   603 
   604 text\<open>Strict monotonicity in both arguments\<close>
   605 lemma add_strict_mono:
   606   "a < b \<Longrightarrow> c < d \<Longrightarrow> a + c < b + d"
   607 apply (erule add_strict_right_mono [THEN less_trans])
   608 apply (erule add_strict_left_mono)
   609 done
   610 
   611 lemma add_less_le_mono:
   612   "a < b \<Longrightarrow> c \<le> d \<Longrightarrow> a + c < b + d"
   613 apply (erule add_strict_right_mono [THEN less_le_trans])
   614 apply (erule add_left_mono)
   615 done
   616 
   617 lemma add_le_less_mono:
   618   "a \<le> b \<Longrightarrow> c < d \<Longrightarrow> a + c < b + d"
   619 apply (erule add_right_mono [THEN le_less_trans])
   620 apply (erule add_strict_left_mono)
   621 done
   622 
   623 end
   624 
   625 class ordered_ab_semigroup_add_imp_le =
   626   ordered_cancel_ab_semigroup_add +
   627   assumes add_le_imp_le_left: "c + a \<le> c + b \<Longrightarrow> a \<le> b"
   628 begin
   629 
   630 lemma add_less_imp_less_left:
   631   assumes less: "c + a < c + b" shows "a < b"
   632 proof -
   633   from less have le: "c + a <= c + b" by (simp add: order_le_less)
   634   have "a <= b"
   635     apply (insert le)
   636     apply (drule add_le_imp_le_left)
   637     by (insert le, drule add_le_imp_le_left, assumption)
   638   moreover have "a \<noteq> b"
   639   proof (rule ccontr)
   640     assume "~(a \<noteq> b)"
   641     then have "a = b" by simp
   642     then have "c + a = c + b" by simp
   643     with less show "False"by simp
   644   qed
   645   ultimately show "a < b" by (simp add: order_le_less)
   646 qed
   647 
   648 lemma add_less_imp_less_right:
   649   "a + c < b + c \<Longrightarrow> a < b"
   650 apply (rule add_less_imp_less_left [of c])
   651 apply (simp add: add.commute)
   652 done
   653 
   654 lemma add_less_cancel_left [simp]:
   655   "c + a < c + b \<longleftrightarrow> a < b"
   656   by (blast intro: add_less_imp_less_left add_strict_left_mono)
   657 
   658 lemma add_less_cancel_right [simp]:
   659   "a + c < b + c \<longleftrightarrow> a < b"
   660   by (blast intro: add_less_imp_less_right add_strict_right_mono)
   661 
   662 lemma add_le_cancel_left [simp]:
   663   "c + a \<le> c + b \<longleftrightarrow> a \<le> b"
   664   by (auto, drule add_le_imp_le_left, simp_all add: add_left_mono)
   665 
   666 lemma add_le_cancel_right [simp]:
   667   "a + c \<le> b + c \<longleftrightarrow> a \<le> b"
   668   by (simp add: add.commute [of a c] add.commute [of b c])
   669 
   670 lemma add_le_imp_le_right:
   671   "a + c \<le> b + c \<Longrightarrow> a \<le> b"
   672 by simp
   673 
   674 lemma max_add_distrib_left:
   675   "max x y + z = max (x + z) (y + z)"
   676   unfolding max_def by auto
   677 
   678 lemma min_add_distrib_left:
   679   "min x y + z = min (x + z) (y + z)"
   680   unfolding min_def by auto
   681 
   682 lemma max_add_distrib_right:
   683   "x + max y z = max (x + y) (x + z)"
   684   unfolding max_def by auto
   685 
   686 lemma min_add_distrib_right:
   687   "x + min y z = min (x + y) (x + z)"
   688   unfolding min_def by auto
   689 
   690 end
   691 
   692 subsection \<open>Support for reasoning about signs\<close>
   693 
   694 class ordered_comm_monoid_add = comm_monoid_add + ordered_ab_semigroup_add
   695 begin
   696 
   697 lemma add_nonneg_nonneg [simp]:
   698   assumes "0 \<le> a" and "0 \<le> b" shows "0 \<le> a + b"
   699 proof -
   700   have "0 + 0 \<le> a + b"
   701     using assms by (rule add_mono)
   702   then show ?thesis by simp
   703 qed
   704 
   705 lemma add_nonpos_nonpos:
   706   assumes "a \<le> 0" and "b \<le> 0" shows "a + b \<le> 0"
   707 proof -
   708   have "a + b \<le> 0 + 0"
   709     using assms by (rule add_mono)
   710   then show ?thesis by simp
   711 qed
   712 
   713 lemma add_nonneg_eq_0_iff:
   714   assumes x: "0 \<le> x" and y: "0 \<le> y"
   715   shows "x + y = 0 \<longleftrightarrow> x = 0 \<and> y = 0"
   716 proof (intro iffI conjI)
   717   have "x = x + 0" by simp
   718   also have "x + 0 \<le> x + y" using y by (rule add_left_mono)
   719   also assume "x + y = 0"
   720   also have "0 \<le> x" using x .
   721   finally show "x = 0" .
   722 next
   723   have "y = 0 + y" by simp
   724   also have "0 + y \<le> x + y" using x by (rule add_right_mono)
   725   also assume "x + y = 0"
   726   also have "0 \<le> y" using y .
   727   finally show "y = 0" .
   728 next
   729   assume "x = 0 \<and> y = 0"
   730   then show "x + y = 0" by simp
   731 qed
   732 
   733 lemma add_increasing:
   734   "0 \<le> a \<Longrightarrow> b \<le> c \<Longrightarrow> b \<le> a + c"
   735   by (insert add_mono [of 0 a b c], simp)
   736 
   737 lemma add_increasing2:
   738   "0 \<le> c \<Longrightarrow> b \<le> a \<Longrightarrow> b \<le> a + c"
   739   by (simp add: add_increasing add.commute [of a])
   740 
   741 end
   742 
   743 class canonically_ordered_monoid_add = comm_monoid_add + order +
   744   assumes le_iff_add: "a \<le> b \<longleftrightarrow> (\<exists>c. b = a + c)"
   745 begin
   746 
   747 subclass ordered_comm_monoid_add
   748   proof qed (auto simp: le_iff_add add_ac)
   749 
   750 lemma zero_le: "0 \<le> x"
   751   by (auto simp: le_iff_add)
   752 
   753 lemma add_eq_0_iff_both_eq_0: "x + y = 0 \<longleftrightarrow> x = 0 \<and> y = 0"
   754   by (intro add_nonneg_eq_0_iff zero_le)
   755 
   756 end
   757 
   758 class ordered_cancel_comm_monoid_diff =
   759   canonically_ordered_monoid_add + comm_monoid_diff + ordered_ab_semigroup_add_imp_le
   760 begin
   761 
   762 context
   763   fixes a b
   764   assumes "a \<le> b"
   765 begin
   766 
   767 lemma add_diff_inverse:
   768   "a + (b - a) = b"
   769   using \<open>a \<le> b\<close> by (auto simp add: le_iff_add)
   770 
   771 lemma add_diff_assoc:
   772   "c + (b - a) = c + b - a"
   773   using \<open>a \<le> b\<close> by (auto simp add: le_iff_add add.left_commute [of c])
   774 
   775 lemma add_diff_assoc2:
   776   "b - a + c = b + c - a"
   777   using \<open>a \<le> b\<close> by (auto simp add: le_iff_add add.assoc)
   778 
   779 lemma diff_add_assoc:
   780   "c + b - a = c + (b - a)"
   781   using \<open>a \<le> b\<close> by (simp add: add.commute add_diff_assoc)
   782 
   783 lemma diff_add_assoc2:
   784   "b + c - a = b - a + c"
   785   using \<open>a \<le> b\<close>by (simp add: add.commute add_diff_assoc)
   786 
   787 lemma diff_diff_right:
   788   "c - (b - a) = c + a - b"
   789   by (simp add: add_diff_inverse add_diff_cancel_left [of a c "b - a", symmetric] add.commute)
   790 
   791 lemma diff_add:
   792   "b - a + a = b"
   793   by (simp add: add.commute add_diff_inverse)
   794 
   795 lemma le_add_diff:
   796   "c \<le> b + c - a"
   797   by (auto simp add: add.commute diff_add_assoc2 le_iff_add)
   798 
   799 lemma le_imp_diff_is_add:
   800   "a \<le> b \<Longrightarrow> b - a = c \<longleftrightarrow> b = c + a"
   801   by (auto simp add: add.commute add_diff_inverse)
   802 
   803 lemma le_diff_conv2:
   804   "c \<le> b - a \<longleftrightarrow> c + a \<le> b" (is "?P \<longleftrightarrow> ?Q")
   805 proof
   806   assume ?P
   807   then have "c + a \<le> b - a + a" by (rule add_right_mono)
   808   then show ?Q by (simp add: add_diff_inverse add.commute)
   809 next
   810   assume ?Q
   811   then have "a + c \<le> a + (b - a)" by (simp add: add_diff_inverse add.commute)
   812   then show ?P by simp
   813 qed
   814 
   815 end
   816 
   817 end
   818 
   819 class ordered_cancel_comm_monoid_add =
   820   ordered_comm_monoid_add + cancel_ab_semigroup_add
   821 begin
   822 
   823 subclass ordered_cancel_ab_semigroup_add ..
   824 
   825 lemma add_neg_nonpos:
   826   assumes "a < 0" and "b \<le> 0" shows "a + b < 0"
   827 proof -
   828   have "a + b < 0 + 0"
   829     using assms by (rule add_less_le_mono)
   830   then show ?thesis by simp
   831 qed
   832 
   833 lemma add_neg_neg:
   834   assumes "a < 0" and "b < 0" shows "a + b < 0"
   835 by (rule add_neg_nonpos) (insert assms, auto)
   836 
   837 lemma add_nonpos_neg:
   838   assumes "a \<le> 0" and "b < 0" shows "a + b < 0"
   839 proof -
   840   have "a + b < 0 + 0"
   841     using assms by (rule add_le_less_mono)
   842   then show ?thesis by simp
   843 qed
   844 
   845 lemma add_pos_nonneg:
   846   assumes "0 < a" and "0 \<le> b" shows "0 < a + b"
   847 proof -
   848   have "0 + 0 < a + b"
   849     using assms by (rule add_less_le_mono)
   850   then show ?thesis by simp
   851 qed
   852 
   853 lemma add_pos_pos:
   854   assumes "0 < a" and "0 < b" shows "0 < a + b"
   855 by (rule add_pos_nonneg) (insert assms, auto)
   856 
   857 lemma add_nonneg_pos:
   858   assumes "0 \<le> a" and "0 < b" shows "0 < a + b"
   859 proof -
   860   have "0 + 0 < a + b"
   861     using assms by (rule add_le_less_mono)
   862   then show ?thesis by simp
   863 qed
   864 
   865 lemmas add_sign_intros =
   866   add_pos_nonneg add_pos_pos add_nonneg_pos add_nonneg_nonneg
   867   add_neg_nonpos add_neg_neg add_nonpos_neg add_nonpos_nonpos
   868 
   869 lemma add_strict_increasing:
   870   "0 < a \<Longrightarrow> b \<le> c \<Longrightarrow> b < a + c"
   871   by (insert add_less_le_mono [of 0 a b c], simp)
   872 
   873 lemma add_strict_increasing2:
   874   "0 \<le> a \<Longrightarrow> b < c \<Longrightarrow> b < a + c"
   875   by (insert add_le_less_mono [of 0 a b c], simp)
   876 
   877 end
   878 
   879 class ordered_ab_group_add = ab_group_add + ordered_ab_semigroup_add
   880 begin
   881 
   882 subclass ordered_cancel_ab_semigroup_add ..
   883 
   884 subclass ordered_ab_semigroup_add_imp_le
   885 proof
   886   fix a b c :: 'a
   887   assume "c + a \<le> c + b"
   888   hence "(-c) + (c + a) \<le> (-c) + (c + b)" by (rule add_left_mono)
   889   hence "((-c) + c) + a \<le> ((-c) + c) + b" by (simp only: add.assoc)
   890   thus "a \<le> b" by simp
   891 qed
   892 
   893 subclass ordered_cancel_comm_monoid_add ..
   894 
   895 lemma add_less_same_cancel1 [simp]:
   896   "b + a < b \<longleftrightarrow> a < 0"
   897   using add_less_cancel_left [of _ _ 0] by simp
   898 
   899 lemma add_less_same_cancel2 [simp]:
   900   "a + b < b \<longleftrightarrow> a < 0"
   901   using add_less_cancel_right [of _ _ 0] by simp
   902 
   903 lemma less_add_same_cancel1 [simp]:
   904   "a < a + b \<longleftrightarrow> 0 < b"
   905   using add_less_cancel_left [of _ 0] by simp
   906 
   907 lemma less_add_same_cancel2 [simp]:
   908   "a < b + a \<longleftrightarrow> 0 < b"
   909   using add_less_cancel_right [of 0] by simp
   910 
   911 lemma add_le_same_cancel1 [simp]:
   912   "b + a \<le> b \<longleftrightarrow> a \<le> 0"
   913   using add_le_cancel_left [of _ _ 0] by simp
   914 
   915 lemma add_le_same_cancel2 [simp]:
   916   "a + b \<le> b \<longleftrightarrow> a \<le> 0"
   917   using add_le_cancel_right [of _ _ 0] by simp
   918 
   919 lemma le_add_same_cancel1 [simp]:
   920   "a \<le> a + b \<longleftrightarrow> 0 \<le> b"
   921   using add_le_cancel_left [of _ 0] by simp
   922 
   923 lemma le_add_same_cancel2 [simp]:
   924   "a \<le> b + a \<longleftrightarrow> 0 \<le> b"
   925   using add_le_cancel_right [of 0] by simp
   926 
   927 lemma max_diff_distrib_left:
   928   shows "max x y - z = max (x - z) (y - z)"
   929   using max_add_distrib_left [of x y "- z"] by simp
   930 
   931 lemma min_diff_distrib_left:
   932   shows "min x y - z = min (x - z) (y - z)"
   933   using min_add_distrib_left [of x y "- z"] by simp
   934 
   935 lemma le_imp_neg_le:
   936   assumes "a \<le> b" shows "-b \<le> -a"
   937 proof -
   938   have "-a+a \<le> -a+b" using \<open>a \<le> b\<close> by (rule add_left_mono)
   939   then have "0 \<le> -a+b" by simp
   940   then have "0 + (-b) \<le> (-a + b) + (-b)" by (rule add_right_mono)
   941   then show ?thesis by (simp add: algebra_simps)
   942 qed
   943 
   944 lemma neg_le_iff_le [simp]: "- b \<le> - a \<longleftrightarrow> a \<le> b"
   945 proof
   946   assume "- b \<le> - a"
   947   hence "- (- a) \<le> - (- b)" by (rule le_imp_neg_le)
   948   thus "a\<le>b" by simp
   949 next
   950   assume "a\<le>b"
   951   thus "-b \<le> -a" by (rule le_imp_neg_le)
   952 qed
   953 
   954 lemma neg_le_0_iff_le [simp]: "- a \<le> 0 \<longleftrightarrow> 0 \<le> a"
   955 by (subst neg_le_iff_le [symmetric], simp)
   956 
   957 lemma neg_0_le_iff_le [simp]: "0 \<le> - a \<longleftrightarrow> a \<le> 0"
   958 by (subst neg_le_iff_le [symmetric], simp)
   959 
   960 lemma neg_less_iff_less [simp]: "- b < - a \<longleftrightarrow> a < b"
   961 by (force simp add: less_le)
   962 
   963 lemma neg_less_0_iff_less [simp]: "- a < 0 \<longleftrightarrow> 0 < a"
   964 by (subst neg_less_iff_less [symmetric], simp)
   965 
   966 lemma neg_0_less_iff_less [simp]: "0 < - a \<longleftrightarrow> a < 0"
   967 by (subst neg_less_iff_less [symmetric], simp)
   968 
   969 text\<open>The next several equations can make the simplifier loop!\<close>
   970 
   971 lemma less_minus_iff: "a < - b \<longleftrightarrow> b < - a"
   972 proof -
   973   have "(- (-a) < - b) = (b < - a)" by (rule neg_less_iff_less)
   974   thus ?thesis by simp
   975 qed
   976 
   977 lemma minus_less_iff: "- a < b \<longleftrightarrow> - b < a"
   978 proof -
   979   have "(- a < - (-b)) = (- b < a)" by (rule neg_less_iff_less)
   980   thus ?thesis by simp
   981 qed
   982 
   983 lemma le_minus_iff: "a \<le> - b \<longleftrightarrow> b \<le> - a"
   984 proof -
   985   have mm: "!! a (b::'a). (-(-a)) < -b \<Longrightarrow> -(-b) < -a" by (simp only: minus_less_iff)
   986   have "(- (- a) <= -b) = (b <= - a)"
   987     apply (auto simp only: le_less)
   988     apply (drule mm)
   989     apply (simp_all)
   990     apply (drule mm[simplified], assumption)
   991     done
   992   then show ?thesis by simp
   993 qed
   994 
   995 lemma minus_le_iff: "- a \<le> b \<longleftrightarrow> - b \<le> a"
   996 by (auto simp add: le_less minus_less_iff)
   997 
   998 lemma diff_less_0_iff_less [simp]:
   999   "a - b < 0 \<longleftrightarrow> a < b"
  1000 proof -
  1001   have "a - b < 0 \<longleftrightarrow> a + (- b) < b + (- b)" by simp
  1002   also have "... \<longleftrightarrow> a < b" by (simp only: add_less_cancel_right)
  1003   finally show ?thesis .
  1004 qed
  1005 
  1006 lemmas less_iff_diff_less_0 = diff_less_0_iff_less [symmetric]
  1007 
  1008 lemma diff_less_eq [algebra_simps, field_simps]:
  1009   "a - b < c \<longleftrightarrow> a < c + b"
  1010 apply (subst less_iff_diff_less_0 [of a])
  1011 apply (rule less_iff_diff_less_0 [of _ c, THEN ssubst])
  1012 apply (simp add: algebra_simps)
  1013 done
  1014 
  1015 lemma less_diff_eq[algebra_simps, field_simps]:
  1016   "a < c - b \<longleftrightarrow> a + b < c"
  1017 apply (subst less_iff_diff_less_0 [of "a + b"])
  1018 apply (subst less_iff_diff_less_0 [of a])
  1019 apply (simp add: algebra_simps)
  1020 done
  1021 
  1022 lemma diff_gt_0_iff_gt [simp]:
  1023   "a - b > 0 \<longleftrightarrow> a > b"
  1024   by (simp add: less_diff_eq)
  1025 
  1026 lemma diff_le_eq [algebra_simps, field_simps]:
  1027   "a - b \<le> c \<longleftrightarrow> a \<le> c + b"
  1028   by (auto simp add: le_less diff_less_eq )
  1029 
  1030 lemma le_diff_eq [algebra_simps, field_simps]:
  1031   "a \<le> c - b \<longleftrightarrow> a + b \<le> c"
  1032   by (auto simp add: le_less less_diff_eq)
  1033 
  1034 lemma diff_le_0_iff_le [simp]:
  1035   "a - b \<le> 0 \<longleftrightarrow> a \<le> b"
  1036   by (simp add: algebra_simps)
  1037 
  1038 lemmas le_iff_diff_le_0 = diff_le_0_iff_le [symmetric]
  1039 
  1040 lemma diff_ge_0_iff_ge [simp]:
  1041   "a - b \<ge> 0 \<longleftrightarrow> a \<ge> b"
  1042   by (simp add: le_diff_eq)
  1043 
  1044 lemma diff_eq_diff_less:
  1045   "a - b = c - d \<Longrightarrow> a < b \<longleftrightarrow> c < d"
  1046   by (auto simp only: less_iff_diff_less_0 [of a b] less_iff_diff_less_0 [of c d])
  1047 
  1048 lemma diff_eq_diff_less_eq:
  1049   "a - b = c - d \<Longrightarrow> a \<le> b \<longleftrightarrow> c \<le> d"
  1050   by (auto simp only: le_iff_diff_le_0 [of a b] le_iff_diff_le_0 [of c d])
  1051 
  1052 lemma diff_mono: "a \<le> b \<Longrightarrow> d \<le> c \<Longrightarrow> a - c \<le> b - d"
  1053   by (simp add: field_simps add_mono)
  1054 
  1055 lemma diff_left_mono: "b \<le> a \<Longrightarrow> c - a \<le> c - b"
  1056   by (simp add: field_simps)
  1057 
  1058 lemma diff_right_mono: "a \<le> b \<Longrightarrow> a - c \<le> b - c"
  1059   by (simp add: field_simps)
  1060 
  1061 lemma diff_strict_mono: "a < b \<Longrightarrow> d < c \<Longrightarrow> a - c < b - d"
  1062   by (simp add: field_simps add_strict_mono)
  1063 
  1064 lemma diff_strict_left_mono: "b < a \<Longrightarrow> c - a < c - b"
  1065   by (simp add: field_simps)
  1066 
  1067 lemma diff_strict_right_mono: "a < b \<Longrightarrow> a - c < b - c"
  1068   by (simp add: field_simps)
  1069 
  1070 end
  1071 
  1072 ML_file "Tools/group_cancel.ML"
  1073 
  1074 simproc_setup group_cancel_add ("a + b::'a::ab_group_add") =
  1075   \<open>fn phi => fn ss => try Group_Cancel.cancel_add_conv\<close>
  1076 
  1077 simproc_setup group_cancel_diff ("a - b::'a::ab_group_add") =
  1078   \<open>fn phi => fn ss => try Group_Cancel.cancel_diff_conv\<close>
  1079 
  1080 simproc_setup group_cancel_eq ("a = (b::'a::ab_group_add)") =
  1081   \<open>fn phi => fn ss => try Group_Cancel.cancel_eq_conv\<close>
  1082 
  1083 simproc_setup group_cancel_le ("a \<le> (b::'a::ordered_ab_group_add)") =
  1084   \<open>fn phi => fn ss => try Group_Cancel.cancel_le_conv\<close>
  1085 
  1086 simproc_setup group_cancel_less ("a < (b::'a::ordered_ab_group_add)") =
  1087   \<open>fn phi => fn ss => try Group_Cancel.cancel_less_conv\<close>
  1088 
  1089 class linordered_ab_semigroup_add =
  1090   linorder + ordered_ab_semigroup_add
  1091 
  1092 class linordered_cancel_ab_semigroup_add =
  1093   linorder + ordered_cancel_ab_semigroup_add
  1094 begin
  1095 
  1096 subclass linordered_ab_semigroup_add ..
  1097 
  1098 subclass ordered_ab_semigroup_add_imp_le
  1099 proof
  1100   fix a b c :: 'a
  1101   assume le: "c + a <= c + b"
  1102   show "a <= b"
  1103   proof (rule ccontr)
  1104     assume w: "~ a \<le> b"
  1105     hence "b <= a" by (simp add: linorder_not_le)
  1106     hence le2: "c + b <= c + a" by (rule add_left_mono)
  1107     have "a = b"
  1108       apply (insert le)
  1109       apply (insert le2)
  1110       apply (drule antisym, simp_all)
  1111       done
  1112     with w show False
  1113       by (simp add: linorder_not_le [symmetric])
  1114   qed
  1115 qed
  1116 
  1117 end
  1118 
  1119 class linordered_ab_group_add = linorder + ordered_ab_group_add
  1120 begin
  1121 
  1122 subclass linordered_cancel_ab_semigroup_add ..
  1123 
  1124 lemma equal_neg_zero [simp]:
  1125   "a = - a \<longleftrightarrow> a = 0"
  1126 proof
  1127   assume "a = 0" then show "a = - a" by simp
  1128 next
  1129   assume A: "a = - a" show "a = 0"
  1130   proof (cases "0 \<le> a")
  1131     case True with A have "0 \<le> - a" by auto
  1132     with le_minus_iff have "a \<le> 0" by simp
  1133     with True show ?thesis by (auto intro: order_trans)
  1134   next
  1135     case False then have B: "a \<le> 0" by auto
  1136     with A have "- a \<le> 0" by auto
  1137     with B show ?thesis by (auto intro: order_trans)
  1138   qed
  1139 qed
  1140 
  1141 lemma neg_equal_zero [simp]:
  1142   "- a = a \<longleftrightarrow> a = 0"
  1143   by (auto dest: sym)
  1144 
  1145 lemma neg_less_eq_nonneg [simp]:
  1146   "- a \<le> a \<longleftrightarrow> 0 \<le> a"
  1147 proof
  1148   assume A: "- a \<le> a" show "0 \<le> a"
  1149   proof (rule classical)
  1150     assume "\<not> 0 \<le> a"
  1151     then have "a < 0" by auto
  1152     with A have "- a < 0" by (rule le_less_trans)
  1153     then show ?thesis by auto
  1154   qed
  1155 next
  1156   assume A: "0 \<le> a" show "- a \<le> a"
  1157   proof (rule order_trans)
  1158     show "- a \<le> 0" using A by (simp add: minus_le_iff)
  1159   next
  1160     show "0 \<le> a" using A .
  1161   qed
  1162 qed
  1163 
  1164 lemma neg_less_pos [simp]:
  1165   "- a < a \<longleftrightarrow> 0 < a"
  1166   by (auto simp add: less_le)
  1167 
  1168 lemma less_eq_neg_nonpos [simp]:
  1169   "a \<le> - a \<longleftrightarrow> a \<le> 0"
  1170   using neg_less_eq_nonneg [of "- a"] by simp
  1171 
  1172 lemma less_neg_neg [simp]:
  1173   "a < - a \<longleftrightarrow> a < 0"
  1174   using neg_less_pos [of "- a"] by simp
  1175 
  1176 lemma double_zero [simp]:
  1177   "a + a = 0 \<longleftrightarrow> a = 0"
  1178 proof
  1179   assume assm: "a + a = 0"
  1180   then have a: "- a = a" by (rule minus_unique)
  1181   then show "a = 0" by (simp only: neg_equal_zero)
  1182 qed simp
  1183 
  1184 lemma double_zero_sym [simp]:
  1185   "0 = a + a \<longleftrightarrow> a = 0"
  1186   by (rule, drule sym) simp_all
  1187 
  1188 lemma zero_less_double_add_iff_zero_less_single_add [simp]:
  1189   "0 < a + a \<longleftrightarrow> 0 < a"
  1190 proof
  1191   assume "0 < a + a"
  1192   then have "0 - a < a" by (simp only: diff_less_eq)
  1193   then have "- a < a" by simp
  1194   then show "0 < a" by simp
  1195 next
  1196   assume "0 < a"
  1197   with this have "0 + 0 < a + a"
  1198     by (rule add_strict_mono)
  1199   then show "0 < a + a" by simp
  1200 qed
  1201 
  1202 lemma zero_le_double_add_iff_zero_le_single_add [simp]:
  1203   "0 \<le> a + a \<longleftrightarrow> 0 \<le> a"
  1204   by (auto simp add: le_less)
  1205 
  1206 lemma double_add_less_zero_iff_single_add_less_zero [simp]:
  1207   "a + a < 0 \<longleftrightarrow> a < 0"
  1208 proof -
  1209   have "\<not> a + a < 0 \<longleftrightarrow> \<not> a < 0"
  1210     by (simp add: not_less)
  1211   then show ?thesis by simp
  1212 qed
  1213 
  1214 lemma double_add_le_zero_iff_single_add_le_zero [simp]:
  1215   "a + a \<le> 0 \<longleftrightarrow> a \<le> 0"
  1216 proof -
  1217   have "\<not> a + a \<le> 0 \<longleftrightarrow> \<not> a \<le> 0"
  1218     by (simp add: not_le)
  1219   then show ?thesis by simp
  1220 qed
  1221 
  1222 lemma minus_max_eq_min:
  1223   "- max x y = min (-x) (-y)"
  1224   by (auto simp add: max_def min_def)
  1225 
  1226 lemma minus_min_eq_max:
  1227   "- min x y = max (-x) (-y)"
  1228   by (auto simp add: max_def min_def)
  1229 
  1230 end
  1231 
  1232 class abs =
  1233   fixes abs :: "'a \<Rightarrow> 'a"  ("\<bar>_\<bar>")
  1234 
  1235 class sgn =
  1236   fixes sgn :: "'a \<Rightarrow> 'a"
  1237 
  1238 class abs_if = minus + uminus + ord + zero + abs +
  1239   assumes abs_if: "\<bar>a\<bar> = (if a < 0 then - a else a)"
  1240 
  1241 class sgn_if = minus + uminus + zero + one + ord + sgn +
  1242   assumes sgn_if: "sgn x = (if x = 0 then 0 else if 0 < x then 1 else - 1)"
  1243 begin
  1244 
  1245 lemma sgn0 [simp]: "sgn 0 = 0"
  1246   by (simp add:sgn_if)
  1247 
  1248 end
  1249 
  1250 class ordered_ab_group_add_abs = ordered_ab_group_add + abs +
  1251   assumes abs_ge_zero [simp]: "\<bar>a\<bar> \<ge> 0"
  1252     and abs_ge_self: "a \<le> \<bar>a\<bar>"
  1253     and abs_leI: "a \<le> b \<Longrightarrow> - a \<le> b \<Longrightarrow> \<bar>a\<bar> \<le> b"
  1254     and abs_minus_cancel [simp]: "\<bar>-a\<bar> = \<bar>a\<bar>"
  1255     and abs_triangle_ineq: "\<bar>a + b\<bar> \<le> \<bar>a\<bar> + \<bar>b\<bar>"
  1256 begin
  1257 
  1258 lemma abs_minus_le_zero: "- \<bar>a\<bar> \<le> 0"
  1259   unfolding neg_le_0_iff_le by simp
  1260 
  1261 lemma abs_of_nonneg [simp]:
  1262   assumes nonneg: "0 \<le> a" shows "\<bar>a\<bar> = a"
  1263 proof (rule antisym)
  1264   from nonneg le_imp_neg_le have "- a \<le> 0" by simp
  1265   from this nonneg have "- a \<le> a" by (rule order_trans)
  1266   then show "\<bar>a\<bar> \<le> a" by (auto intro: abs_leI)
  1267 qed (rule abs_ge_self)
  1268 
  1269 lemma abs_idempotent [simp]: "\<bar>\<bar>a\<bar>\<bar> = \<bar>a\<bar>"
  1270 by (rule antisym)
  1271    (auto intro!: abs_ge_self abs_leI order_trans [of "- \<bar>a\<bar>" 0 "\<bar>a\<bar>"])
  1272 
  1273 lemma abs_eq_0 [simp]: "\<bar>a\<bar> = 0 \<longleftrightarrow> a = 0"
  1274 proof -
  1275   have "\<bar>a\<bar> = 0 \<Longrightarrow> a = 0"
  1276   proof (rule antisym)
  1277     assume zero: "\<bar>a\<bar> = 0"
  1278     with abs_ge_self show "a \<le> 0" by auto
  1279     from zero have "\<bar>-a\<bar> = 0" by simp
  1280     with abs_ge_self [of "- a"] have "- a \<le> 0" by auto
  1281     with neg_le_0_iff_le show "0 \<le> a" by auto
  1282   qed
  1283   then show ?thesis by auto
  1284 qed
  1285 
  1286 lemma abs_zero [simp]: "\<bar>0\<bar> = 0"
  1287 by simp
  1288 
  1289 lemma abs_0_eq [simp]: "0 = \<bar>a\<bar> \<longleftrightarrow> a = 0"
  1290 proof -
  1291   have "0 = \<bar>a\<bar> \<longleftrightarrow> \<bar>a\<bar> = 0" by (simp only: eq_ac)
  1292   thus ?thesis by simp
  1293 qed
  1294 
  1295 lemma abs_le_zero_iff [simp]: "\<bar>a\<bar> \<le> 0 \<longleftrightarrow> a = 0"
  1296 proof
  1297   assume "\<bar>a\<bar> \<le> 0"
  1298   then have "\<bar>a\<bar> = 0" by (rule antisym) simp
  1299   thus "a = 0" by simp
  1300 next
  1301   assume "a = 0"
  1302   thus "\<bar>a\<bar> \<le> 0" by simp
  1303 qed
  1304 
  1305 lemma zero_less_abs_iff [simp]: "0 < \<bar>a\<bar> \<longleftrightarrow> a \<noteq> 0"
  1306 by (simp add: less_le)
  1307 
  1308 lemma abs_not_less_zero [simp]: "\<not> \<bar>a\<bar> < 0"
  1309 proof -
  1310   have a: "\<And>x y. x \<le> y \<Longrightarrow> \<not> y < x" by auto
  1311   show ?thesis by (simp add: a)
  1312 qed
  1313 
  1314 lemma abs_ge_minus_self: "- a \<le> \<bar>a\<bar>"
  1315 proof -
  1316   have "- a \<le> \<bar>-a\<bar>" by (rule abs_ge_self)
  1317   then show ?thesis by simp
  1318 qed
  1319 
  1320 lemma abs_minus_commute:
  1321   "\<bar>a - b\<bar> = \<bar>b - a\<bar>"
  1322 proof -
  1323   have "\<bar>a - b\<bar> = \<bar>- (a - b)\<bar>" by (simp only: abs_minus_cancel)
  1324   also have "... = \<bar>b - a\<bar>" by simp
  1325   finally show ?thesis .
  1326 qed
  1327 
  1328 lemma abs_of_pos: "0 < a \<Longrightarrow> \<bar>a\<bar> = a"
  1329 by (rule abs_of_nonneg, rule less_imp_le)
  1330 
  1331 lemma abs_of_nonpos [simp]:
  1332   assumes "a \<le> 0" shows "\<bar>a\<bar> = - a"
  1333 proof -
  1334   let ?b = "- a"
  1335   have "- ?b \<le> 0 \<Longrightarrow> \<bar>- ?b\<bar> = - (- ?b)"
  1336   unfolding abs_minus_cancel [of "?b"]
  1337   unfolding neg_le_0_iff_le [of "?b"]
  1338   unfolding minus_minus by (erule abs_of_nonneg)
  1339   then show ?thesis using assms by auto
  1340 qed
  1341 
  1342 lemma abs_of_neg: "a < 0 \<Longrightarrow> \<bar>a\<bar> = - a"
  1343 by (rule abs_of_nonpos, rule less_imp_le)
  1344 
  1345 lemma abs_le_D1: "\<bar>a\<bar> \<le> b \<Longrightarrow> a \<le> b"
  1346 by (insert abs_ge_self, blast intro: order_trans)
  1347 
  1348 lemma abs_le_D2: "\<bar>a\<bar> \<le> b \<Longrightarrow> - a \<le> b"
  1349 by (insert abs_le_D1 [of "- a"], simp)
  1350 
  1351 lemma abs_le_iff: "\<bar>a\<bar> \<le> b \<longleftrightarrow> a \<le> b \<and> - a \<le> b"
  1352 by (blast intro: abs_leI dest: abs_le_D1 abs_le_D2)
  1353 
  1354 lemma abs_triangle_ineq2: "\<bar>a\<bar> - \<bar>b\<bar> \<le> \<bar>a - b\<bar>"
  1355 proof -
  1356   have "\<bar>a\<bar> = \<bar>b + (a - b)\<bar>"
  1357     by (simp add: algebra_simps)
  1358   then have "\<bar>a\<bar> \<le> \<bar>b\<bar> + \<bar>a - b\<bar>"
  1359     by (simp add: abs_triangle_ineq)
  1360   then show ?thesis
  1361     by (simp add: algebra_simps)
  1362 qed
  1363 
  1364 lemma abs_triangle_ineq2_sym: "\<bar>a\<bar> - \<bar>b\<bar> \<le> \<bar>b - a\<bar>"
  1365   by (simp only: abs_minus_commute [of b] abs_triangle_ineq2)
  1366 
  1367 lemma abs_triangle_ineq3: "\<bar>\<bar>a\<bar> - \<bar>b\<bar>\<bar> \<le> \<bar>a - b\<bar>"
  1368   by (simp add: abs_le_iff abs_triangle_ineq2 abs_triangle_ineq2_sym)
  1369 
  1370 lemma abs_triangle_ineq4: "\<bar>a - b\<bar> \<le> \<bar>a\<bar> + \<bar>b\<bar>"
  1371 proof -
  1372   have "\<bar>a - b\<bar> = \<bar>a + - b\<bar>" by (simp add: algebra_simps)
  1373   also have "... \<le> \<bar>a\<bar> + \<bar>- b\<bar>" by (rule abs_triangle_ineq)
  1374   finally show ?thesis by simp
  1375 qed
  1376 
  1377 lemma abs_diff_triangle_ineq: "\<bar>a + b - (c + d)\<bar> \<le> \<bar>a - c\<bar> + \<bar>b - d\<bar>"
  1378 proof -
  1379   have "\<bar>a + b - (c+d)\<bar> = \<bar>(a-c) + (b-d)\<bar>" by (simp add: algebra_simps)
  1380   also have "... \<le> \<bar>a-c\<bar> + \<bar>b-d\<bar>" by (rule abs_triangle_ineq)
  1381   finally show ?thesis .
  1382 qed
  1383 
  1384 lemma abs_add_abs [simp]:
  1385   "\<bar>\<bar>a\<bar> + \<bar>b\<bar>\<bar> = \<bar>a\<bar> + \<bar>b\<bar>" (is "?L = ?R")
  1386 proof (rule antisym)
  1387   show "?L \<ge> ?R" by(rule abs_ge_self)
  1388 next
  1389   have "?L \<le> \<bar>\<bar>a\<bar>\<bar> + \<bar>\<bar>b\<bar>\<bar>" by(rule abs_triangle_ineq)
  1390   also have "\<dots> = ?R" by simp
  1391   finally show "?L \<le> ?R" .
  1392 qed
  1393 
  1394 end
  1395 
  1396 lemma dense_eq0_I:
  1397   fixes x::"'a::{dense_linorder,ordered_ab_group_add_abs}"
  1398   shows "(\<And>e. 0 < e \<Longrightarrow> \<bar>x\<bar> \<le> e) ==> x = 0"
  1399   apply (cases "\<bar>x\<bar> = 0", simp)
  1400   apply (simp only: zero_less_abs_iff [symmetric])
  1401   apply (drule dense)
  1402   apply (auto simp add: not_less [symmetric])
  1403   done
  1404 
  1405 hide_fact (open) ab_diff_conv_add_uminus add_0 mult_1 ab_left_minus
  1406 
  1407 lemmas add_0 = add_0_left \<comment> \<open>FIXME duplicate\<close>
  1408 lemmas mult_1 = mult_1_left \<comment> \<open>FIXME duplicate\<close>
  1409 lemmas ab_left_minus = left_minus \<comment> \<open>FIXME duplicate\<close>
  1410 lemmas diff_diff_eq = diff_diff_add \<comment> \<open>FIXME duplicate\<close>
  1411 
  1412 subsection \<open>Tools setup\<close>
  1413 
  1414 lemma add_mono_thms_linordered_semiring:
  1415   fixes i j k :: "'a::ordered_ab_semigroup_add"
  1416   shows "i \<le> j \<and> k \<le> l \<Longrightarrow> i + k \<le> j + l"
  1417     and "i = j \<and> k \<le> l \<Longrightarrow> i + k \<le> j + l"
  1418     and "i \<le> j \<and> k = l \<Longrightarrow> i + k \<le> j + l"
  1419     and "i = j \<and> k = l \<Longrightarrow> i + k = j + l"
  1420 by (rule add_mono, clarify+)+
  1421 
  1422 lemma add_mono_thms_linordered_field:
  1423   fixes i j k :: "'a::ordered_cancel_ab_semigroup_add"
  1424   shows "i < j \<and> k = l \<Longrightarrow> i + k < j + l"
  1425     and "i = j \<and> k < l \<Longrightarrow> i + k < j + l"
  1426     and "i < j \<and> k \<le> l \<Longrightarrow> i + k < j + l"
  1427     and "i \<le> j \<and> k < l \<Longrightarrow> i + k < j + l"
  1428     and "i < j \<and> k < l \<Longrightarrow> i + k < j + l"
  1429 by (auto intro: add_strict_right_mono add_strict_left_mono
  1430   add_less_le_mono add_le_less_mono add_strict_mono)
  1431 
  1432 code_identifier
  1433   code_module Groups \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith
  1434 
  1435 end
  1436