src/HOL/Groups.thy
author paulson <lp15@cam.ac.uk>
Mon Feb 22 14:37:56 2016 +0000 (2016-02-22)
changeset 62379 340738057c8c
parent 62378 85ed00c1fe7c
child 62608 19f87fa0cfcb
permissions -rw-r--r--
An assortment of useful lemmas about sums, norm, etc. Also: norm_conv_dist [symmetric] is now a simprule!
     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 begin
   757 
   758 lemma pos_add_strict:
   759   shows "0 < a \<Longrightarrow> b < c \<Longrightarrow> b < a + c"
   760   using add_strict_mono [of 0 a b c] by simp
   761 
   762 end
   763 
   764 class ordered_cancel_comm_monoid_add = ordered_comm_monoid_add + cancel_ab_semigroup_add
   765 begin
   766 
   767 subclass ordered_cancel_ab_semigroup_add ..
   768 subclass strict_ordered_comm_monoid_add ..
   769 
   770 lemma add_strict_increasing:
   771   "0 < a \<Longrightarrow> b \<le> c \<Longrightarrow> b < a + c"
   772   by (insert add_less_le_mono [of 0 a b c], simp)
   773 
   774 lemma add_strict_increasing2:
   775   "0 \<le> a \<Longrightarrow> b < c \<Longrightarrow> b < a + c"
   776   by (insert add_le_less_mono [of 0 a b c], simp)
   777 
   778 end
   779 
   780 class ordered_ab_group_add = ab_group_add + ordered_ab_semigroup_add
   781 begin
   782 
   783 subclass ordered_cancel_ab_semigroup_add ..
   784 
   785 subclass ordered_ab_semigroup_add_imp_le
   786 proof
   787   fix a b c :: 'a
   788   assume "c + a \<le> c + b"
   789   hence "(-c) + (c + a) \<le> (-c) + (c + b)" by (rule add_left_mono)
   790   hence "((-c) + c) + a \<le> ((-c) + c) + b" by (simp only: add.assoc)
   791   thus "a \<le> b" by simp
   792 qed
   793 
   794 subclass ordered_cancel_comm_monoid_add ..
   795 
   796 lemma add_less_same_cancel1 [simp]:
   797   "b + a < b \<longleftrightarrow> a < 0"
   798   using add_less_cancel_left [of _ _ 0] by simp
   799 
   800 lemma add_less_same_cancel2 [simp]:
   801   "a + b < b \<longleftrightarrow> a < 0"
   802   using add_less_cancel_right [of _ _ 0] by simp
   803 
   804 lemma less_add_same_cancel1 [simp]:
   805   "a < a + b \<longleftrightarrow> 0 < b"
   806   using add_less_cancel_left [of _ 0] by simp
   807 
   808 lemma less_add_same_cancel2 [simp]:
   809   "a < b + a \<longleftrightarrow> 0 < b"
   810   using add_less_cancel_right [of 0] by simp
   811 
   812 lemma add_le_same_cancel1 [simp]:
   813   "b + a \<le> b \<longleftrightarrow> a \<le> 0"
   814   using add_le_cancel_left [of _ _ 0] by simp
   815 
   816 lemma add_le_same_cancel2 [simp]:
   817   "a + b \<le> b \<longleftrightarrow> a \<le> 0"
   818   using add_le_cancel_right [of _ _ 0] by simp
   819 
   820 lemma le_add_same_cancel1 [simp]:
   821   "a \<le> a + b \<longleftrightarrow> 0 \<le> b"
   822   using add_le_cancel_left [of _ 0] by simp
   823 
   824 lemma le_add_same_cancel2 [simp]:
   825   "a \<le> b + a \<longleftrightarrow> 0 \<le> b"
   826   using add_le_cancel_right [of 0] by simp
   827 
   828 lemma max_diff_distrib_left:
   829   shows "max x y - z = max (x - z) (y - z)"
   830   using max_add_distrib_left [of x y "- z"] by simp
   831 
   832 lemma min_diff_distrib_left:
   833   shows "min x y - z = min (x - z) (y - z)"
   834   using min_add_distrib_left [of x y "- z"] by simp
   835 
   836 lemma le_imp_neg_le:
   837   assumes "a \<le> b" shows "-b \<le> -a"
   838 proof -
   839   have "-a+a \<le> -a+b" using \<open>a \<le> b\<close> by (rule add_left_mono)
   840   then have "0 \<le> -a+b" by simp
   841   then have "0 + (-b) \<le> (-a + b) + (-b)" by (rule add_right_mono)
   842   then show ?thesis by (simp add: algebra_simps)
   843 qed
   844 
   845 lemma neg_le_iff_le [simp]: "- b \<le> - a \<longleftrightarrow> a \<le> b"
   846 proof
   847   assume "- b \<le> - a"
   848   hence "- (- a) \<le> - (- b)" by (rule le_imp_neg_le)
   849   thus "a\<le>b" by simp
   850 next
   851   assume "a\<le>b"
   852   thus "-b \<le> -a" by (rule le_imp_neg_le)
   853 qed
   854 
   855 lemma neg_le_0_iff_le [simp]: "- a \<le> 0 \<longleftrightarrow> 0 \<le> a"
   856 by (subst neg_le_iff_le [symmetric], simp)
   857 
   858 lemma neg_0_le_iff_le [simp]: "0 \<le> - a \<longleftrightarrow> a \<le> 0"
   859 by (subst neg_le_iff_le [symmetric], simp)
   860 
   861 lemma neg_less_iff_less [simp]: "- b < - a \<longleftrightarrow> a < b"
   862 by (force simp add: less_le)
   863 
   864 lemma neg_less_0_iff_less [simp]: "- a < 0 \<longleftrightarrow> 0 < a"
   865 by (subst neg_less_iff_less [symmetric], simp)
   866 
   867 lemma neg_0_less_iff_less [simp]: "0 < - a \<longleftrightarrow> a < 0"
   868 by (subst neg_less_iff_less [symmetric], simp)
   869 
   870 text\<open>The next several equations can make the simplifier loop!\<close>
   871 
   872 lemma less_minus_iff: "a < - b \<longleftrightarrow> b < - a"
   873 proof -
   874   have "(- (-a) < - b) = (b < - a)" by (rule neg_less_iff_less)
   875   thus ?thesis by simp
   876 qed
   877 
   878 lemma minus_less_iff: "- a < b \<longleftrightarrow> - b < a"
   879 proof -
   880   have "(- a < - (-b)) = (- b < a)" by (rule neg_less_iff_less)
   881   thus ?thesis by simp
   882 qed
   883 
   884 lemma le_minus_iff: "a \<le> - b \<longleftrightarrow> b \<le> - a"
   885 proof -
   886   have mm: "!! a (b::'a). (-(-a)) < -b \<Longrightarrow> -(-b) < -a" by (simp only: minus_less_iff)
   887   have "(- (- a) <= -b) = (b <= - a)"
   888     apply (auto simp only: le_less)
   889     apply (drule mm)
   890     apply (simp_all)
   891     apply (drule mm[simplified], assumption)
   892     done
   893   then show ?thesis by simp
   894 qed
   895 
   896 lemma minus_le_iff: "- a \<le> b \<longleftrightarrow> - b \<le> a"
   897 by (auto simp add: le_less minus_less_iff)
   898 
   899 lemma diff_less_0_iff_less [simp]:
   900   "a - b < 0 \<longleftrightarrow> a < b"
   901 proof -
   902   have "a - b < 0 \<longleftrightarrow> a + (- b) < b + (- b)" by simp
   903   also have "... \<longleftrightarrow> a < b" by (simp only: add_less_cancel_right)
   904   finally show ?thesis .
   905 qed
   906 
   907 lemmas less_iff_diff_less_0 = diff_less_0_iff_less [symmetric]
   908 
   909 lemma diff_less_eq [algebra_simps, field_simps]:
   910   "a - b < c \<longleftrightarrow> a < c + b"
   911 apply (subst less_iff_diff_less_0 [of a])
   912 apply (rule less_iff_diff_less_0 [of _ c, THEN ssubst])
   913 apply (simp add: algebra_simps)
   914 done
   915 
   916 lemma less_diff_eq[algebra_simps, field_simps]:
   917   "a < c - b \<longleftrightarrow> a + b < c"
   918 apply (subst less_iff_diff_less_0 [of "a + b"])
   919 apply (subst less_iff_diff_less_0 [of a])
   920 apply (simp add: algebra_simps)
   921 done
   922 
   923 lemma diff_gt_0_iff_gt [simp]:
   924   "a - b > 0 \<longleftrightarrow> a > b"
   925   by (simp add: less_diff_eq)
   926 
   927 lemma diff_le_eq [algebra_simps, field_simps]:
   928   "a - b \<le> c \<longleftrightarrow> a \<le> c + b"
   929   by (auto simp add: le_less diff_less_eq )
   930 
   931 lemma le_diff_eq [algebra_simps, field_simps]:
   932   "a \<le> c - b \<longleftrightarrow> a + b \<le> c"
   933   by (auto simp add: le_less less_diff_eq)
   934 
   935 lemma diff_le_0_iff_le [simp]:
   936   "a - b \<le> 0 \<longleftrightarrow> a \<le> b"
   937   by (simp add: algebra_simps)
   938 
   939 lemmas le_iff_diff_le_0 = diff_le_0_iff_le [symmetric]
   940 
   941 lemma diff_ge_0_iff_ge [simp]:
   942   "a - b \<ge> 0 \<longleftrightarrow> a \<ge> b"
   943   by (simp add: le_diff_eq)
   944 
   945 lemma diff_eq_diff_less:
   946   "a - b = c - d \<Longrightarrow> a < b \<longleftrightarrow> c < d"
   947   by (auto simp only: less_iff_diff_less_0 [of a b] less_iff_diff_less_0 [of c d])
   948 
   949 lemma diff_eq_diff_less_eq:
   950   "a - b = c - d \<Longrightarrow> a \<le> b \<longleftrightarrow> c \<le> d"
   951   by (auto simp only: le_iff_diff_le_0 [of a b] le_iff_diff_le_0 [of c d])
   952 
   953 lemma diff_mono: "a \<le> b \<Longrightarrow> d \<le> c \<Longrightarrow> a - c \<le> b - d"
   954   by (simp add: field_simps add_mono)
   955 
   956 lemma diff_left_mono: "b \<le> a \<Longrightarrow> c - a \<le> c - b"
   957   by (simp add: field_simps)
   958 
   959 lemma diff_right_mono: "a \<le> b \<Longrightarrow> a - c \<le> b - c"
   960   by (simp add: field_simps)
   961 
   962 lemma diff_strict_mono: "a < b \<Longrightarrow> d < c \<Longrightarrow> a - c < b - d"
   963   by (simp add: field_simps add_strict_mono)
   964 
   965 lemma diff_strict_left_mono: "b < a \<Longrightarrow> c - a < c - b"
   966   by (simp add: field_simps)
   967 
   968 lemma diff_strict_right_mono: "a < b \<Longrightarrow> a - c < b - c"
   969   by (simp add: field_simps)
   970 
   971 end
   972 
   973 ML_file "Tools/group_cancel.ML"
   974 
   975 simproc_setup group_cancel_add ("a + b::'a::ab_group_add") =
   976   \<open>fn phi => fn ss => try Group_Cancel.cancel_add_conv\<close>
   977 
   978 simproc_setup group_cancel_diff ("a - b::'a::ab_group_add") =
   979   \<open>fn phi => fn ss => try Group_Cancel.cancel_diff_conv\<close>
   980 
   981 simproc_setup group_cancel_eq ("a = (b::'a::ab_group_add)") =
   982   \<open>fn phi => fn ss => try Group_Cancel.cancel_eq_conv\<close>
   983 
   984 simproc_setup group_cancel_le ("a \<le> (b::'a::ordered_ab_group_add)") =
   985   \<open>fn phi => fn ss => try Group_Cancel.cancel_le_conv\<close>
   986 
   987 simproc_setup group_cancel_less ("a < (b::'a::ordered_ab_group_add)") =
   988   \<open>fn phi => fn ss => try Group_Cancel.cancel_less_conv\<close>
   989 
   990 class linordered_ab_semigroup_add =
   991   linorder + ordered_ab_semigroup_add
   992 
   993 class linordered_cancel_ab_semigroup_add =
   994   linorder + ordered_cancel_ab_semigroup_add
   995 begin
   996 
   997 subclass linordered_ab_semigroup_add ..
   998 
   999 subclass ordered_ab_semigroup_add_imp_le
  1000 proof
  1001   fix a b c :: 'a
  1002   assume le: "c + a <= c + b"
  1003   show "a <= b"
  1004   proof (rule ccontr)
  1005     assume w: "~ a \<le> b"
  1006     hence "b <= a" by (simp add: linorder_not_le)
  1007     hence le2: "c + b <= c + a" by (rule add_left_mono)
  1008     have "a = b"
  1009       apply (insert le)
  1010       apply (insert le2)
  1011       apply (drule antisym, simp_all)
  1012       done
  1013     with w show False
  1014       by (simp add: linorder_not_le [symmetric])
  1015   qed
  1016 qed
  1017 
  1018 end
  1019 
  1020 class linordered_ab_group_add = linorder + ordered_ab_group_add
  1021 begin
  1022 
  1023 subclass linordered_cancel_ab_semigroup_add ..
  1024 
  1025 lemma equal_neg_zero [simp]:
  1026   "a = - a \<longleftrightarrow> a = 0"
  1027 proof
  1028   assume "a = 0" then show "a = - a" by simp
  1029 next
  1030   assume A: "a = - a" show "a = 0"
  1031   proof (cases "0 \<le> a")
  1032     case True with A have "0 \<le> - a" by auto
  1033     with le_minus_iff have "a \<le> 0" by simp
  1034     with True show ?thesis by (auto intro: order_trans)
  1035   next
  1036     case False then have B: "a \<le> 0" by auto
  1037     with A have "- a \<le> 0" by auto
  1038     with B show ?thesis by (auto intro: order_trans)
  1039   qed
  1040 qed
  1041 
  1042 lemma neg_equal_zero [simp]:
  1043   "- a = a \<longleftrightarrow> a = 0"
  1044   by (auto dest: sym)
  1045 
  1046 lemma neg_less_eq_nonneg [simp]:
  1047   "- a \<le> a \<longleftrightarrow> 0 \<le> a"
  1048 proof
  1049   assume A: "- a \<le> a" show "0 \<le> a"
  1050   proof (rule classical)
  1051     assume "\<not> 0 \<le> a"
  1052     then have "a < 0" by auto
  1053     with A have "- a < 0" by (rule le_less_trans)
  1054     then show ?thesis by auto
  1055   qed
  1056 next
  1057   assume A: "0 \<le> a" show "- a \<le> a"
  1058   proof (rule order_trans)
  1059     show "- a \<le> 0" using A by (simp add: minus_le_iff)
  1060   next
  1061     show "0 \<le> a" using A .
  1062   qed
  1063 qed
  1064 
  1065 lemma neg_less_pos [simp]:
  1066   "- a < a \<longleftrightarrow> 0 < a"
  1067   by (auto simp add: less_le)
  1068 
  1069 lemma less_eq_neg_nonpos [simp]:
  1070   "a \<le> - a \<longleftrightarrow> a \<le> 0"
  1071   using neg_less_eq_nonneg [of "- a"] by simp
  1072 
  1073 lemma less_neg_neg [simp]:
  1074   "a < - a \<longleftrightarrow> a < 0"
  1075   using neg_less_pos [of "- a"] by simp
  1076 
  1077 lemma double_zero [simp]:
  1078   "a + a = 0 \<longleftrightarrow> a = 0"
  1079 proof
  1080   assume assm: "a + a = 0"
  1081   then have a: "- a = a" by (rule minus_unique)
  1082   then show "a = 0" by (simp only: neg_equal_zero)
  1083 qed simp
  1084 
  1085 lemma double_zero_sym [simp]:
  1086   "0 = a + a \<longleftrightarrow> a = 0"
  1087   by (rule, drule sym) simp_all
  1088 
  1089 lemma zero_less_double_add_iff_zero_less_single_add [simp]:
  1090   "0 < a + a \<longleftrightarrow> 0 < a"
  1091 proof
  1092   assume "0 < a + a"
  1093   then have "0 - a < a" by (simp only: diff_less_eq)
  1094   then have "- a < a" by simp
  1095   then show "0 < a" by simp
  1096 next
  1097   assume "0 < a"
  1098   with this have "0 + 0 < a + a"
  1099     by (rule add_strict_mono)
  1100   then show "0 < a + a" by simp
  1101 qed
  1102 
  1103 lemma zero_le_double_add_iff_zero_le_single_add [simp]:
  1104   "0 \<le> a + a \<longleftrightarrow> 0 \<le> a"
  1105   by (auto simp add: le_less)
  1106 
  1107 lemma double_add_less_zero_iff_single_add_less_zero [simp]:
  1108   "a + a < 0 \<longleftrightarrow> a < 0"
  1109 proof -
  1110   have "\<not> a + a < 0 \<longleftrightarrow> \<not> a < 0"
  1111     by (simp add: not_less)
  1112   then show ?thesis by simp
  1113 qed
  1114 
  1115 lemma double_add_le_zero_iff_single_add_le_zero [simp]:
  1116   "a + a \<le> 0 \<longleftrightarrow> a \<le> 0"
  1117 proof -
  1118   have "\<not> a + a \<le> 0 \<longleftrightarrow> \<not> a \<le> 0"
  1119     by (simp add: not_le)
  1120   then show ?thesis by simp
  1121 qed
  1122 
  1123 lemma minus_max_eq_min:
  1124   "- max x y = min (-x) (-y)"
  1125   by (auto simp add: max_def min_def)
  1126 
  1127 lemma minus_min_eq_max:
  1128   "- min x y = max (-x) (-y)"
  1129   by (auto simp add: max_def min_def)
  1130 
  1131 end
  1132 
  1133 class abs =
  1134   fixes abs :: "'a \<Rightarrow> 'a"  ("\<bar>_\<bar>")
  1135 
  1136 class sgn =
  1137   fixes sgn :: "'a \<Rightarrow> 'a"
  1138 
  1139 class abs_if = minus + uminus + ord + zero + abs +
  1140   assumes abs_if: "\<bar>a\<bar> = (if a < 0 then - a else a)"
  1141 
  1142 class sgn_if = minus + uminus + zero + one + ord + sgn +
  1143   assumes sgn_if: "sgn x = (if x = 0 then 0 else if 0 < x then 1 else - 1)"
  1144 begin
  1145 
  1146 lemma sgn0 [simp]: "sgn 0 = 0"
  1147   by (simp add:sgn_if)
  1148 
  1149 end
  1150 
  1151 class ordered_ab_group_add_abs = ordered_ab_group_add + abs +
  1152   assumes abs_ge_zero [simp]: "\<bar>a\<bar> \<ge> 0"
  1153     and abs_ge_self: "a \<le> \<bar>a\<bar>"
  1154     and abs_leI: "a \<le> b \<Longrightarrow> - a \<le> b \<Longrightarrow> \<bar>a\<bar> \<le> b"
  1155     and abs_minus_cancel [simp]: "\<bar>-a\<bar> = \<bar>a\<bar>"
  1156     and abs_triangle_ineq: "\<bar>a + b\<bar> \<le> \<bar>a\<bar> + \<bar>b\<bar>"
  1157 begin
  1158 
  1159 lemma abs_minus_le_zero: "- \<bar>a\<bar> \<le> 0"
  1160   unfolding neg_le_0_iff_le by simp
  1161 
  1162 lemma abs_of_nonneg [simp]:
  1163   assumes nonneg: "0 \<le> a" shows "\<bar>a\<bar> = a"
  1164 proof (rule antisym)
  1165   from nonneg le_imp_neg_le have "- a \<le> 0" by simp
  1166   from this nonneg have "- a \<le> a" by (rule order_trans)
  1167   then show "\<bar>a\<bar> \<le> a" by (auto intro: abs_leI)
  1168 qed (rule abs_ge_self)
  1169 
  1170 lemma abs_idempotent [simp]: "\<bar>\<bar>a\<bar>\<bar> = \<bar>a\<bar>"
  1171 by (rule antisym)
  1172    (auto intro!: abs_ge_self abs_leI order_trans [of "- \<bar>a\<bar>" 0 "\<bar>a\<bar>"])
  1173 
  1174 lemma abs_eq_0 [simp]: "\<bar>a\<bar> = 0 \<longleftrightarrow> a = 0"
  1175 proof -
  1176   have "\<bar>a\<bar> = 0 \<Longrightarrow> a = 0"
  1177   proof (rule antisym)
  1178     assume zero: "\<bar>a\<bar> = 0"
  1179     with abs_ge_self show "a \<le> 0" by auto
  1180     from zero have "\<bar>-a\<bar> = 0" by simp
  1181     with abs_ge_self [of "- a"] have "- a \<le> 0" by auto
  1182     with neg_le_0_iff_le show "0 \<le> a" by auto
  1183   qed
  1184   then show ?thesis by auto
  1185 qed
  1186 
  1187 lemma abs_zero [simp]: "\<bar>0\<bar> = 0"
  1188 by simp
  1189 
  1190 lemma abs_0_eq [simp]: "0 = \<bar>a\<bar> \<longleftrightarrow> a = 0"
  1191 proof -
  1192   have "0 = \<bar>a\<bar> \<longleftrightarrow> \<bar>a\<bar> = 0" by (simp only: eq_ac)
  1193   thus ?thesis by simp
  1194 qed
  1195 
  1196 lemma abs_le_zero_iff [simp]: "\<bar>a\<bar> \<le> 0 \<longleftrightarrow> a = 0"
  1197 proof
  1198   assume "\<bar>a\<bar> \<le> 0"
  1199   then have "\<bar>a\<bar> = 0" by (rule antisym) simp
  1200   thus "a = 0" by simp
  1201 next
  1202   assume "a = 0"
  1203   thus "\<bar>a\<bar> \<le> 0" by simp
  1204 qed
  1205 
  1206 lemma abs_le_self_iff [simp]: "\<bar>a\<bar> \<le> a \<longleftrightarrow> 0 \<le> a"
  1207 proof -
  1208   have "\<forall>a. (0::'a) \<le> \<bar>a\<bar>"
  1209     using abs_ge_zero by blast
  1210   then have "\<bar>a\<bar> \<le> a \<Longrightarrow> 0 \<le> a"
  1211     using order.trans by blast
  1212   then show ?thesis
  1213     using abs_of_nonneg eq_refl by blast
  1214 qed
  1215 
  1216 lemma zero_less_abs_iff [simp]: "0 < \<bar>a\<bar> \<longleftrightarrow> a \<noteq> 0"
  1217 by (simp add: less_le)
  1218 
  1219 lemma abs_not_less_zero [simp]: "\<not> \<bar>a\<bar> < 0"
  1220 proof -
  1221   have a: "\<And>x y. x \<le> y \<Longrightarrow> \<not> y < x" by auto
  1222   show ?thesis by (simp add: a)
  1223 qed
  1224 
  1225 lemma abs_ge_minus_self: "- a \<le> \<bar>a\<bar>"
  1226 proof -
  1227   have "- a \<le> \<bar>-a\<bar>" by (rule abs_ge_self)
  1228   then show ?thesis by simp
  1229 qed
  1230 
  1231 lemma abs_minus_commute:
  1232   "\<bar>a - b\<bar> = \<bar>b - a\<bar>"
  1233 proof -
  1234   have "\<bar>a - b\<bar> = \<bar>- (a - b)\<bar>" by (simp only: abs_minus_cancel)
  1235   also have "... = \<bar>b - a\<bar>" by simp
  1236   finally show ?thesis .
  1237 qed
  1238 
  1239 lemma abs_of_pos: "0 < a \<Longrightarrow> \<bar>a\<bar> = a"
  1240 by (rule abs_of_nonneg, rule less_imp_le)
  1241 
  1242 lemma abs_of_nonpos [simp]:
  1243   assumes "a \<le> 0" shows "\<bar>a\<bar> = - a"
  1244 proof -
  1245   let ?b = "- a"
  1246   have "- ?b \<le> 0 \<Longrightarrow> \<bar>- ?b\<bar> = - (- ?b)"
  1247   unfolding abs_minus_cancel [of "?b"]
  1248   unfolding neg_le_0_iff_le [of "?b"]
  1249   unfolding minus_minus by (erule abs_of_nonneg)
  1250   then show ?thesis using assms by auto
  1251 qed
  1252 
  1253 lemma abs_of_neg: "a < 0 \<Longrightarrow> \<bar>a\<bar> = - a"
  1254 by (rule abs_of_nonpos, rule less_imp_le)
  1255 
  1256 lemma abs_le_D1: "\<bar>a\<bar> \<le> b \<Longrightarrow> a \<le> b"
  1257 by (insert abs_ge_self, blast intro: order_trans)
  1258 
  1259 lemma abs_le_D2: "\<bar>a\<bar> \<le> b \<Longrightarrow> - a \<le> b"
  1260 by (insert abs_le_D1 [of "- a"], simp)
  1261 
  1262 lemma abs_le_iff: "\<bar>a\<bar> \<le> b \<longleftrightarrow> a \<le> b \<and> - a \<le> b"
  1263 by (blast intro: abs_leI dest: abs_le_D1 abs_le_D2)
  1264 
  1265 lemma abs_triangle_ineq2: "\<bar>a\<bar> - \<bar>b\<bar> \<le> \<bar>a - b\<bar>"
  1266 proof -
  1267   have "\<bar>a\<bar> = \<bar>b + (a - b)\<bar>"
  1268     by (simp add: algebra_simps)
  1269   then have "\<bar>a\<bar> \<le> \<bar>b\<bar> + \<bar>a - b\<bar>"
  1270     by (simp add: abs_triangle_ineq)
  1271   then show ?thesis
  1272     by (simp add: algebra_simps)
  1273 qed
  1274 
  1275 lemma abs_triangle_ineq2_sym: "\<bar>a\<bar> - \<bar>b\<bar> \<le> \<bar>b - a\<bar>"
  1276   by (simp only: abs_minus_commute [of b] abs_triangle_ineq2)
  1277 
  1278 lemma abs_triangle_ineq3: "\<bar>\<bar>a\<bar> - \<bar>b\<bar>\<bar> \<le> \<bar>a - b\<bar>"
  1279   by (simp add: abs_le_iff abs_triangle_ineq2 abs_triangle_ineq2_sym)
  1280 
  1281 lemma abs_triangle_ineq4: "\<bar>a - b\<bar> \<le> \<bar>a\<bar> + \<bar>b\<bar>"
  1282 proof -
  1283   have "\<bar>a - b\<bar> = \<bar>a + - b\<bar>" by (simp add: algebra_simps)
  1284   also have "... \<le> \<bar>a\<bar> + \<bar>- b\<bar>" by (rule abs_triangle_ineq)
  1285   finally show ?thesis by simp
  1286 qed
  1287 
  1288 lemma abs_diff_triangle_ineq: "\<bar>a + b - (c + d)\<bar> \<le> \<bar>a - c\<bar> + \<bar>b - d\<bar>"
  1289 proof -
  1290   have "\<bar>a + b - (c+d)\<bar> = \<bar>(a-c) + (b-d)\<bar>" by (simp add: algebra_simps)
  1291   also have "... \<le> \<bar>a-c\<bar> + \<bar>b-d\<bar>" by (rule abs_triangle_ineq)
  1292   finally show ?thesis .
  1293 qed
  1294 
  1295 lemma abs_add_abs [simp]:
  1296   "\<bar>\<bar>a\<bar> + \<bar>b\<bar>\<bar> = \<bar>a\<bar> + \<bar>b\<bar>" (is "?L = ?R")
  1297 proof (rule antisym)
  1298   show "?L \<ge> ?R" by(rule abs_ge_self)
  1299 next
  1300   have "?L \<le> \<bar>\<bar>a\<bar>\<bar> + \<bar>\<bar>b\<bar>\<bar>" by(rule abs_triangle_ineq)
  1301   also have "\<dots> = ?R" by simp
  1302   finally show "?L \<le> ?R" .
  1303 qed
  1304 
  1305 end
  1306 
  1307 lemma dense_eq0_I:
  1308   fixes x::"'a::{dense_linorder,ordered_ab_group_add_abs}"
  1309   shows "(\<And>e. 0 < e \<Longrightarrow> \<bar>x\<bar> \<le> e) ==> x = 0"
  1310   apply (cases "\<bar>x\<bar> = 0", simp)
  1311   apply (simp only: zero_less_abs_iff [symmetric])
  1312   apply (drule dense)
  1313   apply (auto simp add: not_less [symmetric])
  1314   done
  1315 
  1316 hide_fact (open) ab_diff_conv_add_uminus add_0 mult_1 ab_left_minus
  1317 
  1318 lemmas add_0 = add_0_left \<comment> \<open>FIXME duplicate\<close>
  1319 lemmas mult_1 = mult_1_left \<comment> \<open>FIXME duplicate\<close>
  1320 lemmas ab_left_minus = left_minus \<comment> \<open>FIXME duplicate\<close>
  1321 lemmas diff_diff_eq = diff_diff_add \<comment> \<open>FIXME duplicate\<close>
  1322 
  1323 subsection \<open>Canonically ordered monoids\<close>
  1324 
  1325 text \<open>Canonically ordered monoids are never groups.\<close>
  1326 
  1327 class canonically_ordered_monoid_add = comm_monoid_add + order +
  1328   assumes le_iff_add: "a \<le> b \<longleftrightarrow> (\<exists>c. b = a + c)"
  1329 begin
  1330 
  1331 lemma zero_le[simp]: "0 \<le> x"
  1332   by (auto simp: le_iff_add)
  1333 
  1334 lemma le_zero_eq[simp]: "n \<le> 0 \<longleftrightarrow> n = 0"
  1335   by (auto intro: antisym)
  1336 
  1337 lemma not_less_zero[simp]: "\<not> n < 0"
  1338   by (auto simp: less_le)
  1339 
  1340 lemma zero_less_iff_neq_zero: "(0 < n) \<longleftrightarrow> (n \<noteq> 0)"
  1341   by (auto simp: less_le)
  1342 
  1343 text \<open>This theorem is useful with \<open>blast\<close>\<close>
  1344 lemma gr_zeroI: "(n = 0 \<Longrightarrow> False) \<Longrightarrow> 0 < n"
  1345   by (rule zero_less_iff_neq_zero[THEN iffD2]) iprover
  1346 
  1347 lemma not_gr_zero[simp]: "(\<not> (0 < n)) \<longleftrightarrow> (n = 0)"
  1348   by (simp add: zero_less_iff_neq_zero)
  1349 
  1350 subclass ordered_comm_monoid_add
  1351   proof qed (auto simp: le_iff_add add_ac)
  1352 
  1353 lemma add_eq_0_iff_both_eq_0: "x + y = 0 \<longleftrightarrow> x = 0 \<and> y = 0"
  1354   by (intro add_nonneg_eq_0_iff zero_le)
  1355 
  1356 lemma gr_implies_not_zero: "m < n \<Longrightarrow> n \<noteq> 0"
  1357   using add_eq_0_iff_both_eq_0[of m] by (auto simp: le_iff_add less_le)
  1358 
  1359 lemmas zero_order = zero_le le_zero_eq not_less_zero zero_less_iff_neq_zero not_gr_zero
  1360   -- \<open>This should be attributed with \<open>[iff]\<close>, but then \<open>blast\<close> fails in \<open>Set\<close>.\<close>
  1361 
  1362 end
  1363 
  1364 class ordered_cancel_comm_monoid_diff =
  1365   canonically_ordered_monoid_add + comm_monoid_diff + ordered_ab_semigroup_add_imp_le
  1366 begin
  1367 
  1368 context
  1369   fixes a b
  1370   assumes "a \<le> b"
  1371 begin
  1372 
  1373 lemma add_diff_inverse:
  1374   "a + (b - a) = b"
  1375   using \<open>a \<le> b\<close> by (auto simp add: le_iff_add)
  1376 
  1377 lemma add_diff_assoc:
  1378   "c + (b - a) = c + b - a"
  1379   using \<open>a \<le> b\<close> by (auto simp add: le_iff_add add.left_commute [of c])
  1380 
  1381 lemma add_diff_assoc2:
  1382   "b - a + c = b + c - a"
  1383   using \<open>a \<le> b\<close> by (auto simp add: le_iff_add add.assoc)
  1384 
  1385 lemma diff_add_assoc:
  1386   "c + b - a = c + (b - a)"
  1387   using \<open>a \<le> b\<close> by (simp add: add.commute add_diff_assoc)
  1388 
  1389 lemma diff_add_assoc2:
  1390   "b + c - a = b - a + c"
  1391   using \<open>a \<le> b\<close>by (simp add: add.commute add_diff_assoc)
  1392 
  1393 lemma diff_diff_right:
  1394   "c - (b - a) = c + a - b"
  1395   by (simp add: add_diff_inverse add_diff_cancel_left [of a c "b - a", symmetric] add.commute)
  1396 
  1397 lemma diff_add:
  1398   "b - a + a = b"
  1399   by (simp add: add.commute add_diff_inverse)
  1400 
  1401 lemma le_add_diff:
  1402   "c \<le> b + c - a"
  1403   by (auto simp add: add.commute diff_add_assoc2 le_iff_add)
  1404 
  1405 lemma le_imp_diff_is_add:
  1406   "a \<le> b \<Longrightarrow> b - a = c \<longleftrightarrow> b = c + a"
  1407   by (auto simp add: add.commute add_diff_inverse)
  1408 
  1409 lemma le_diff_conv2:
  1410   "c \<le> b - a \<longleftrightarrow> c + a \<le> b" (is "?P \<longleftrightarrow> ?Q")
  1411 proof
  1412   assume ?P
  1413   then have "c + a \<le> b - a + a" by (rule add_right_mono)
  1414   then show ?Q by (simp add: add_diff_inverse add.commute)
  1415 next
  1416   assume ?Q
  1417   then have "a + c \<le> a + (b - a)" by (simp add: add_diff_inverse add.commute)
  1418   then show ?P by simp
  1419 qed
  1420 
  1421 end
  1422 
  1423 end
  1424 
  1425 subsection \<open>Tools setup\<close>
  1426 
  1427 lemma add_mono_thms_linordered_semiring:
  1428   fixes i j k :: "'a::ordered_ab_semigroup_add"
  1429   shows "i \<le> j \<and> k \<le> l \<Longrightarrow> i + k \<le> j + l"
  1430     and "i = j \<and> k \<le> l \<Longrightarrow> i + k \<le> j + l"
  1431     and "i \<le> j \<and> k = l \<Longrightarrow> i + k \<le> j + l"
  1432     and "i = j \<and> k = l \<Longrightarrow> i + k = j + l"
  1433 by (rule add_mono, clarify+)+
  1434 
  1435 lemma add_mono_thms_linordered_field:
  1436   fixes i j k :: "'a::ordered_cancel_ab_semigroup_add"
  1437   shows "i < j \<and> k = l \<Longrightarrow> i + k < j + l"
  1438     and "i = j \<and> k < l \<Longrightarrow> i + k < j + l"
  1439     and "i < j \<and> k \<le> l \<Longrightarrow> i + k < j + l"
  1440     and "i \<le> j \<and> k < l \<Longrightarrow> i + k < j + l"
  1441     and "i < j \<and> k < l \<Longrightarrow> i + k < j + l"
  1442 by (auto intro: add_strict_right_mono add_strict_left_mono
  1443   add_less_le_mono add_le_less_mono add_strict_mono)
  1444 
  1445 code_identifier
  1446   code_module Groups \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith
  1447 
  1448 end