src/HOL/Groups.thy
author wenzelm
Fri Oct 28 23:41:16 2011 +0200 (2011-10-28)
changeset 45294 3c5d3d286055
parent 44848 f4d0b060c7ca
child 45548 3e2722d66169
permissions -rw-r--r--
tuned Named_Thms: proper binding;
     1 (*  Title:   HOL/Groups.thy
     2     Author:  Gertrud Bauer, Steven Obua, Lawrence C Paulson, Markus Wenzel, Jeremy Avigad
     3 *)
     4 
     5 header {* Groups, also combined with orderings *}
     6 
     7 theory Groups
     8 imports Orderings
     9 uses ("Tools/abel_cancel.ML")
    10 begin
    11 
    12 subsection {* Fact collections *}
    13 
    14 ML {*
    15 structure Ac_Simps = Named_Thms
    16 (
    17   val name = @{binding ac_simps}
    18   val description = "associativity and commutativity simplification rules"
    19 )
    20 *}
    21 
    22 setup Ac_Simps.setup
    23 
    24 text{* The rewrites accumulated in @{text algebra_simps} deal with the
    25 classical algebraic structures of groups, rings and family. They simplify
    26 terms by multiplying everything out (in case of a ring) and bringing sums and
    27 products into a canonical form (by ordered rewriting). As a result it decides
    28 group and ring equalities but also helps with inequalities.
    29 
    30 Of course it also works for fields, but it knows nothing about multiplicative
    31 inverses or division. This is catered for by @{text field_simps}. *}
    32 
    33 ML {*
    34 structure Algebra_Simps = Named_Thms
    35 (
    36   val name = @{binding algebra_simps}
    37   val description = "algebra simplification rules"
    38 )
    39 *}
    40 
    41 setup Algebra_Simps.setup
    42 
    43 text{* Lemmas @{text field_simps} multiply with denominators in (in)equations
    44 if they can be proved to be non-zero (for equations) or positive/negative
    45 (for inequations). Can be too aggressive and is therefore separate from the
    46 more benign @{text algebra_simps}. *}
    47 
    48 ML {*
    49 structure Field_Simps = Named_Thms
    50 (
    51   val name = @{binding field_simps}
    52   val description = "algebra simplification rules for fields"
    53 )
    54 *}
    55 
    56 setup Field_Simps.setup
    57 
    58 
    59 subsection {* Abstract structures *}
    60 
    61 text {*
    62   These locales provide basic structures for interpretation into
    63   bigger structures;  extensions require careful thinking, otherwise
    64   undesired effects may occur due to interpretation.
    65 *}
    66 
    67 locale semigroup =
    68   fixes f :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "*" 70)
    69   assumes assoc [ac_simps]: "a * b * c = a * (b * c)"
    70 
    71 locale abel_semigroup = semigroup +
    72   assumes commute [ac_simps]: "a * b = b * a"
    73 begin
    74 
    75 lemma left_commute [ac_simps]:
    76   "b * (a * c) = a * (b * c)"
    77 proof -
    78   have "(b * a) * c = (a * b) * c"
    79     by (simp only: commute)
    80   then show ?thesis
    81     by (simp only: assoc)
    82 qed
    83 
    84 end
    85 
    86 locale monoid = semigroup +
    87   fixes z :: 'a ("1")
    88   assumes left_neutral [simp]: "1 * a = a"
    89   assumes right_neutral [simp]: "a * 1 = a"
    90 
    91 locale comm_monoid = abel_semigroup +
    92   fixes z :: 'a ("1")
    93   assumes comm_neutral: "a * 1 = a"
    94 
    95 sublocale comm_monoid < monoid proof
    96 qed (simp_all add: commute comm_neutral)
    97 
    98 
    99 subsection {* Generic operations *}
   100 
   101 class zero = 
   102   fixes zero :: 'a  ("0")
   103 
   104 class one =
   105   fixes one  :: 'a  ("1")
   106 
   107 hide_const (open) zero one
   108 
   109 lemma Let_0 [simp]: "Let 0 f = f 0"
   110   unfolding Let_def ..
   111 
   112 lemma Let_1 [simp]: "Let 1 f = f 1"
   113   unfolding Let_def ..
   114 
   115 setup {*
   116   Reorient_Proc.add
   117     (fn Const(@{const_name Groups.zero}, _) => true
   118       | Const(@{const_name Groups.one}, _) => true
   119       | _ => false)
   120 *}
   121 
   122 simproc_setup reorient_zero ("0 = x") = Reorient_Proc.proc
   123 simproc_setup reorient_one ("1 = x") = Reorient_Proc.proc
   124 
   125 typed_print_translation (advanced) {*
   126   let
   127     fun tr' c = (c, fn ctxt => fn T => fn ts =>
   128       if not (null ts) orelse T = dummyT
   129         orelse not (Config.get ctxt show_types) andalso can Term.dest_Type T
   130       then raise Match
   131       else
   132         Syntax.const @{syntax_const "_constrain"} $ Syntax.const c $
   133           Syntax_Phases.term_of_typ ctxt T);
   134   in map tr' [@{const_syntax Groups.one}, @{const_syntax Groups.zero}] end;
   135 *} -- {* show types that are presumably too general *}
   136 
   137 class plus =
   138   fixes plus :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "+" 65)
   139 
   140 class minus =
   141   fixes minus :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "-" 65)
   142 
   143 class uminus =
   144   fixes uminus :: "'a \<Rightarrow> 'a"  ("- _" [81] 80)
   145 
   146 class times =
   147   fixes times :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "*" 70)
   148 
   149 
   150 subsection {* Semigroups and Monoids *}
   151 
   152 class semigroup_add = plus +
   153   assumes add_assoc [algebra_simps, field_simps]: "(a + b) + c = a + (b + c)"
   154 
   155 sublocale semigroup_add < add!: semigroup plus proof
   156 qed (fact add_assoc)
   157 
   158 class ab_semigroup_add = semigroup_add +
   159   assumes add_commute [algebra_simps, field_simps]: "a + b = b + a"
   160 
   161 sublocale ab_semigroup_add < add!: abel_semigroup plus proof
   162 qed (fact add_commute)
   163 
   164 context ab_semigroup_add
   165 begin
   166 
   167 lemmas add_left_commute [algebra_simps, field_simps] = add.left_commute
   168 
   169 theorems add_ac = add_assoc add_commute add_left_commute
   170 
   171 end
   172 
   173 theorems add_ac = add_assoc add_commute add_left_commute
   174 
   175 class semigroup_mult = times +
   176   assumes mult_assoc [algebra_simps, field_simps]: "(a * b) * c = a * (b * c)"
   177 
   178 sublocale semigroup_mult < mult!: semigroup times proof
   179 qed (fact mult_assoc)
   180 
   181 class ab_semigroup_mult = semigroup_mult +
   182   assumes mult_commute [algebra_simps, field_simps]: "a * b = b * a"
   183 
   184 sublocale ab_semigroup_mult < mult!: abel_semigroup times proof
   185 qed (fact mult_commute)
   186 
   187 context ab_semigroup_mult
   188 begin
   189 
   190 lemmas mult_left_commute [algebra_simps, field_simps] = mult.left_commute
   191 
   192 theorems mult_ac = mult_assoc mult_commute mult_left_commute
   193 
   194 end
   195 
   196 theorems mult_ac = mult_assoc mult_commute mult_left_commute
   197 
   198 class monoid_add = zero + semigroup_add +
   199   assumes add_0_left: "0 + a = a"
   200     and add_0_right: "a + 0 = a"
   201 
   202 sublocale monoid_add < add!: monoid plus 0 proof
   203 qed (fact add_0_left add_0_right)+
   204 
   205 lemma zero_reorient: "0 = x \<longleftrightarrow> x = 0"
   206 by (rule eq_commute)
   207 
   208 class comm_monoid_add = zero + ab_semigroup_add +
   209   assumes add_0: "0 + a = a"
   210 
   211 sublocale comm_monoid_add < add!: comm_monoid plus 0 proof
   212 qed (insert add_0, simp add: ac_simps)
   213 
   214 subclass (in comm_monoid_add) monoid_add proof
   215 qed (fact add.left_neutral add.right_neutral)+
   216 
   217 class monoid_mult = one + semigroup_mult +
   218   assumes mult_1_left: "1 * a  = a"
   219     and mult_1_right: "a * 1 = a"
   220 
   221 sublocale monoid_mult < mult!: monoid times 1 proof
   222 qed (fact mult_1_left mult_1_right)+
   223 
   224 lemma one_reorient: "1 = x \<longleftrightarrow> x = 1"
   225 by (rule eq_commute)
   226 
   227 class comm_monoid_mult = one + ab_semigroup_mult +
   228   assumes mult_1: "1 * a = a"
   229 
   230 sublocale comm_monoid_mult < mult!: comm_monoid times 1 proof
   231 qed (insert mult_1, simp add: ac_simps)
   232 
   233 subclass (in comm_monoid_mult) monoid_mult proof
   234 qed (fact mult.left_neutral mult.right_neutral)+
   235 
   236 class cancel_semigroup_add = semigroup_add +
   237   assumes add_left_imp_eq: "a + b = a + c \<Longrightarrow> b = c"
   238   assumes add_right_imp_eq: "b + a = c + a \<Longrightarrow> b = c"
   239 begin
   240 
   241 lemma add_left_cancel [simp]:
   242   "a + b = a + c \<longleftrightarrow> b = c"
   243 by (blast dest: add_left_imp_eq)
   244 
   245 lemma add_right_cancel [simp]:
   246   "b + a = c + a \<longleftrightarrow> b = c"
   247 by (blast dest: add_right_imp_eq)
   248 
   249 end
   250 
   251 class cancel_ab_semigroup_add = ab_semigroup_add +
   252   assumes add_imp_eq: "a + b = a + c \<Longrightarrow> b = c"
   253 begin
   254 
   255 subclass cancel_semigroup_add
   256 proof
   257   fix a b c :: 'a
   258   assume "a + b = a + c" 
   259   then show "b = c" by (rule add_imp_eq)
   260 next
   261   fix a b c :: 'a
   262   assume "b + a = c + a"
   263   then have "a + b = a + c" by (simp only: add_commute)
   264   then show "b = c" by (rule add_imp_eq)
   265 qed
   266 
   267 end
   268 
   269 class cancel_comm_monoid_add = cancel_ab_semigroup_add + comm_monoid_add
   270 
   271 
   272 subsection {* Groups *}
   273 
   274 class group_add = minus + uminus + monoid_add +
   275   assumes left_minus [simp]: "- a + a = 0"
   276   assumes diff_minus: "a - b = a + (- b)"
   277 begin
   278 
   279 lemma minus_unique:
   280   assumes "a + b = 0" shows "- a = b"
   281 proof -
   282   have "- a = - a + (a + b)" using assms by simp
   283   also have "\<dots> = b" by (simp add: add_assoc [symmetric])
   284   finally show ?thesis .
   285 qed
   286 
   287 
   288 lemmas equals_zero_I = minus_unique (* legacy name *)
   289 
   290 lemma minus_zero [simp]: "- 0 = 0"
   291 proof -
   292   have "0 + 0 = 0" by (rule add_0_right)
   293   thus "- 0 = 0" by (rule minus_unique)
   294 qed
   295 
   296 lemma minus_minus [simp]: "- (- a) = a"
   297 proof -
   298   have "- a + a = 0" by (rule left_minus)
   299   thus "- (- a) = a" by (rule minus_unique)
   300 qed
   301 
   302 lemma right_minus [simp]: "a + - a = 0"
   303 proof -
   304   have "a + - a = - (- a) + - a" by simp
   305   also have "\<dots> = 0" by (rule left_minus)
   306   finally show ?thesis .
   307 qed
   308 
   309 subclass cancel_semigroup_add
   310 proof
   311   fix a b c :: 'a
   312   assume "a + b = a + c"
   313   then have "- a + a + b = - a + a + c"
   314     unfolding add_assoc by simp
   315   then show "b = c" by simp
   316 next
   317   fix a b c :: 'a
   318   assume "b + a = c + a"
   319   then have "b + a + - a = c + a  + - a" by simp
   320   then show "b = c" unfolding add_assoc by simp
   321 qed
   322 
   323 lemma minus_add_cancel: "- a + (a + b) = b"
   324 by (simp add: add_assoc [symmetric])
   325 
   326 lemma add_minus_cancel: "a + (- a + b) = b"
   327 by (simp add: add_assoc [symmetric])
   328 
   329 lemma minus_add: "- (a + b) = - b + - a"
   330 proof -
   331   have "(a + b) + (- b + - a) = 0"
   332     by (simp add: add_assoc add_minus_cancel)
   333   thus "- (a + b) = - b + - a"
   334     by (rule minus_unique)
   335 qed
   336 
   337 lemma right_minus_eq: "a - b = 0 \<longleftrightarrow> a = b"
   338 proof
   339   assume "a - b = 0"
   340   have "a = (a - b) + b" by (simp add:diff_minus add_assoc)
   341   also have "\<dots> = b" using `a - b = 0` by simp
   342   finally show "a = b" .
   343 next
   344   assume "a = b" thus "a - b = 0" by (simp add: diff_minus)
   345 qed
   346 
   347 lemma diff_self [simp]: "a - a = 0"
   348 by (simp add: diff_minus)
   349 
   350 lemma diff_0 [simp]: "0 - a = - a"
   351 by (simp add: diff_minus)
   352 
   353 lemma diff_0_right [simp]: "a - 0 = a" 
   354 by (simp add: diff_minus)
   355 
   356 lemma diff_minus_eq_add [simp]: "a - - b = a + b"
   357 by (simp add: diff_minus)
   358 
   359 lemma neg_equal_iff_equal [simp]:
   360   "- a = - b \<longleftrightarrow> a = b" 
   361 proof 
   362   assume "- a = - b"
   363   hence "- (- a) = - (- b)" by simp
   364   thus "a = b" by simp
   365 next
   366   assume "a = b"
   367   thus "- a = - b" by simp
   368 qed
   369 
   370 lemma neg_equal_0_iff_equal [simp]:
   371   "- a = 0 \<longleftrightarrow> a = 0"
   372 by (subst neg_equal_iff_equal [symmetric], simp)
   373 
   374 lemma neg_0_equal_iff_equal [simp]:
   375   "0 = - a \<longleftrightarrow> 0 = a"
   376 by (subst neg_equal_iff_equal [symmetric], simp)
   377 
   378 text{*The next two equations can make the simplifier loop!*}
   379 
   380 lemma equation_minus_iff:
   381   "a = - b \<longleftrightarrow> b = - a"
   382 proof -
   383   have "- (- a) = - b \<longleftrightarrow> - a = b" by (rule neg_equal_iff_equal)
   384   thus ?thesis by (simp add: eq_commute)
   385 qed
   386 
   387 lemma minus_equation_iff:
   388   "- a = b \<longleftrightarrow> - b = a"
   389 proof -
   390   have "- a = - (- b) \<longleftrightarrow> a = -b" by (rule neg_equal_iff_equal)
   391   thus ?thesis by (simp add: eq_commute)
   392 qed
   393 
   394 lemma diff_add_cancel: "a - b + b = a"
   395 by (simp add: diff_minus add_assoc)
   396 
   397 lemma add_diff_cancel: "a + b - b = a"
   398 by (simp add: diff_minus add_assoc)
   399 
   400 declare diff_minus[symmetric, algebra_simps, field_simps]
   401 
   402 lemma eq_neg_iff_add_eq_0: "a = - b \<longleftrightarrow> a + b = 0"
   403 proof
   404   assume "a = - b" then show "a + b = 0" by simp
   405 next
   406   assume "a + b = 0"
   407   moreover have "a + (b + - b) = (a + b) + - b"
   408     by (simp only: add_assoc)
   409   ultimately show "a = - b" by simp
   410 qed
   411 
   412 lemma add_eq_0_iff: "x + y = 0 \<longleftrightarrow> y = - x"
   413   unfolding eq_neg_iff_add_eq_0 [symmetric]
   414   by (rule equation_minus_iff)
   415 
   416 end
   417 
   418 class ab_group_add = minus + uminus + comm_monoid_add +
   419   assumes ab_left_minus: "- a + a = 0"
   420   assumes ab_diff_minus: "a - b = a + (- b)"
   421 begin
   422 
   423 subclass group_add
   424   proof qed (simp_all add: ab_left_minus ab_diff_minus)
   425 
   426 subclass cancel_comm_monoid_add
   427 proof
   428   fix a b c :: 'a
   429   assume "a + b = a + c"
   430   then have "- a + a + b = - a + a + c"
   431     unfolding add_assoc by simp
   432   then show "b = c" by simp
   433 qed
   434 
   435 lemma uminus_add_conv_diff[algebra_simps, field_simps]:
   436   "- a + b = b - a"
   437 by (simp add:diff_minus add_commute)
   438 
   439 lemma minus_add_distrib [simp]:
   440   "- (a + b) = - a + - b"
   441 by (rule minus_unique) (simp add: add_ac)
   442 
   443 lemma minus_diff_eq [simp]:
   444   "- (a - b) = b - a"
   445 by (simp add: diff_minus add_commute)
   446 
   447 lemma add_diff_eq[algebra_simps, field_simps]: "a + (b - c) = (a + b) - c"
   448 by (simp add: diff_minus add_ac)
   449 
   450 lemma diff_add_eq[algebra_simps, field_simps]: "(a - b) + c = (a + c) - b"
   451 by (simp add: diff_minus add_ac)
   452 
   453 lemma diff_eq_eq[algebra_simps, field_simps]: "a - b = c \<longleftrightarrow> a = c + b"
   454 by (auto simp add: diff_minus add_assoc)
   455 
   456 lemma eq_diff_eq[algebra_simps, field_simps]: "a = c - b \<longleftrightarrow> a + b = c"
   457 by (auto simp add: diff_minus add_assoc)
   458 
   459 lemma diff_diff_eq[algebra_simps, field_simps]: "(a - b) - c = a - (b + c)"
   460 by (simp add: diff_minus add_ac)
   461 
   462 lemma diff_diff_eq2[algebra_simps, field_simps]: "a - (b - c) = (a + c) - b"
   463 by (simp add: diff_minus add_ac)
   464 
   465 lemma eq_iff_diff_eq_0: "a = b \<longleftrightarrow> a - b = 0"
   466 by (simp add: algebra_simps)
   467 
   468 (* FIXME: duplicates right_minus_eq from class group_add *)
   469 (* but only this one is declared as a simp rule. *)
   470 lemma diff_eq_0_iff_eq [simp, no_atp]: "a - b = 0 \<longleftrightarrow> a = b"
   471   by (rule right_minus_eq)
   472 
   473 lemma diff_eq_diff_eq:
   474   "a - b = c - d \<Longrightarrow> a = b \<longleftrightarrow> c = d"
   475   by (auto simp add: algebra_simps)
   476   
   477 end
   478 
   479 
   480 subsection {* (Partially) Ordered Groups *} 
   481 
   482 text {*
   483   The theory of partially ordered groups is taken from the books:
   484   \begin{itemize}
   485   \item \emph{Lattice Theory} by Garret Birkhoff, American Mathematical Society 1979 
   486   \item \emph{Partially Ordered Algebraic Systems}, Pergamon Press 1963
   487   \end{itemize}
   488   Most of the used notions can also be looked up in 
   489   \begin{itemize}
   490   \item \url{http://www.mathworld.com} by Eric Weisstein et. al.
   491   \item \emph{Algebra I} by van der Waerden, Springer.
   492   \end{itemize}
   493 *}
   494 
   495 class ordered_ab_semigroup_add = order + ab_semigroup_add +
   496   assumes add_left_mono: "a \<le> b \<Longrightarrow> c + a \<le> c + b"
   497 begin
   498 
   499 lemma add_right_mono:
   500   "a \<le> b \<Longrightarrow> a + c \<le> b + c"
   501 by (simp add: add_commute [of _ c] add_left_mono)
   502 
   503 text {* non-strict, in both arguments *}
   504 lemma add_mono:
   505   "a \<le> b \<Longrightarrow> c \<le> d \<Longrightarrow> a + c \<le> b + d"
   506   apply (erule add_right_mono [THEN order_trans])
   507   apply (simp add: add_commute add_left_mono)
   508   done
   509 
   510 end
   511 
   512 class ordered_cancel_ab_semigroup_add =
   513   ordered_ab_semigroup_add + cancel_ab_semigroup_add
   514 begin
   515 
   516 lemma add_strict_left_mono:
   517   "a < b \<Longrightarrow> c + a < c + b"
   518 by (auto simp add: less_le add_left_mono)
   519 
   520 lemma add_strict_right_mono:
   521   "a < b \<Longrightarrow> a + c < b + c"
   522 by (simp add: add_commute [of _ c] add_strict_left_mono)
   523 
   524 text{*Strict monotonicity in both arguments*}
   525 lemma add_strict_mono:
   526   "a < b \<Longrightarrow> c < d \<Longrightarrow> a + c < b + d"
   527 apply (erule add_strict_right_mono [THEN less_trans])
   528 apply (erule add_strict_left_mono)
   529 done
   530 
   531 lemma add_less_le_mono:
   532   "a < b \<Longrightarrow> c \<le> d \<Longrightarrow> a + c < b + d"
   533 apply (erule add_strict_right_mono [THEN less_le_trans])
   534 apply (erule add_left_mono)
   535 done
   536 
   537 lemma add_le_less_mono:
   538   "a \<le> b \<Longrightarrow> c < d \<Longrightarrow> a + c < b + d"
   539 apply (erule add_right_mono [THEN le_less_trans])
   540 apply (erule add_strict_left_mono) 
   541 done
   542 
   543 end
   544 
   545 class ordered_ab_semigroup_add_imp_le =
   546   ordered_cancel_ab_semigroup_add +
   547   assumes add_le_imp_le_left: "c + a \<le> c + b \<Longrightarrow> a \<le> b"
   548 begin
   549 
   550 lemma add_less_imp_less_left:
   551   assumes less: "c + a < c + b" shows "a < b"
   552 proof -
   553   from less have le: "c + a <= c + b" by (simp add: order_le_less)
   554   have "a <= b" 
   555     apply (insert le)
   556     apply (drule add_le_imp_le_left)
   557     by (insert le, drule add_le_imp_le_left, assumption)
   558   moreover have "a \<noteq> b"
   559   proof (rule ccontr)
   560     assume "~(a \<noteq> b)"
   561     then have "a = b" by simp
   562     then have "c + a = c + b" by simp
   563     with less show "False"by simp
   564   qed
   565   ultimately show "a < b" by (simp add: order_le_less)
   566 qed
   567 
   568 lemma add_less_imp_less_right:
   569   "a + c < b + c \<Longrightarrow> a < b"
   570 apply (rule add_less_imp_less_left [of c])
   571 apply (simp add: add_commute)  
   572 done
   573 
   574 lemma add_less_cancel_left [simp]:
   575   "c + a < c + b \<longleftrightarrow> a < b"
   576 by (blast intro: add_less_imp_less_left add_strict_left_mono) 
   577 
   578 lemma add_less_cancel_right [simp]:
   579   "a + c < b + c \<longleftrightarrow> a < b"
   580 by (blast intro: add_less_imp_less_right add_strict_right_mono)
   581 
   582 lemma add_le_cancel_left [simp]:
   583   "c + a \<le> c + b \<longleftrightarrow> a \<le> b"
   584 by (auto, drule add_le_imp_le_left, simp_all add: add_left_mono) 
   585 
   586 lemma add_le_cancel_right [simp]:
   587   "a + c \<le> b + c \<longleftrightarrow> a \<le> b"
   588 by (simp add: add_commute [of a c] add_commute [of b c])
   589 
   590 lemma add_le_imp_le_right:
   591   "a + c \<le> b + c \<Longrightarrow> a \<le> b"
   592 by simp
   593 
   594 lemma max_add_distrib_left:
   595   "max x y + z = max (x + z) (y + z)"
   596   unfolding max_def by auto
   597 
   598 lemma min_add_distrib_left:
   599   "min x y + z = min (x + z) (y + z)"
   600   unfolding min_def by auto
   601 
   602 lemma max_add_distrib_right:
   603   "x + max y z = max (x + y) (x + z)"
   604   unfolding max_def by auto
   605 
   606 lemma min_add_distrib_right:
   607   "x + min y z = min (x + y) (x + z)"
   608   unfolding min_def by auto
   609 
   610 end
   611 
   612 subsection {* Support for reasoning about signs *}
   613 
   614 class ordered_comm_monoid_add =
   615   ordered_cancel_ab_semigroup_add + comm_monoid_add
   616 begin
   617 
   618 lemma add_pos_nonneg:
   619   assumes "0 < a" and "0 \<le> b" shows "0 < a + b"
   620 proof -
   621   have "0 + 0 < a + b" 
   622     using assms by (rule add_less_le_mono)
   623   then show ?thesis by simp
   624 qed
   625 
   626 lemma add_pos_pos:
   627   assumes "0 < a" and "0 < b" shows "0 < a + b"
   628 by (rule add_pos_nonneg) (insert assms, auto)
   629 
   630 lemma add_nonneg_pos:
   631   assumes "0 \<le> a" and "0 < b" shows "0 < a + b"
   632 proof -
   633   have "0 + 0 < a + b" 
   634     using assms by (rule add_le_less_mono)
   635   then show ?thesis by simp
   636 qed
   637 
   638 lemma add_nonneg_nonneg [simp]:
   639   assumes "0 \<le> a" and "0 \<le> b" shows "0 \<le> a + b"
   640 proof -
   641   have "0 + 0 \<le> a + b" 
   642     using assms by (rule add_mono)
   643   then show ?thesis by simp
   644 qed
   645 
   646 lemma add_neg_nonpos:
   647   assumes "a < 0" and "b \<le> 0" shows "a + b < 0"
   648 proof -
   649   have "a + b < 0 + 0"
   650     using assms by (rule add_less_le_mono)
   651   then show ?thesis by simp
   652 qed
   653 
   654 lemma add_neg_neg: 
   655   assumes "a < 0" and "b < 0" shows "a + b < 0"
   656 by (rule add_neg_nonpos) (insert assms, auto)
   657 
   658 lemma add_nonpos_neg:
   659   assumes "a \<le> 0" and "b < 0" shows "a + b < 0"
   660 proof -
   661   have "a + b < 0 + 0"
   662     using assms by (rule add_le_less_mono)
   663   then show ?thesis by simp
   664 qed
   665 
   666 lemma add_nonpos_nonpos:
   667   assumes "a \<le> 0" and "b \<le> 0" shows "a + b \<le> 0"
   668 proof -
   669   have "a + b \<le> 0 + 0"
   670     using assms by (rule add_mono)
   671   then show ?thesis by simp
   672 qed
   673 
   674 lemmas add_sign_intros =
   675   add_pos_nonneg add_pos_pos add_nonneg_pos add_nonneg_nonneg
   676   add_neg_nonpos add_neg_neg add_nonpos_neg add_nonpos_nonpos
   677 
   678 lemma add_nonneg_eq_0_iff:
   679   assumes x: "0 \<le> x" and y: "0 \<le> y"
   680   shows "x + y = 0 \<longleftrightarrow> x = 0 \<and> y = 0"
   681 proof (intro iffI conjI)
   682   have "x = x + 0" by simp
   683   also have "x + 0 \<le> x + y" using y by (rule add_left_mono)
   684   also assume "x + y = 0"
   685   also have "0 \<le> x" using x .
   686   finally show "x = 0" .
   687 next
   688   have "y = 0 + y" by simp
   689   also have "0 + y \<le> x + y" using x by (rule add_right_mono)
   690   also assume "x + y = 0"
   691   also have "0 \<le> y" using y .
   692   finally show "y = 0" .
   693 next
   694   assume "x = 0 \<and> y = 0"
   695   then show "x + y = 0" by simp
   696 qed
   697 
   698 end
   699 
   700 class ordered_ab_group_add =
   701   ab_group_add + ordered_ab_semigroup_add
   702 begin
   703 
   704 subclass ordered_cancel_ab_semigroup_add ..
   705 
   706 subclass ordered_ab_semigroup_add_imp_le
   707 proof
   708   fix a b c :: 'a
   709   assume "c + a \<le> c + b"
   710   hence "(-c) + (c + a) \<le> (-c) + (c + b)" by (rule add_left_mono)
   711   hence "((-c) + c) + a \<le> ((-c) + c) + b" by (simp only: add_assoc)
   712   thus "a \<le> b" by simp
   713 qed
   714 
   715 subclass ordered_comm_monoid_add ..
   716 
   717 lemma max_diff_distrib_left:
   718   shows "max x y - z = max (x - z) (y - z)"
   719 by (simp add: diff_minus, rule max_add_distrib_left) 
   720 
   721 lemma min_diff_distrib_left:
   722   shows "min x y - z = min (x - z) (y - z)"
   723 by (simp add: diff_minus, rule min_add_distrib_left) 
   724 
   725 lemma le_imp_neg_le:
   726   assumes "a \<le> b" shows "-b \<le> -a"
   727 proof -
   728   have "-a+a \<le> -a+b" using `a \<le> b` by (rule add_left_mono) 
   729   hence "0 \<le> -a+b" by simp
   730   hence "0 + (-b) \<le> (-a + b) + (-b)" by (rule add_right_mono) 
   731   thus ?thesis by (simp add: add_assoc)
   732 qed
   733 
   734 lemma neg_le_iff_le [simp]: "- b \<le> - a \<longleftrightarrow> a \<le> b"
   735 proof 
   736   assume "- b \<le> - a"
   737   hence "- (- a) \<le> - (- b)" by (rule le_imp_neg_le)
   738   thus "a\<le>b" by simp
   739 next
   740   assume "a\<le>b"
   741   thus "-b \<le> -a" by (rule le_imp_neg_le)
   742 qed
   743 
   744 lemma neg_le_0_iff_le [simp]: "- a \<le> 0 \<longleftrightarrow> 0 \<le> a"
   745 by (subst neg_le_iff_le [symmetric], simp)
   746 
   747 lemma neg_0_le_iff_le [simp]: "0 \<le> - a \<longleftrightarrow> a \<le> 0"
   748 by (subst neg_le_iff_le [symmetric], simp)
   749 
   750 lemma neg_less_iff_less [simp]: "- b < - a \<longleftrightarrow> a < b"
   751 by (force simp add: less_le) 
   752 
   753 lemma neg_less_0_iff_less [simp]: "- a < 0 \<longleftrightarrow> 0 < a"
   754 by (subst neg_less_iff_less [symmetric], simp)
   755 
   756 lemma neg_0_less_iff_less [simp]: "0 < - a \<longleftrightarrow> a < 0"
   757 by (subst neg_less_iff_less [symmetric], simp)
   758 
   759 text{*The next several equations can make the simplifier loop!*}
   760 
   761 lemma less_minus_iff: "a < - b \<longleftrightarrow> b < - a"
   762 proof -
   763   have "(- (-a) < - b) = (b < - a)" by (rule neg_less_iff_less)
   764   thus ?thesis by simp
   765 qed
   766 
   767 lemma minus_less_iff: "- a < b \<longleftrightarrow> - b < a"
   768 proof -
   769   have "(- a < - (-b)) = (- b < a)" by (rule neg_less_iff_less)
   770   thus ?thesis by simp
   771 qed
   772 
   773 lemma le_minus_iff: "a \<le> - b \<longleftrightarrow> b \<le> - a"
   774 proof -
   775   have mm: "!! a (b::'a). (-(-a)) < -b \<Longrightarrow> -(-b) < -a" by (simp only: minus_less_iff)
   776   have "(- (- a) <= -b) = (b <= - a)" 
   777     apply (auto simp only: le_less)
   778     apply (drule mm)
   779     apply (simp_all)
   780     apply (drule mm[simplified], assumption)
   781     done
   782   then show ?thesis by simp
   783 qed
   784 
   785 lemma minus_le_iff: "- a \<le> b \<longleftrightarrow> - b \<le> a"
   786 by (auto simp add: le_less minus_less_iff)
   787 
   788 lemma diff_less_0_iff_less [simp, no_atp]:
   789   "a - b < 0 \<longleftrightarrow> a < b"
   790 proof -
   791   have "a - b < 0 \<longleftrightarrow> a + (- b) < b + (- b)" by (simp add: diff_minus)
   792   also have "... \<longleftrightarrow> a < b" by (simp only: add_less_cancel_right)
   793   finally show ?thesis .
   794 qed
   795 
   796 lemmas less_iff_diff_less_0 = diff_less_0_iff_less [symmetric]
   797 
   798 lemma diff_less_eq[algebra_simps, field_simps]: "a - b < c \<longleftrightarrow> a < c + b"
   799 apply (subst less_iff_diff_less_0 [of a])
   800 apply (rule less_iff_diff_less_0 [of _ c, THEN ssubst])
   801 apply (simp add: diff_minus add_ac)
   802 done
   803 
   804 lemma less_diff_eq[algebra_simps, field_simps]: "a < c - b \<longleftrightarrow> a + b < c"
   805 apply (subst less_iff_diff_less_0 [of "a + b"])
   806 apply (subst less_iff_diff_less_0 [of a])
   807 apply (simp add: diff_minus add_ac)
   808 done
   809 
   810 lemma diff_le_eq[algebra_simps, field_simps]: "a - b \<le> c \<longleftrightarrow> a \<le> c + b"
   811 by (auto simp add: le_less diff_less_eq diff_add_cancel add_diff_cancel)
   812 
   813 lemma le_diff_eq[algebra_simps, field_simps]: "a \<le> c - b \<longleftrightarrow> a + b \<le> c"
   814 by (auto simp add: le_less less_diff_eq diff_add_cancel add_diff_cancel)
   815 
   816 lemma diff_le_0_iff_le [simp, no_atp]:
   817   "a - b \<le> 0 \<longleftrightarrow> a \<le> b"
   818   by (simp add: algebra_simps)
   819 
   820 lemmas le_iff_diff_le_0 = diff_le_0_iff_le [symmetric]
   821 
   822 lemma diff_eq_diff_less:
   823   "a - b = c - d \<Longrightarrow> a < b \<longleftrightarrow> c < d"
   824   by (auto simp only: less_iff_diff_less_0 [of a b] less_iff_diff_less_0 [of c d])
   825 
   826 lemma diff_eq_diff_less_eq:
   827   "a - b = c - d \<Longrightarrow> a \<le> b \<longleftrightarrow> c \<le> d"
   828   by (auto simp only: le_iff_diff_le_0 [of a b] le_iff_diff_le_0 [of c d])
   829 
   830 end
   831 
   832 use "Tools/abel_cancel.ML"
   833 
   834 simproc_setup abel_cancel_sum
   835   ("a + b::'a::ab_group_add" | "a - b::'a::ab_group_add") =
   836   {* fn phi => Abel_Cancel.sum_proc *}
   837 
   838 simproc_setup abel_cancel_relation
   839   ("a < (b::'a::ordered_ab_group_add)" | "a \<le> (b::'a::ordered_ab_group_add)" | "c = (d::'b::ab_group_add)") =
   840   {* fn phi => Abel_Cancel.rel_proc *}
   841 
   842 class linordered_ab_semigroup_add =
   843   linorder + ordered_ab_semigroup_add
   844 
   845 class linordered_cancel_ab_semigroup_add =
   846   linorder + ordered_cancel_ab_semigroup_add
   847 begin
   848 
   849 subclass linordered_ab_semigroup_add ..
   850 
   851 subclass ordered_ab_semigroup_add_imp_le
   852 proof
   853   fix a b c :: 'a
   854   assume le: "c + a <= c + b"  
   855   show "a <= b"
   856   proof (rule ccontr)
   857     assume w: "~ a \<le> b"
   858     hence "b <= a" by (simp add: linorder_not_le)
   859     hence le2: "c + b <= c + a" by (rule add_left_mono)
   860     have "a = b" 
   861       apply (insert le)
   862       apply (insert le2)
   863       apply (drule antisym, simp_all)
   864       done
   865     with w show False 
   866       by (simp add: linorder_not_le [symmetric])
   867   qed
   868 qed
   869 
   870 end
   871 
   872 class linordered_ab_group_add = linorder + ordered_ab_group_add
   873 begin
   874 
   875 subclass linordered_cancel_ab_semigroup_add ..
   876 
   877 lemma neg_less_eq_nonneg [simp]:
   878   "- a \<le> a \<longleftrightarrow> 0 \<le> a"
   879 proof
   880   assume A: "- a \<le> a" show "0 \<le> a"
   881   proof (rule classical)
   882     assume "\<not> 0 \<le> a"
   883     then have "a < 0" by auto
   884     with A have "- a < 0" by (rule le_less_trans)
   885     then show ?thesis by auto
   886   qed
   887 next
   888   assume A: "0 \<le> a" show "- a \<le> a"
   889   proof (rule order_trans)
   890     show "- a \<le> 0" using A by (simp add: minus_le_iff)
   891   next
   892     show "0 \<le> a" using A .
   893   qed
   894 qed
   895 
   896 lemma neg_less_nonneg [simp]:
   897   "- a < a \<longleftrightarrow> 0 < a"
   898 proof
   899   assume A: "- a < a" show "0 < a"
   900   proof (rule classical)
   901     assume "\<not> 0 < a"
   902     then have "a \<le> 0" by auto
   903     with A have "- a < 0" by (rule less_le_trans)
   904     then show ?thesis by auto
   905   qed
   906 next
   907   assume A: "0 < a" show "- a < a"
   908   proof (rule less_trans)
   909     show "- a < 0" using A by (simp add: minus_le_iff)
   910   next
   911     show "0 < a" using A .
   912   qed
   913 qed
   914 
   915 lemma less_eq_neg_nonpos [simp]:
   916   "a \<le> - a \<longleftrightarrow> a \<le> 0"
   917 proof
   918   assume A: "a \<le> - a" show "a \<le> 0"
   919   proof (rule classical)
   920     assume "\<not> a \<le> 0"
   921     then have "0 < a" by auto
   922     then have "0 < - a" using A by (rule less_le_trans)
   923     then show ?thesis by auto
   924   qed
   925 next
   926   assume A: "a \<le> 0" show "a \<le> - a"
   927   proof (rule order_trans)
   928     show "0 \<le> - a" using A by (simp add: minus_le_iff)
   929   next
   930     show "a \<le> 0" using A .
   931   qed
   932 qed
   933 
   934 lemma equal_neg_zero [simp]:
   935   "a = - a \<longleftrightarrow> a = 0"
   936 proof
   937   assume "a = 0" then show "a = - a" by simp
   938 next
   939   assume A: "a = - a" show "a = 0"
   940   proof (cases "0 \<le> a")
   941     case True with A have "0 \<le> - a" by auto
   942     with le_minus_iff have "a \<le> 0" by simp
   943     with True show ?thesis by (auto intro: order_trans)
   944   next
   945     case False then have B: "a \<le> 0" by auto
   946     with A have "- a \<le> 0" by auto
   947     with B show ?thesis by (auto intro: order_trans)
   948   qed
   949 qed
   950 
   951 lemma neg_equal_zero [simp]:
   952   "- a = a \<longleftrightarrow> a = 0"
   953   by (auto dest: sym)
   954 
   955 lemma double_zero [simp]:
   956   "a + a = 0 \<longleftrightarrow> a = 0"
   957 proof
   958   assume assm: "a + a = 0"
   959   then have a: "- a = a" by (rule minus_unique)
   960   then show "a = 0" by (simp only: neg_equal_zero)
   961 qed simp
   962 
   963 lemma double_zero_sym [simp]:
   964   "0 = a + a \<longleftrightarrow> a = 0"
   965   by (rule, drule sym) simp_all
   966 
   967 lemma zero_less_double_add_iff_zero_less_single_add [simp]:
   968   "0 < a + a \<longleftrightarrow> 0 < a"
   969 proof
   970   assume "0 < a + a"
   971   then have "0 - a < a" by (simp only: diff_less_eq)
   972   then have "- a < a" by simp
   973   then show "0 < a" by (simp only: neg_less_nonneg)
   974 next
   975   assume "0 < a"
   976   with this have "0 + 0 < a + a"
   977     by (rule add_strict_mono)
   978   then show "0 < a + a" by simp
   979 qed
   980 
   981 lemma zero_le_double_add_iff_zero_le_single_add [simp]:
   982   "0 \<le> a + a \<longleftrightarrow> 0 \<le> a"
   983   by (auto simp add: le_less)
   984 
   985 lemma double_add_less_zero_iff_single_add_less_zero [simp]:
   986   "a + a < 0 \<longleftrightarrow> a < 0"
   987 proof -
   988   have "\<not> a + a < 0 \<longleftrightarrow> \<not> a < 0"
   989     by (simp add: not_less)
   990   then show ?thesis by simp
   991 qed
   992 
   993 lemma double_add_le_zero_iff_single_add_le_zero [simp]:
   994   "a + a \<le> 0 \<longleftrightarrow> a \<le> 0" 
   995 proof -
   996   have "\<not> a + a \<le> 0 \<longleftrightarrow> \<not> a \<le> 0"
   997     by (simp add: not_le)
   998   then show ?thesis by simp
   999 qed
  1000 
  1001 lemma le_minus_self_iff:
  1002   "a \<le> - a \<longleftrightarrow> a \<le> 0"
  1003 proof -
  1004   from add_le_cancel_left [of "- a" "a + a" 0]
  1005   have "a \<le> - a \<longleftrightarrow> a + a \<le> 0" 
  1006     by (simp add: add_assoc [symmetric])
  1007   thus ?thesis by simp
  1008 qed
  1009 
  1010 lemma minus_le_self_iff:
  1011   "- a \<le> a \<longleftrightarrow> 0 \<le> a"
  1012 proof -
  1013   from add_le_cancel_left [of "- a" 0 "a + a"]
  1014   have "- a \<le> a \<longleftrightarrow> 0 \<le> a + a" 
  1015     by (simp add: add_assoc [symmetric])
  1016   thus ?thesis by simp
  1017 qed
  1018 
  1019 lemma minus_max_eq_min:
  1020   "- max x y = min (-x) (-y)"
  1021   by (auto simp add: max_def min_def)
  1022 
  1023 lemma minus_min_eq_max:
  1024   "- min x y = max (-x) (-y)"
  1025   by (auto simp add: max_def min_def)
  1026 
  1027 end
  1028 
  1029 context ordered_comm_monoid_add
  1030 begin
  1031 
  1032 lemma add_increasing:
  1033   "0 \<le> a \<Longrightarrow> b \<le> c \<Longrightarrow> b \<le> a + c"
  1034   by (insert add_mono [of 0 a b c], simp)
  1035 
  1036 lemma add_increasing2:
  1037   "0 \<le> c \<Longrightarrow> b \<le> a \<Longrightarrow> b \<le> a + c"
  1038   by (simp add: add_increasing add_commute [of a])
  1039 
  1040 lemma add_strict_increasing:
  1041   "0 < a \<Longrightarrow> b \<le> c \<Longrightarrow> b < a + c"
  1042   by (insert add_less_le_mono [of 0 a b c], simp)
  1043 
  1044 lemma add_strict_increasing2:
  1045   "0 \<le> a \<Longrightarrow> b < c \<Longrightarrow> b < a + c"
  1046   by (insert add_le_less_mono [of 0 a b c], simp)
  1047 
  1048 end
  1049 
  1050 class abs =
  1051   fixes abs :: "'a \<Rightarrow> 'a"
  1052 begin
  1053 
  1054 notation (xsymbols)
  1055   abs  ("\<bar>_\<bar>")
  1056 
  1057 notation (HTML output)
  1058   abs  ("\<bar>_\<bar>")
  1059 
  1060 end
  1061 
  1062 class sgn =
  1063   fixes sgn :: "'a \<Rightarrow> 'a"
  1064 
  1065 class abs_if = minus + uminus + ord + zero + abs +
  1066   assumes abs_if: "\<bar>a\<bar> = (if a < 0 then - a else a)"
  1067 
  1068 class sgn_if = minus + uminus + zero + one + ord + sgn +
  1069   assumes sgn_if: "sgn x = (if x = 0 then 0 else if 0 < x then 1 else - 1)"
  1070 begin
  1071 
  1072 lemma sgn0 [simp]: "sgn 0 = 0"
  1073   by (simp add:sgn_if)
  1074 
  1075 end
  1076 
  1077 class ordered_ab_group_add_abs = ordered_ab_group_add + abs +
  1078   assumes abs_ge_zero [simp]: "\<bar>a\<bar> \<ge> 0"
  1079     and abs_ge_self: "a \<le> \<bar>a\<bar>"
  1080     and abs_leI: "a \<le> b \<Longrightarrow> - a \<le> b \<Longrightarrow> \<bar>a\<bar> \<le> b"
  1081     and abs_minus_cancel [simp]: "\<bar>-a\<bar> = \<bar>a\<bar>"
  1082     and abs_triangle_ineq: "\<bar>a + b\<bar> \<le> \<bar>a\<bar> + \<bar>b\<bar>"
  1083 begin
  1084 
  1085 lemma abs_minus_le_zero: "- \<bar>a\<bar> \<le> 0"
  1086   unfolding neg_le_0_iff_le by simp
  1087 
  1088 lemma abs_of_nonneg [simp]:
  1089   assumes nonneg: "0 \<le> a" shows "\<bar>a\<bar> = a"
  1090 proof (rule antisym)
  1091   from nonneg le_imp_neg_le have "- a \<le> 0" by simp
  1092   from this nonneg have "- a \<le> a" by (rule order_trans)
  1093   then show "\<bar>a\<bar> \<le> a" by (auto intro: abs_leI)
  1094 qed (rule abs_ge_self)
  1095 
  1096 lemma abs_idempotent [simp]: "\<bar>\<bar>a\<bar>\<bar> = \<bar>a\<bar>"
  1097 by (rule antisym)
  1098    (auto intro!: abs_ge_self abs_leI order_trans [of "- \<bar>a\<bar>" 0 "\<bar>a\<bar>"])
  1099 
  1100 lemma abs_eq_0 [simp]: "\<bar>a\<bar> = 0 \<longleftrightarrow> a = 0"
  1101 proof -
  1102   have "\<bar>a\<bar> = 0 \<Longrightarrow> a = 0"
  1103   proof (rule antisym)
  1104     assume zero: "\<bar>a\<bar> = 0"
  1105     with abs_ge_self show "a \<le> 0" by auto
  1106     from zero have "\<bar>-a\<bar> = 0" by simp
  1107     with abs_ge_self [of "- a"] have "- a \<le> 0" by auto
  1108     with neg_le_0_iff_le show "0 \<le> a" by auto
  1109   qed
  1110   then show ?thesis by auto
  1111 qed
  1112 
  1113 lemma abs_zero [simp]: "\<bar>0\<bar> = 0"
  1114 by simp
  1115 
  1116 lemma abs_0_eq [simp, no_atp]: "0 = \<bar>a\<bar> \<longleftrightarrow> a = 0"
  1117 proof -
  1118   have "0 = \<bar>a\<bar> \<longleftrightarrow> \<bar>a\<bar> = 0" by (simp only: eq_ac)
  1119   thus ?thesis by simp
  1120 qed
  1121 
  1122 lemma abs_le_zero_iff [simp]: "\<bar>a\<bar> \<le> 0 \<longleftrightarrow> a = 0" 
  1123 proof
  1124   assume "\<bar>a\<bar> \<le> 0"
  1125   then have "\<bar>a\<bar> = 0" by (rule antisym) simp
  1126   thus "a = 0" by simp
  1127 next
  1128   assume "a = 0"
  1129   thus "\<bar>a\<bar> \<le> 0" by simp
  1130 qed
  1131 
  1132 lemma zero_less_abs_iff [simp]: "0 < \<bar>a\<bar> \<longleftrightarrow> a \<noteq> 0"
  1133 by (simp add: less_le)
  1134 
  1135 lemma abs_not_less_zero [simp]: "\<not> \<bar>a\<bar> < 0"
  1136 proof -
  1137   have a: "\<And>x y. x \<le> y \<Longrightarrow> \<not> y < x" by auto
  1138   show ?thesis by (simp add: a)
  1139 qed
  1140 
  1141 lemma abs_ge_minus_self: "- a \<le> \<bar>a\<bar>"
  1142 proof -
  1143   have "- a \<le> \<bar>-a\<bar>" by (rule abs_ge_self)
  1144   then show ?thesis by simp
  1145 qed
  1146 
  1147 lemma abs_minus_commute: 
  1148   "\<bar>a - b\<bar> = \<bar>b - a\<bar>"
  1149 proof -
  1150   have "\<bar>a - b\<bar> = \<bar>- (a - b)\<bar>" by (simp only: abs_minus_cancel)
  1151   also have "... = \<bar>b - a\<bar>" by simp
  1152   finally show ?thesis .
  1153 qed
  1154 
  1155 lemma abs_of_pos: "0 < a \<Longrightarrow> \<bar>a\<bar> = a"
  1156 by (rule abs_of_nonneg, rule less_imp_le)
  1157 
  1158 lemma abs_of_nonpos [simp]:
  1159   assumes "a \<le> 0" shows "\<bar>a\<bar> = - a"
  1160 proof -
  1161   let ?b = "- a"
  1162   have "- ?b \<le> 0 \<Longrightarrow> \<bar>- ?b\<bar> = - (- ?b)"
  1163   unfolding abs_minus_cancel [of "?b"]
  1164   unfolding neg_le_0_iff_le [of "?b"]
  1165   unfolding minus_minus by (erule abs_of_nonneg)
  1166   then show ?thesis using assms by auto
  1167 qed
  1168   
  1169 lemma abs_of_neg: "a < 0 \<Longrightarrow> \<bar>a\<bar> = - a"
  1170 by (rule abs_of_nonpos, rule less_imp_le)
  1171 
  1172 lemma abs_le_D1: "\<bar>a\<bar> \<le> b \<Longrightarrow> a \<le> b"
  1173 by (insert abs_ge_self, blast intro: order_trans)
  1174 
  1175 lemma abs_le_D2: "\<bar>a\<bar> \<le> b \<Longrightarrow> - a \<le> b"
  1176 by (insert abs_le_D1 [of "- a"], simp)
  1177 
  1178 lemma abs_le_iff: "\<bar>a\<bar> \<le> b \<longleftrightarrow> a \<le> b \<and> - a \<le> b"
  1179 by (blast intro: abs_leI dest: abs_le_D1 abs_le_D2)
  1180 
  1181 lemma abs_triangle_ineq2: "\<bar>a\<bar> - \<bar>b\<bar> \<le> \<bar>a - b\<bar>"
  1182 proof -
  1183   have "\<bar>a\<bar> = \<bar>b + (a - b)\<bar>"
  1184     by (simp add: algebra_simps add_diff_cancel)
  1185   then have "\<bar>a\<bar> \<le> \<bar>b\<bar> + \<bar>a - b\<bar>"
  1186     by (simp add: abs_triangle_ineq)
  1187   then show ?thesis
  1188     by (simp add: algebra_simps)
  1189 qed
  1190 
  1191 lemma abs_triangle_ineq2_sym: "\<bar>a\<bar> - \<bar>b\<bar> \<le> \<bar>b - a\<bar>"
  1192   by (simp only: abs_minus_commute [of b] abs_triangle_ineq2)
  1193 
  1194 lemma abs_triangle_ineq3: "\<bar>\<bar>a\<bar> - \<bar>b\<bar>\<bar> \<le> \<bar>a - b\<bar>"
  1195   by (simp add: abs_le_iff abs_triangle_ineq2 abs_triangle_ineq2_sym)
  1196 
  1197 lemma abs_triangle_ineq4: "\<bar>a - b\<bar> \<le> \<bar>a\<bar> + \<bar>b\<bar>"
  1198 proof -
  1199   have "\<bar>a - b\<bar> = \<bar>a + - b\<bar>" by (subst diff_minus, rule refl)
  1200   also have "... \<le> \<bar>a\<bar> + \<bar>- b\<bar>" by (rule abs_triangle_ineq)
  1201   finally show ?thesis by simp
  1202 qed
  1203 
  1204 lemma abs_diff_triangle_ineq: "\<bar>a + b - (c + d)\<bar> \<le> \<bar>a - c\<bar> + \<bar>b - d\<bar>"
  1205 proof -
  1206   have "\<bar>a + b - (c+d)\<bar> = \<bar>(a-c) + (b-d)\<bar>" by (simp add: diff_minus add_ac)
  1207   also have "... \<le> \<bar>a-c\<bar> + \<bar>b-d\<bar>" by (rule abs_triangle_ineq)
  1208   finally show ?thesis .
  1209 qed
  1210 
  1211 lemma abs_add_abs [simp]:
  1212   "\<bar>\<bar>a\<bar> + \<bar>b\<bar>\<bar> = \<bar>a\<bar> + \<bar>b\<bar>" (is "?L = ?R")
  1213 proof (rule antisym)
  1214   show "?L \<ge> ?R" by(rule abs_ge_self)
  1215 next
  1216   have "?L \<le> \<bar>\<bar>a\<bar>\<bar> + \<bar>\<bar>b\<bar>\<bar>" by(rule abs_triangle_ineq)
  1217   also have "\<dots> = ?R" by simp
  1218   finally show "?L \<le> ?R" .
  1219 qed
  1220 
  1221 end
  1222 
  1223 
  1224 subsection {* Tools setup *}
  1225 
  1226 lemma add_mono_thms_linordered_semiring [no_atp]:
  1227   fixes i j k :: "'a\<Colon>ordered_ab_semigroup_add"
  1228   shows "i \<le> j \<and> k \<le> l \<Longrightarrow> i + k \<le> j + l"
  1229     and "i = j \<and> k \<le> l \<Longrightarrow> i + k \<le> j + l"
  1230     and "i \<le> j \<and> k = l \<Longrightarrow> i + k \<le> j + l"
  1231     and "i = j \<and> k = l \<Longrightarrow> i + k = j + l"
  1232 by (rule add_mono, clarify+)+
  1233 
  1234 lemma add_mono_thms_linordered_field [no_atp]:
  1235   fixes i j k :: "'a\<Colon>ordered_cancel_ab_semigroup_add"
  1236   shows "i < j \<and> k = l \<Longrightarrow> i + k < j + l"
  1237     and "i = j \<and> k < l \<Longrightarrow> i + k < j + l"
  1238     and "i < j \<and> k \<le> l \<Longrightarrow> i + k < j + l"
  1239     and "i \<le> j \<and> k < l \<Longrightarrow> i + k < j + l"
  1240     and "i < j \<and> k < l \<Longrightarrow> i + k < j + l"
  1241 by (auto intro: add_strict_right_mono add_strict_left_mono
  1242   add_less_le_mono add_le_less_mono add_strict_mono)
  1243 
  1244 code_modulename SML
  1245   Groups Arith
  1246 
  1247 code_modulename OCaml
  1248   Groups Arith
  1249 
  1250 code_modulename Haskell
  1251   Groups Arith
  1252 
  1253 
  1254 text {* Legacy *}
  1255 
  1256 lemmas diff_def = diff_minus
  1257 
  1258 end