src/HOL/Groups.thy
author kuncar
Fri Dec 09 18:07:04 2011 +0100 (2011-12-09)
changeset 45802 b16f976db515
parent 45548 3e2722d66169
child 48556 62a3fbf9d35b
permissions -rw-r--r--
Quotient_Info stores only relation maps
     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 lemmas equals_zero_I = minus_unique (* legacy name *)
   288 
   289 lemma minus_zero [simp]: "- 0 = 0"
   290 proof -
   291   have "0 + 0 = 0" by (rule add_0_right)
   292   thus "- 0 = 0" by (rule minus_unique)
   293 qed
   294 
   295 lemma minus_minus [simp]: "- (- a) = a"
   296 proof -
   297   have "- a + a = 0" by (rule left_minus)
   298   thus "- (- a) = a" by (rule minus_unique)
   299 qed
   300 
   301 lemma right_minus [simp]: "a + - a = 0"
   302 proof -
   303   have "a + - a = - (- a) + - a" by simp
   304   also have "\<dots> = 0" by (rule left_minus)
   305   finally show ?thesis .
   306 qed
   307 
   308 subclass cancel_semigroup_add
   309 proof
   310   fix a b c :: 'a
   311   assume "a + b = a + c"
   312   then have "- a + a + b = - a + a + c"
   313     unfolding add_assoc by simp
   314   then show "b = c" by simp
   315 next
   316   fix a b c :: 'a
   317   assume "b + a = c + a"
   318   then have "b + a + - a = c + a  + - a" by simp
   319   then show "b = c" unfolding add_assoc by simp
   320 qed
   321 
   322 lemma minus_add_cancel: "- a + (a + b) = b"
   323 by (simp add: add_assoc [symmetric])
   324 
   325 lemma add_minus_cancel: "a + (- a + b) = b"
   326 by (simp add: add_assoc [symmetric])
   327 
   328 lemma minus_add: "- (a + b) = - b + - a"
   329 proof -
   330   have "(a + b) + (- b + - a) = 0"
   331     by (simp add: add_assoc add_minus_cancel)
   332   thus "- (a + b) = - b + - a"
   333     by (rule minus_unique)
   334 qed
   335 
   336 lemma right_minus_eq: "a - b = 0 \<longleftrightarrow> a = b"
   337 proof
   338   assume "a - b = 0"
   339   have "a = (a - b) + b" by (simp add:diff_minus add_assoc)
   340   also have "\<dots> = b" using `a - b = 0` by simp
   341   finally show "a = b" .
   342 next
   343   assume "a = b" thus "a - b = 0" by (simp add: diff_minus)
   344 qed
   345 
   346 lemma diff_self [simp]: "a - a = 0"
   347 by (simp add: diff_minus)
   348 
   349 lemma diff_0 [simp]: "0 - a = - a"
   350 by (simp add: diff_minus)
   351 
   352 lemma diff_0_right [simp]: "a - 0 = a" 
   353 by (simp add: diff_minus)
   354 
   355 lemma diff_minus_eq_add [simp]: "a - - b = a + b"
   356 by (simp add: diff_minus)
   357 
   358 lemma neg_equal_iff_equal [simp]:
   359   "- a = - b \<longleftrightarrow> a = b" 
   360 proof 
   361   assume "- a = - b"
   362   hence "- (- a) = - (- b)" by simp
   363   thus "a = b" by simp
   364 next
   365   assume "a = b"
   366   thus "- a = - b" by simp
   367 qed
   368 
   369 lemma neg_equal_0_iff_equal [simp]:
   370   "- a = 0 \<longleftrightarrow> a = 0"
   371 by (subst neg_equal_iff_equal [symmetric], simp)
   372 
   373 lemma neg_0_equal_iff_equal [simp]:
   374   "0 = - a \<longleftrightarrow> 0 = a"
   375 by (subst neg_equal_iff_equal [symmetric], simp)
   376 
   377 text{*The next two equations can make the simplifier loop!*}
   378 
   379 lemma equation_minus_iff:
   380   "a = - b \<longleftrightarrow> b = - a"
   381 proof -
   382   have "- (- a) = - b \<longleftrightarrow> - a = b" by (rule neg_equal_iff_equal)
   383   thus ?thesis by (simp add: eq_commute)
   384 qed
   385 
   386 lemma minus_equation_iff:
   387   "- a = b \<longleftrightarrow> - b = a"
   388 proof -
   389   have "- a = - (- b) \<longleftrightarrow> a = -b" by (rule neg_equal_iff_equal)
   390   thus ?thesis by (simp add: eq_commute)
   391 qed
   392 
   393 lemma diff_add_cancel: "a - b + b = a"
   394 by (simp add: diff_minus add_assoc)
   395 
   396 lemma add_diff_cancel: "a + b - b = a"
   397 by (simp add: diff_minus add_assoc)
   398 
   399 declare diff_minus[symmetric, algebra_simps, field_simps]
   400 
   401 lemma eq_neg_iff_add_eq_0: "a = - b \<longleftrightarrow> a + b = 0"
   402 proof
   403   assume "a = - b" then show "a + b = 0" by simp
   404 next
   405   assume "a + b = 0"
   406   moreover have "a + (b + - b) = (a + b) + - b"
   407     by (simp only: add_assoc)
   408   ultimately show "a = - b" by simp
   409 qed
   410 
   411 lemma add_eq_0_iff: "x + y = 0 \<longleftrightarrow> y = - x"
   412   unfolding eq_neg_iff_add_eq_0 [symmetric]
   413   by (rule equation_minus_iff)
   414 
   415 lemma minus_diff_eq [simp]: "- (a - b) = b - a"
   416   by (simp add: diff_minus minus_add)
   417 
   418 lemma add_diff_eq[algebra_simps, field_simps]: "a + (b - c) = (a + b) - c"
   419   by (simp add: diff_minus add_assoc)
   420 
   421 lemma diff_eq_eq[algebra_simps, field_simps]: "a - b = c \<longleftrightarrow> a = c + b"
   422   by (auto simp add: diff_minus add_assoc)
   423 
   424 lemma eq_diff_eq[algebra_simps, field_simps]: "a = c - b \<longleftrightarrow> a + b = c"
   425   by (auto simp add: diff_minus add_assoc)
   426 
   427 lemma diff_diff_eq2[algebra_simps, field_simps]: "a - (b - c) = (a + c) - b"
   428   by (simp add: diff_minus minus_add add_assoc)
   429 
   430 lemma eq_iff_diff_eq_0: "a = b \<longleftrightarrow> a - b = 0"
   431   by (fact right_minus_eq [symmetric])
   432 
   433 lemma diff_eq_diff_eq:
   434   "a - b = c - d \<Longrightarrow> a = b \<longleftrightarrow> c = d"
   435   by (simp add: eq_iff_diff_eq_0 [of a b] eq_iff_diff_eq_0 [of c d])
   436 
   437 end
   438 
   439 class ab_group_add = minus + uminus + comm_monoid_add +
   440   assumes ab_left_minus: "- a + a = 0"
   441   assumes ab_diff_minus: "a - b = a + (- b)"
   442 begin
   443 
   444 subclass group_add
   445   proof qed (simp_all add: ab_left_minus ab_diff_minus)
   446 
   447 subclass cancel_comm_monoid_add
   448 proof
   449   fix a b c :: 'a
   450   assume "a + b = a + c"
   451   then have "- a + a + b = - a + a + c"
   452     unfolding add_assoc by simp
   453   then show "b = c" by simp
   454 qed
   455 
   456 lemma uminus_add_conv_diff[algebra_simps, field_simps]:
   457   "- a + b = b - a"
   458 by (simp add:diff_minus add_commute)
   459 
   460 lemma minus_add_distrib [simp]:
   461   "- (a + b) = - a + - b"
   462 by (rule minus_unique) (simp add: add_ac)
   463 
   464 lemma diff_add_eq[algebra_simps, field_simps]: "(a - b) + c = (a + c) - b"
   465 by (simp add: diff_minus add_ac)
   466 
   467 lemma diff_diff_eq[algebra_simps, field_simps]: "(a - b) - c = a - (b + c)"
   468 by (simp add: diff_minus add_ac)
   469 
   470 (* FIXME: duplicates right_minus_eq from class group_add *)
   471 (* but only this one is declared as a simp rule. *)
   472 lemma diff_eq_0_iff_eq [simp, no_atp]: "a - b = 0 \<longleftrightarrow> a = b"
   473   by (rule right_minus_eq)
   474 
   475 end
   476 
   477 
   478 subsection {* (Partially) Ordered Groups *} 
   479 
   480 text {*
   481   The theory of partially ordered groups is taken from the books:
   482   \begin{itemize}
   483   \item \emph{Lattice Theory} by Garret Birkhoff, American Mathematical Society 1979 
   484   \item \emph{Partially Ordered Algebraic Systems}, Pergamon Press 1963
   485   \end{itemize}
   486   Most of the used notions can also be looked up in 
   487   \begin{itemize}
   488   \item \url{http://www.mathworld.com} by Eric Weisstein et. al.
   489   \item \emph{Algebra I} by van der Waerden, Springer.
   490   \end{itemize}
   491 *}
   492 
   493 class ordered_ab_semigroup_add = order + ab_semigroup_add +
   494   assumes add_left_mono: "a \<le> b \<Longrightarrow> c + a \<le> c + b"
   495 begin
   496 
   497 lemma add_right_mono:
   498   "a \<le> b \<Longrightarrow> a + c \<le> b + c"
   499 by (simp add: add_commute [of _ c] add_left_mono)
   500 
   501 text {* non-strict, in both arguments *}
   502 lemma add_mono:
   503   "a \<le> b \<Longrightarrow> c \<le> d \<Longrightarrow> a + c \<le> b + d"
   504   apply (erule add_right_mono [THEN order_trans])
   505   apply (simp add: add_commute add_left_mono)
   506   done
   507 
   508 end
   509 
   510 class ordered_cancel_ab_semigroup_add =
   511   ordered_ab_semigroup_add + cancel_ab_semigroup_add
   512 begin
   513 
   514 lemma add_strict_left_mono:
   515   "a < b \<Longrightarrow> c + a < c + b"
   516 by (auto simp add: less_le add_left_mono)
   517 
   518 lemma add_strict_right_mono:
   519   "a < b \<Longrightarrow> a + c < b + c"
   520 by (simp add: add_commute [of _ c] add_strict_left_mono)
   521 
   522 text{*Strict monotonicity in both arguments*}
   523 lemma add_strict_mono:
   524   "a < b \<Longrightarrow> c < d \<Longrightarrow> a + c < b + d"
   525 apply (erule add_strict_right_mono [THEN less_trans])
   526 apply (erule add_strict_left_mono)
   527 done
   528 
   529 lemma add_less_le_mono:
   530   "a < b \<Longrightarrow> c \<le> d \<Longrightarrow> a + c < b + d"
   531 apply (erule add_strict_right_mono [THEN less_le_trans])
   532 apply (erule add_left_mono)
   533 done
   534 
   535 lemma add_le_less_mono:
   536   "a \<le> b \<Longrightarrow> c < d \<Longrightarrow> a + c < b + d"
   537 apply (erule add_right_mono [THEN le_less_trans])
   538 apply (erule add_strict_left_mono) 
   539 done
   540 
   541 end
   542 
   543 class ordered_ab_semigroup_add_imp_le =
   544   ordered_cancel_ab_semigroup_add +
   545   assumes add_le_imp_le_left: "c + a \<le> c + b \<Longrightarrow> a \<le> b"
   546 begin
   547 
   548 lemma add_less_imp_less_left:
   549   assumes less: "c + a < c + b" shows "a < b"
   550 proof -
   551   from less have le: "c + a <= c + b" by (simp add: order_le_less)
   552   have "a <= b" 
   553     apply (insert le)
   554     apply (drule add_le_imp_le_left)
   555     by (insert le, drule add_le_imp_le_left, assumption)
   556   moreover have "a \<noteq> b"
   557   proof (rule ccontr)
   558     assume "~(a \<noteq> b)"
   559     then have "a = b" by simp
   560     then have "c + a = c + b" by simp
   561     with less show "False"by simp
   562   qed
   563   ultimately show "a < b" by (simp add: order_le_less)
   564 qed
   565 
   566 lemma add_less_imp_less_right:
   567   "a + c < b + c \<Longrightarrow> a < b"
   568 apply (rule add_less_imp_less_left [of c])
   569 apply (simp add: add_commute)  
   570 done
   571 
   572 lemma add_less_cancel_left [simp]:
   573   "c + a < c + b \<longleftrightarrow> a < b"
   574 by (blast intro: add_less_imp_less_left add_strict_left_mono) 
   575 
   576 lemma add_less_cancel_right [simp]:
   577   "a + c < b + c \<longleftrightarrow> a < b"
   578 by (blast intro: add_less_imp_less_right add_strict_right_mono)
   579 
   580 lemma add_le_cancel_left [simp]:
   581   "c + a \<le> c + b \<longleftrightarrow> a \<le> b"
   582 by (auto, drule add_le_imp_le_left, simp_all add: add_left_mono) 
   583 
   584 lemma add_le_cancel_right [simp]:
   585   "a + c \<le> b + c \<longleftrightarrow> a \<le> b"
   586 by (simp add: add_commute [of a c] add_commute [of b c])
   587 
   588 lemma add_le_imp_le_right:
   589   "a + c \<le> b + c \<Longrightarrow> a \<le> b"
   590 by simp
   591 
   592 lemma max_add_distrib_left:
   593   "max x y + z = max (x + z) (y + z)"
   594   unfolding max_def by auto
   595 
   596 lemma min_add_distrib_left:
   597   "min x y + z = min (x + z) (y + z)"
   598   unfolding min_def by auto
   599 
   600 lemma max_add_distrib_right:
   601   "x + max y z = max (x + y) (x + z)"
   602   unfolding max_def by auto
   603 
   604 lemma min_add_distrib_right:
   605   "x + min y z = min (x + y) (x + z)"
   606   unfolding min_def by auto
   607 
   608 end
   609 
   610 subsection {* Support for reasoning about signs *}
   611 
   612 class ordered_comm_monoid_add =
   613   ordered_cancel_ab_semigroup_add + comm_monoid_add
   614 begin
   615 
   616 lemma add_pos_nonneg:
   617   assumes "0 < a" and "0 \<le> b" shows "0 < a + b"
   618 proof -
   619   have "0 + 0 < a + b" 
   620     using assms by (rule add_less_le_mono)
   621   then show ?thesis by simp
   622 qed
   623 
   624 lemma add_pos_pos:
   625   assumes "0 < a" and "0 < b" shows "0 < a + b"
   626 by (rule add_pos_nonneg) (insert assms, auto)
   627 
   628 lemma add_nonneg_pos:
   629   assumes "0 \<le> a" and "0 < b" shows "0 < a + b"
   630 proof -
   631   have "0 + 0 < a + b" 
   632     using assms by (rule add_le_less_mono)
   633   then show ?thesis by simp
   634 qed
   635 
   636 lemma add_nonneg_nonneg [simp]:
   637   assumes "0 \<le> a" and "0 \<le> b" shows "0 \<le> a + b"
   638 proof -
   639   have "0 + 0 \<le> a + b" 
   640     using assms by (rule add_mono)
   641   then show ?thesis by simp
   642 qed
   643 
   644 lemma add_neg_nonpos:
   645   assumes "a < 0" and "b \<le> 0" shows "a + b < 0"
   646 proof -
   647   have "a + b < 0 + 0"
   648     using assms by (rule add_less_le_mono)
   649   then show ?thesis by simp
   650 qed
   651 
   652 lemma add_neg_neg: 
   653   assumes "a < 0" and "b < 0" shows "a + b < 0"
   654 by (rule add_neg_nonpos) (insert assms, auto)
   655 
   656 lemma add_nonpos_neg:
   657   assumes "a \<le> 0" and "b < 0" shows "a + b < 0"
   658 proof -
   659   have "a + b < 0 + 0"
   660     using assms by (rule add_le_less_mono)
   661   then show ?thesis by simp
   662 qed
   663 
   664 lemma add_nonpos_nonpos:
   665   assumes "a \<le> 0" and "b \<le> 0" shows "a + b \<le> 0"
   666 proof -
   667   have "a + b \<le> 0 + 0"
   668     using assms by (rule add_mono)
   669   then show ?thesis by simp
   670 qed
   671 
   672 lemmas add_sign_intros =
   673   add_pos_nonneg add_pos_pos add_nonneg_pos add_nonneg_nonneg
   674   add_neg_nonpos add_neg_neg add_nonpos_neg add_nonpos_nonpos
   675 
   676 lemma add_nonneg_eq_0_iff:
   677   assumes x: "0 \<le> x" and y: "0 \<le> y"
   678   shows "x + y = 0 \<longleftrightarrow> x = 0 \<and> y = 0"
   679 proof (intro iffI conjI)
   680   have "x = x + 0" by simp
   681   also have "x + 0 \<le> x + y" using y by (rule add_left_mono)
   682   also assume "x + y = 0"
   683   also have "0 \<le> x" using x .
   684   finally show "x = 0" .
   685 next
   686   have "y = 0 + y" by simp
   687   also have "0 + y \<le> x + y" using x by (rule add_right_mono)
   688   also assume "x + y = 0"
   689   also have "0 \<le> y" using y .
   690   finally show "y = 0" .
   691 next
   692   assume "x = 0 \<and> y = 0"
   693   then show "x + y = 0" by simp
   694 qed
   695 
   696 end
   697 
   698 class ordered_ab_group_add =
   699   ab_group_add + ordered_ab_semigroup_add
   700 begin
   701 
   702 subclass ordered_cancel_ab_semigroup_add ..
   703 
   704 subclass ordered_ab_semigroup_add_imp_le
   705 proof
   706   fix a b c :: 'a
   707   assume "c + a \<le> c + b"
   708   hence "(-c) + (c + a) \<le> (-c) + (c + b)" by (rule add_left_mono)
   709   hence "((-c) + c) + a \<le> ((-c) + c) + b" by (simp only: add_assoc)
   710   thus "a \<le> b" by simp
   711 qed
   712 
   713 subclass ordered_comm_monoid_add ..
   714 
   715 lemma max_diff_distrib_left:
   716   shows "max x y - z = max (x - z) (y - z)"
   717 by (simp add: diff_minus, rule max_add_distrib_left) 
   718 
   719 lemma min_diff_distrib_left:
   720   shows "min x y - z = min (x - z) (y - z)"
   721 by (simp add: diff_minus, rule min_add_distrib_left) 
   722 
   723 lemma le_imp_neg_le:
   724   assumes "a \<le> b" shows "-b \<le> -a"
   725 proof -
   726   have "-a+a \<le> -a+b" using `a \<le> b` by (rule add_left_mono) 
   727   hence "0 \<le> -a+b" by simp
   728   hence "0 + (-b) \<le> (-a + b) + (-b)" by (rule add_right_mono) 
   729   thus ?thesis by (simp add: add_assoc)
   730 qed
   731 
   732 lemma neg_le_iff_le [simp]: "- b \<le> - a \<longleftrightarrow> a \<le> b"
   733 proof 
   734   assume "- b \<le> - a"
   735   hence "- (- a) \<le> - (- b)" by (rule le_imp_neg_le)
   736   thus "a\<le>b" by simp
   737 next
   738   assume "a\<le>b"
   739   thus "-b \<le> -a" by (rule le_imp_neg_le)
   740 qed
   741 
   742 lemma neg_le_0_iff_le [simp]: "- a \<le> 0 \<longleftrightarrow> 0 \<le> a"
   743 by (subst neg_le_iff_le [symmetric], simp)
   744 
   745 lemma neg_0_le_iff_le [simp]: "0 \<le> - a \<longleftrightarrow> a \<le> 0"
   746 by (subst neg_le_iff_le [symmetric], simp)
   747 
   748 lemma neg_less_iff_less [simp]: "- b < - a \<longleftrightarrow> a < b"
   749 by (force simp add: less_le) 
   750 
   751 lemma neg_less_0_iff_less [simp]: "- a < 0 \<longleftrightarrow> 0 < a"
   752 by (subst neg_less_iff_less [symmetric], simp)
   753 
   754 lemma neg_0_less_iff_less [simp]: "0 < - a \<longleftrightarrow> a < 0"
   755 by (subst neg_less_iff_less [symmetric], simp)
   756 
   757 text{*The next several equations can make the simplifier loop!*}
   758 
   759 lemma less_minus_iff: "a < - b \<longleftrightarrow> b < - a"
   760 proof -
   761   have "(- (-a) < - b) = (b < - a)" by (rule neg_less_iff_less)
   762   thus ?thesis by simp
   763 qed
   764 
   765 lemma minus_less_iff: "- a < b \<longleftrightarrow> - b < a"
   766 proof -
   767   have "(- a < - (-b)) = (- b < a)" by (rule neg_less_iff_less)
   768   thus ?thesis by simp
   769 qed
   770 
   771 lemma le_minus_iff: "a \<le> - b \<longleftrightarrow> b \<le> - a"
   772 proof -
   773   have mm: "!! a (b::'a). (-(-a)) < -b \<Longrightarrow> -(-b) < -a" by (simp only: minus_less_iff)
   774   have "(- (- a) <= -b) = (b <= - a)" 
   775     apply (auto simp only: le_less)
   776     apply (drule mm)
   777     apply (simp_all)
   778     apply (drule mm[simplified], assumption)
   779     done
   780   then show ?thesis by simp
   781 qed
   782 
   783 lemma minus_le_iff: "- a \<le> b \<longleftrightarrow> - b \<le> a"
   784 by (auto simp add: le_less minus_less_iff)
   785 
   786 lemma diff_less_0_iff_less [simp, no_atp]:
   787   "a - b < 0 \<longleftrightarrow> a < b"
   788 proof -
   789   have "a - b < 0 \<longleftrightarrow> a + (- b) < b + (- b)" by (simp add: diff_minus)
   790   also have "... \<longleftrightarrow> a < b" by (simp only: add_less_cancel_right)
   791   finally show ?thesis .
   792 qed
   793 
   794 lemmas less_iff_diff_less_0 = diff_less_0_iff_less [symmetric]
   795 
   796 lemma diff_less_eq[algebra_simps, field_simps]: "a - b < c \<longleftrightarrow> a < c + b"
   797 apply (subst less_iff_diff_less_0 [of a])
   798 apply (rule less_iff_diff_less_0 [of _ c, THEN ssubst])
   799 apply (simp add: diff_minus add_ac)
   800 done
   801 
   802 lemma less_diff_eq[algebra_simps, field_simps]: "a < c - b \<longleftrightarrow> a + b < c"
   803 apply (subst less_iff_diff_less_0 [of "a + b"])
   804 apply (subst less_iff_diff_less_0 [of a])
   805 apply (simp add: diff_minus add_ac)
   806 done
   807 
   808 lemma diff_le_eq[algebra_simps, field_simps]: "a - b \<le> c \<longleftrightarrow> a \<le> c + b"
   809 by (auto simp add: le_less diff_less_eq diff_add_cancel add_diff_cancel)
   810 
   811 lemma le_diff_eq[algebra_simps, field_simps]: "a \<le> c - b \<longleftrightarrow> a + b \<le> c"
   812 by (auto simp add: le_less less_diff_eq diff_add_cancel add_diff_cancel)
   813 
   814 lemma diff_le_0_iff_le [simp, no_atp]:
   815   "a - b \<le> 0 \<longleftrightarrow> a \<le> b"
   816   by (simp add: algebra_simps)
   817 
   818 lemmas le_iff_diff_le_0 = diff_le_0_iff_le [symmetric]
   819 
   820 lemma diff_eq_diff_less:
   821   "a - b = c - d \<Longrightarrow> a < b \<longleftrightarrow> c < d"
   822   by (auto simp only: less_iff_diff_less_0 [of a b] less_iff_diff_less_0 [of c d])
   823 
   824 lemma diff_eq_diff_less_eq:
   825   "a - b = c - d \<Longrightarrow> a \<le> b \<longleftrightarrow> c \<le> d"
   826   by (auto simp only: le_iff_diff_le_0 [of a b] le_iff_diff_le_0 [of c d])
   827 
   828 end
   829 
   830 use "Tools/abel_cancel.ML"
   831 
   832 simproc_setup abel_cancel_sum
   833   ("a + b::'a::ab_group_add" | "a - b::'a::ab_group_add") =
   834   {* fn phi => Abel_Cancel.sum_proc *}
   835 
   836 simproc_setup abel_cancel_relation
   837   ("a < (b::'a::ordered_ab_group_add)" | "a \<le> (b::'a::ordered_ab_group_add)" | "c = (d::'b::ab_group_add)") =
   838   {* fn phi => Abel_Cancel.rel_proc *}
   839 
   840 class linordered_ab_semigroup_add =
   841   linorder + ordered_ab_semigroup_add
   842 
   843 class linordered_cancel_ab_semigroup_add =
   844   linorder + ordered_cancel_ab_semigroup_add
   845 begin
   846 
   847 subclass linordered_ab_semigroup_add ..
   848 
   849 subclass ordered_ab_semigroup_add_imp_le
   850 proof
   851   fix a b c :: 'a
   852   assume le: "c + a <= c + b"  
   853   show "a <= b"
   854   proof (rule ccontr)
   855     assume w: "~ a \<le> b"
   856     hence "b <= a" by (simp add: linorder_not_le)
   857     hence le2: "c + b <= c + a" by (rule add_left_mono)
   858     have "a = b" 
   859       apply (insert le)
   860       apply (insert le2)
   861       apply (drule antisym, simp_all)
   862       done
   863     with w show False 
   864       by (simp add: linorder_not_le [symmetric])
   865   qed
   866 qed
   867 
   868 end
   869 
   870 class linordered_ab_group_add = linorder + ordered_ab_group_add
   871 begin
   872 
   873 subclass linordered_cancel_ab_semigroup_add ..
   874 
   875 lemma neg_less_eq_nonneg [simp]:
   876   "- a \<le> a \<longleftrightarrow> 0 \<le> a"
   877 proof
   878   assume A: "- a \<le> a" show "0 \<le> a"
   879   proof (rule classical)
   880     assume "\<not> 0 \<le> a"
   881     then have "a < 0" by auto
   882     with A have "- a < 0" by (rule le_less_trans)
   883     then show ?thesis by auto
   884   qed
   885 next
   886   assume A: "0 \<le> a" show "- a \<le> a"
   887   proof (rule order_trans)
   888     show "- a \<le> 0" using A by (simp add: minus_le_iff)
   889   next
   890     show "0 \<le> a" using A .
   891   qed
   892 qed
   893 
   894 lemma neg_less_nonneg [simp]:
   895   "- a < a \<longleftrightarrow> 0 < a"
   896 proof
   897   assume A: "- a < a" show "0 < a"
   898   proof (rule classical)
   899     assume "\<not> 0 < a"
   900     then have "a \<le> 0" by auto
   901     with A have "- a < 0" by (rule less_le_trans)
   902     then show ?thesis by auto
   903   qed
   904 next
   905   assume A: "0 < a" show "- a < a"
   906   proof (rule less_trans)
   907     show "- a < 0" using A by (simp add: minus_le_iff)
   908   next
   909     show "0 < a" using A .
   910   qed
   911 qed
   912 
   913 lemma less_eq_neg_nonpos [simp]:
   914   "a \<le> - a \<longleftrightarrow> a \<le> 0"
   915 proof
   916   assume A: "a \<le> - a" show "a \<le> 0"
   917   proof (rule classical)
   918     assume "\<not> a \<le> 0"
   919     then have "0 < a" by auto
   920     then have "0 < - a" using A by (rule less_le_trans)
   921     then show ?thesis by auto
   922   qed
   923 next
   924   assume A: "a \<le> 0" show "a \<le> - a"
   925   proof (rule order_trans)
   926     show "0 \<le> - a" using A by (simp add: minus_le_iff)
   927   next
   928     show "a \<le> 0" using A .
   929   qed
   930 qed
   931 
   932 lemma equal_neg_zero [simp]:
   933   "a = - a \<longleftrightarrow> a = 0"
   934 proof
   935   assume "a = 0" then show "a = - a" by simp
   936 next
   937   assume A: "a = - a" show "a = 0"
   938   proof (cases "0 \<le> a")
   939     case True with A have "0 \<le> - a" by auto
   940     with le_minus_iff have "a \<le> 0" by simp
   941     with True show ?thesis by (auto intro: order_trans)
   942   next
   943     case False then have B: "a \<le> 0" by auto
   944     with A have "- a \<le> 0" by auto
   945     with B show ?thesis by (auto intro: order_trans)
   946   qed
   947 qed
   948 
   949 lemma neg_equal_zero [simp]:
   950   "- a = a \<longleftrightarrow> a = 0"
   951   by (auto dest: sym)
   952 
   953 lemma double_zero [simp]:
   954   "a + a = 0 \<longleftrightarrow> a = 0"
   955 proof
   956   assume assm: "a + a = 0"
   957   then have a: "- a = a" by (rule minus_unique)
   958   then show "a = 0" by (simp only: neg_equal_zero)
   959 qed simp
   960 
   961 lemma double_zero_sym [simp]:
   962   "0 = a + a \<longleftrightarrow> a = 0"
   963   by (rule, drule sym) simp_all
   964 
   965 lemma zero_less_double_add_iff_zero_less_single_add [simp]:
   966   "0 < a + a \<longleftrightarrow> 0 < a"
   967 proof
   968   assume "0 < a + a"
   969   then have "0 - a < a" by (simp only: diff_less_eq)
   970   then have "- a < a" by simp
   971   then show "0 < a" by (simp only: neg_less_nonneg)
   972 next
   973   assume "0 < a"
   974   with this have "0 + 0 < a + a"
   975     by (rule add_strict_mono)
   976   then show "0 < a + a" by simp
   977 qed
   978 
   979 lemma zero_le_double_add_iff_zero_le_single_add [simp]:
   980   "0 \<le> a + a \<longleftrightarrow> 0 \<le> a"
   981   by (auto simp add: le_less)
   982 
   983 lemma double_add_less_zero_iff_single_add_less_zero [simp]:
   984   "a + a < 0 \<longleftrightarrow> a < 0"
   985 proof -
   986   have "\<not> a + a < 0 \<longleftrightarrow> \<not> a < 0"
   987     by (simp add: not_less)
   988   then show ?thesis by simp
   989 qed
   990 
   991 lemma double_add_le_zero_iff_single_add_le_zero [simp]:
   992   "a + a \<le> 0 \<longleftrightarrow> a \<le> 0" 
   993 proof -
   994   have "\<not> a + a \<le> 0 \<longleftrightarrow> \<not> a \<le> 0"
   995     by (simp add: not_le)
   996   then show ?thesis by simp
   997 qed
   998 
   999 lemma le_minus_self_iff:
  1000   "a \<le> - a \<longleftrightarrow> a \<le> 0"
  1001 proof -
  1002   from add_le_cancel_left [of "- a" "a + a" 0]
  1003   have "a \<le> - a \<longleftrightarrow> a + a \<le> 0" 
  1004     by (simp add: add_assoc [symmetric])
  1005   thus ?thesis by simp
  1006 qed
  1007 
  1008 lemma minus_le_self_iff:
  1009   "- a \<le> a \<longleftrightarrow> 0 \<le> a"
  1010 proof -
  1011   from add_le_cancel_left [of "- a" 0 "a + a"]
  1012   have "- a \<le> a \<longleftrightarrow> 0 \<le> a + a" 
  1013     by (simp add: add_assoc [symmetric])
  1014   thus ?thesis by simp
  1015 qed
  1016 
  1017 lemma minus_max_eq_min:
  1018   "- max x y = min (-x) (-y)"
  1019   by (auto simp add: max_def min_def)
  1020 
  1021 lemma minus_min_eq_max:
  1022   "- min x y = max (-x) (-y)"
  1023   by (auto simp add: max_def min_def)
  1024 
  1025 end
  1026 
  1027 context ordered_comm_monoid_add
  1028 begin
  1029 
  1030 lemma add_increasing:
  1031   "0 \<le> a \<Longrightarrow> b \<le> c \<Longrightarrow> b \<le> a + c"
  1032   by (insert add_mono [of 0 a b c], simp)
  1033 
  1034 lemma add_increasing2:
  1035   "0 \<le> c \<Longrightarrow> b \<le> a \<Longrightarrow> b \<le> a + c"
  1036   by (simp add: add_increasing add_commute [of a])
  1037 
  1038 lemma add_strict_increasing:
  1039   "0 < a \<Longrightarrow> b \<le> c \<Longrightarrow> b < a + c"
  1040   by (insert add_less_le_mono [of 0 a b c], simp)
  1041 
  1042 lemma add_strict_increasing2:
  1043   "0 \<le> a \<Longrightarrow> b < c \<Longrightarrow> b < a + c"
  1044   by (insert add_le_less_mono [of 0 a b c], simp)
  1045 
  1046 end
  1047 
  1048 class abs =
  1049   fixes abs :: "'a \<Rightarrow> 'a"
  1050 begin
  1051 
  1052 notation (xsymbols)
  1053   abs  ("\<bar>_\<bar>")
  1054 
  1055 notation (HTML output)
  1056   abs  ("\<bar>_\<bar>")
  1057 
  1058 end
  1059 
  1060 class sgn =
  1061   fixes sgn :: "'a \<Rightarrow> 'a"
  1062 
  1063 class abs_if = minus + uminus + ord + zero + abs +
  1064   assumes abs_if: "\<bar>a\<bar> = (if a < 0 then - a else a)"
  1065 
  1066 class sgn_if = minus + uminus + zero + one + ord + sgn +
  1067   assumes sgn_if: "sgn x = (if x = 0 then 0 else if 0 < x then 1 else - 1)"
  1068 begin
  1069 
  1070 lemma sgn0 [simp]: "sgn 0 = 0"
  1071   by (simp add:sgn_if)
  1072 
  1073 end
  1074 
  1075 class ordered_ab_group_add_abs = ordered_ab_group_add + abs +
  1076   assumes abs_ge_zero [simp]: "\<bar>a\<bar> \<ge> 0"
  1077     and abs_ge_self: "a \<le> \<bar>a\<bar>"
  1078     and abs_leI: "a \<le> b \<Longrightarrow> - a \<le> b \<Longrightarrow> \<bar>a\<bar> \<le> b"
  1079     and abs_minus_cancel [simp]: "\<bar>-a\<bar> = \<bar>a\<bar>"
  1080     and abs_triangle_ineq: "\<bar>a + b\<bar> \<le> \<bar>a\<bar> + \<bar>b\<bar>"
  1081 begin
  1082 
  1083 lemma abs_minus_le_zero: "- \<bar>a\<bar> \<le> 0"
  1084   unfolding neg_le_0_iff_le by simp
  1085 
  1086 lemma abs_of_nonneg [simp]:
  1087   assumes nonneg: "0 \<le> a" shows "\<bar>a\<bar> = a"
  1088 proof (rule antisym)
  1089   from nonneg le_imp_neg_le have "- a \<le> 0" by simp
  1090   from this nonneg have "- a \<le> a" by (rule order_trans)
  1091   then show "\<bar>a\<bar> \<le> a" by (auto intro: abs_leI)
  1092 qed (rule abs_ge_self)
  1093 
  1094 lemma abs_idempotent [simp]: "\<bar>\<bar>a\<bar>\<bar> = \<bar>a\<bar>"
  1095 by (rule antisym)
  1096    (auto intro!: abs_ge_self abs_leI order_trans [of "- \<bar>a\<bar>" 0 "\<bar>a\<bar>"])
  1097 
  1098 lemma abs_eq_0 [simp]: "\<bar>a\<bar> = 0 \<longleftrightarrow> a = 0"
  1099 proof -
  1100   have "\<bar>a\<bar> = 0 \<Longrightarrow> a = 0"
  1101   proof (rule antisym)
  1102     assume zero: "\<bar>a\<bar> = 0"
  1103     with abs_ge_self show "a \<le> 0" by auto
  1104     from zero have "\<bar>-a\<bar> = 0" by simp
  1105     with abs_ge_self [of "- a"] have "- a \<le> 0" by auto
  1106     with neg_le_0_iff_le show "0 \<le> a" by auto
  1107   qed
  1108   then show ?thesis by auto
  1109 qed
  1110 
  1111 lemma abs_zero [simp]: "\<bar>0\<bar> = 0"
  1112 by simp
  1113 
  1114 lemma abs_0_eq [simp, no_atp]: "0 = \<bar>a\<bar> \<longleftrightarrow> a = 0"
  1115 proof -
  1116   have "0 = \<bar>a\<bar> \<longleftrightarrow> \<bar>a\<bar> = 0" by (simp only: eq_ac)
  1117   thus ?thesis by simp
  1118 qed
  1119 
  1120 lemma abs_le_zero_iff [simp]: "\<bar>a\<bar> \<le> 0 \<longleftrightarrow> a = 0" 
  1121 proof
  1122   assume "\<bar>a\<bar> \<le> 0"
  1123   then have "\<bar>a\<bar> = 0" by (rule antisym) simp
  1124   thus "a = 0" by simp
  1125 next
  1126   assume "a = 0"
  1127   thus "\<bar>a\<bar> \<le> 0" by simp
  1128 qed
  1129 
  1130 lemma zero_less_abs_iff [simp]: "0 < \<bar>a\<bar> \<longleftrightarrow> a \<noteq> 0"
  1131 by (simp add: less_le)
  1132 
  1133 lemma abs_not_less_zero [simp]: "\<not> \<bar>a\<bar> < 0"
  1134 proof -
  1135   have a: "\<And>x y. x \<le> y \<Longrightarrow> \<not> y < x" by auto
  1136   show ?thesis by (simp add: a)
  1137 qed
  1138 
  1139 lemma abs_ge_minus_self: "- a \<le> \<bar>a\<bar>"
  1140 proof -
  1141   have "- a \<le> \<bar>-a\<bar>" by (rule abs_ge_self)
  1142   then show ?thesis by simp
  1143 qed
  1144 
  1145 lemma abs_minus_commute: 
  1146   "\<bar>a - b\<bar> = \<bar>b - a\<bar>"
  1147 proof -
  1148   have "\<bar>a - b\<bar> = \<bar>- (a - b)\<bar>" by (simp only: abs_minus_cancel)
  1149   also have "... = \<bar>b - a\<bar>" by simp
  1150   finally show ?thesis .
  1151 qed
  1152 
  1153 lemma abs_of_pos: "0 < a \<Longrightarrow> \<bar>a\<bar> = a"
  1154 by (rule abs_of_nonneg, rule less_imp_le)
  1155 
  1156 lemma abs_of_nonpos [simp]:
  1157   assumes "a \<le> 0" shows "\<bar>a\<bar> = - a"
  1158 proof -
  1159   let ?b = "- a"
  1160   have "- ?b \<le> 0 \<Longrightarrow> \<bar>- ?b\<bar> = - (- ?b)"
  1161   unfolding abs_minus_cancel [of "?b"]
  1162   unfolding neg_le_0_iff_le [of "?b"]
  1163   unfolding minus_minus by (erule abs_of_nonneg)
  1164   then show ?thesis using assms by auto
  1165 qed
  1166   
  1167 lemma abs_of_neg: "a < 0 \<Longrightarrow> \<bar>a\<bar> = - a"
  1168 by (rule abs_of_nonpos, rule less_imp_le)
  1169 
  1170 lemma abs_le_D1: "\<bar>a\<bar> \<le> b \<Longrightarrow> a \<le> b"
  1171 by (insert abs_ge_self, blast intro: order_trans)
  1172 
  1173 lemma abs_le_D2: "\<bar>a\<bar> \<le> b \<Longrightarrow> - a \<le> b"
  1174 by (insert abs_le_D1 [of "- a"], simp)
  1175 
  1176 lemma abs_le_iff: "\<bar>a\<bar> \<le> b \<longleftrightarrow> a \<le> b \<and> - a \<le> b"
  1177 by (blast intro: abs_leI dest: abs_le_D1 abs_le_D2)
  1178 
  1179 lemma abs_triangle_ineq2: "\<bar>a\<bar> - \<bar>b\<bar> \<le> \<bar>a - b\<bar>"
  1180 proof -
  1181   have "\<bar>a\<bar> = \<bar>b + (a - b)\<bar>"
  1182     by (simp add: algebra_simps add_diff_cancel)
  1183   then have "\<bar>a\<bar> \<le> \<bar>b\<bar> + \<bar>a - b\<bar>"
  1184     by (simp add: abs_triangle_ineq)
  1185   then show ?thesis
  1186     by (simp add: algebra_simps)
  1187 qed
  1188 
  1189 lemma abs_triangle_ineq2_sym: "\<bar>a\<bar> - \<bar>b\<bar> \<le> \<bar>b - a\<bar>"
  1190   by (simp only: abs_minus_commute [of b] abs_triangle_ineq2)
  1191 
  1192 lemma abs_triangle_ineq3: "\<bar>\<bar>a\<bar> - \<bar>b\<bar>\<bar> \<le> \<bar>a - b\<bar>"
  1193   by (simp add: abs_le_iff abs_triangle_ineq2 abs_triangle_ineq2_sym)
  1194 
  1195 lemma abs_triangle_ineq4: "\<bar>a - b\<bar> \<le> \<bar>a\<bar> + \<bar>b\<bar>"
  1196 proof -
  1197   have "\<bar>a - b\<bar> = \<bar>a + - b\<bar>" by (subst diff_minus, rule refl)
  1198   also have "... \<le> \<bar>a\<bar> + \<bar>- b\<bar>" by (rule abs_triangle_ineq)
  1199   finally show ?thesis by simp
  1200 qed
  1201 
  1202 lemma abs_diff_triangle_ineq: "\<bar>a + b - (c + d)\<bar> \<le> \<bar>a - c\<bar> + \<bar>b - d\<bar>"
  1203 proof -
  1204   have "\<bar>a + b - (c+d)\<bar> = \<bar>(a-c) + (b-d)\<bar>" by (simp add: diff_minus add_ac)
  1205   also have "... \<le> \<bar>a-c\<bar> + \<bar>b-d\<bar>" by (rule abs_triangle_ineq)
  1206   finally show ?thesis .
  1207 qed
  1208 
  1209 lemma abs_add_abs [simp]:
  1210   "\<bar>\<bar>a\<bar> + \<bar>b\<bar>\<bar> = \<bar>a\<bar> + \<bar>b\<bar>" (is "?L = ?R")
  1211 proof (rule antisym)
  1212   show "?L \<ge> ?R" by(rule abs_ge_self)
  1213 next
  1214   have "?L \<le> \<bar>\<bar>a\<bar>\<bar> + \<bar>\<bar>b\<bar>\<bar>" by(rule abs_triangle_ineq)
  1215   also have "\<dots> = ?R" by simp
  1216   finally show "?L \<le> ?R" .
  1217 qed
  1218 
  1219 end
  1220 
  1221 
  1222 subsection {* Tools setup *}
  1223 
  1224 lemma add_mono_thms_linordered_semiring [no_atp]:
  1225   fixes i j k :: "'a\<Colon>ordered_ab_semigroup_add"
  1226   shows "i \<le> j \<and> k \<le> l \<Longrightarrow> i + k \<le> j + l"
  1227     and "i = j \<and> k \<le> l \<Longrightarrow> i + k \<le> j + l"
  1228     and "i \<le> j \<and> k = l \<Longrightarrow> i + k \<le> j + l"
  1229     and "i = j \<and> k = l \<Longrightarrow> i + k = j + l"
  1230 by (rule add_mono, clarify+)+
  1231 
  1232 lemma add_mono_thms_linordered_field [no_atp]:
  1233   fixes i j k :: "'a\<Colon>ordered_cancel_ab_semigroup_add"
  1234   shows "i < j \<and> k = l \<Longrightarrow> i + k < j + l"
  1235     and "i = j \<and> k < l \<Longrightarrow> i + k < j + l"
  1236     and "i < j \<and> k \<le> l \<Longrightarrow> i + k < j + l"
  1237     and "i \<le> j \<and> k < l \<Longrightarrow> i + k < j + l"
  1238     and "i < j \<and> k < l \<Longrightarrow> i + k < j + l"
  1239 by (auto intro: add_strict_right_mono add_strict_left_mono
  1240   add_less_le_mono add_le_less_mono add_strict_mono)
  1241 
  1242 code_modulename SML
  1243   Groups Arith
  1244 
  1245 code_modulename OCaml
  1246   Groups Arith
  1247 
  1248 code_modulename Haskell
  1249   Groups Arith
  1250 
  1251 
  1252 text {* Legacy *}
  1253 
  1254 lemmas diff_def = diff_minus
  1255 
  1256 end