src/HOL/Groups.thy
author wenzelm
Wed Apr 06 13:33:46 2011 +0200 (2011-04-06)
changeset 42247 12fe41a92cd5
parent 42245 29e3967550d5
child 42248 04bffad68aa4
permissions -rw-r--r--
typed_print_translation: discontinued show_sorts argument;
     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   val name = "ac_simps"
    17   val description = "associativity and commutativity simplification rules"
    18 )
    19 *}
    20 
    21 setup Ac_Simps.setup
    22 
    23 text{* The rewrites accumulated in @{text algebra_simps} deal with the
    24 classical algebraic structures of groups, rings and family. They simplify
    25 terms by multiplying everything out (in case of a ring) and bringing sums and
    26 products into a canonical form (by ordered rewriting). As a result it decides
    27 group and ring equalities but also helps with inequalities.
    28 
    29 Of course it also works for fields, but it knows nothing about multiplicative
    30 inverses or division. This is catered for by @{text field_simps}. *}
    31 
    32 ML {*
    33 structure Algebra_Simps = Named_Thms(
    34   val name = "algebra_simps"
    35   val description = "algebra simplification rules"
    36 )
    37 *}
    38 
    39 setup Algebra_Simps.setup
    40 
    41 text{* Lemmas @{text field_simps} multiply with denominators in (in)equations
    42 if they can be proved to be non-zero (for equations) or positive/negative
    43 (for inequations). Can be too aggressive and is therefore separate from the
    44 more benign @{text algebra_simps}. *}
    45 
    46 ML {*
    47 structure Field_Simps = Named_Thms(
    48   val name = "field_simps"
    49   val description = "algebra simplification rules for fields"
    50 )
    51 *}
    52 
    53 setup Field_Simps.setup
    54 
    55 
    56 subsection {* Abstract structures *}
    57 
    58 text {*
    59   These locales provide basic structures for interpretation into
    60   bigger structures;  extensions require careful thinking, otherwise
    61   undesired effects may occur due to interpretation.
    62 *}
    63 
    64 locale semigroup =
    65   fixes f :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "*" 70)
    66   assumes assoc [ac_simps]: "a * b * c = a * (b * c)"
    67 
    68 locale abel_semigroup = semigroup +
    69   assumes commute [ac_simps]: "a * b = b * a"
    70 begin
    71 
    72 lemma left_commute [ac_simps]:
    73   "b * (a * c) = a * (b * c)"
    74 proof -
    75   have "(b * a) * c = (a * b) * c"
    76     by (simp only: commute)
    77   then show ?thesis
    78     by (simp only: assoc)
    79 qed
    80 
    81 end
    82 
    83 locale monoid = semigroup +
    84   fixes z :: 'a ("1")
    85   assumes left_neutral [simp]: "1 * a = a"
    86   assumes right_neutral [simp]: "a * 1 = a"
    87 
    88 locale comm_monoid = abel_semigroup +
    89   fixes z :: 'a ("1")
    90   assumes comm_neutral: "a * 1 = a"
    91 
    92 sublocale comm_monoid < monoid proof
    93 qed (simp_all add: commute comm_neutral)
    94 
    95 
    96 subsection {* Generic operations *}
    97 
    98 class zero = 
    99   fixes zero :: 'a  ("0")
   100 
   101 class one =
   102   fixes one  :: 'a  ("1")
   103 
   104 hide_const (open) zero one
   105 
   106 syntax
   107   "_index1"  :: index    ("\<^sub>1")
   108 translations
   109   (index) "\<^sub>1" => (index) "\<^bsub>\<struct>\<^esub>"
   110 
   111 lemma Let_0 [simp]: "Let 0 f = f 0"
   112   unfolding Let_def ..
   113 
   114 lemma Let_1 [simp]: "Let 1 f = f 1"
   115   unfolding Let_def ..
   116 
   117 setup {*
   118   Reorient_Proc.add
   119     (fn Const(@{const_name Groups.zero}, _) => true
   120       | Const(@{const_name Groups.one}, _) => true
   121       | _ => false)
   122 *}
   123 
   124 simproc_setup reorient_zero ("0 = x") = Reorient_Proc.proc
   125 simproc_setup reorient_one ("1 = x") = Reorient_Proc.proc
   126 
   127 typed_print_translation (advanced) {*
   128   let
   129     fun tr' c = (c, fn ctxt => fn T => fn ts =>
   130       if not (null ts) orelse T = dummyT
   131         orelse not (Config.get ctxt show_types) andalso can Term.dest_Type T
   132       then raise Match
   133       else Syntax.const Syntax.constrainC $ Syntax.const c $ 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 end
   413 
   414 class ab_group_add = minus + uminus + comm_monoid_add +
   415   assumes ab_left_minus: "- a + a = 0"
   416   assumes ab_diff_minus: "a - b = a + (- b)"
   417 begin
   418 
   419 subclass group_add
   420   proof qed (simp_all add: ab_left_minus ab_diff_minus)
   421 
   422 subclass cancel_comm_monoid_add
   423 proof
   424   fix a b c :: 'a
   425   assume "a + b = a + c"
   426   then have "- a + a + b = - a + a + c"
   427     unfolding add_assoc by simp
   428   then show "b = c" by simp
   429 qed
   430 
   431 lemma uminus_add_conv_diff[algebra_simps, field_simps]:
   432   "- a + b = b - a"
   433 by (simp add:diff_minus add_commute)
   434 
   435 lemma minus_add_distrib [simp]:
   436   "- (a + b) = - a + - b"
   437 by (rule minus_unique) (simp add: add_ac)
   438 
   439 lemma minus_diff_eq [simp]:
   440   "- (a - b) = b - a"
   441 by (simp add: diff_minus add_commute)
   442 
   443 lemma add_diff_eq[algebra_simps, field_simps]: "a + (b - c) = (a + b) - c"
   444 by (simp add: diff_minus add_ac)
   445 
   446 lemma diff_add_eq[algebra_simps, field_simps]: "(a - b) + c = (a + c) - b"
   447 by (simp add: diff_minus add_ac)
   448 
   449 lemma diff_eq_eq[algebra_simps, field_simps]: "a - b = c \<longleftrightarrow> a = c + b"
   450 by (auto simp add: diff_minus add_assoc)
   451 
   452 lemma eq_diff_eq[algebra_simps, field_simps]: "a = c - b \<longleftrightarrow> a + b = c"
   453 by (auto simp add: diff_minus add_assoc)
   454 
   455 lemma diff_diff_eq[algebra_simps, field_simps]: "(a - b) - c = a - (b + c)"
   456 by (simp add: diff_minus add_ac)
   457 
   458 lemma diff_diff_eq2[algebra_simps, field_simps]: "a - (b - c) = (a + c) - b"
   459 by (simp add: diff_minus add_ac)
   460 
   461 lemma eq_iff_diff_eq_0: "a = b \<longleftrightarrow> a - b = 0"
   462 by (simp add: algebra_simps)
   463 
   464 (* FIXME: duplicates right_minus_eq from class group_add *)
   465 (* but only this one is declared as a simp rule. *)
   466 lemma diff_eq_0_iff_eq [simp, no_atp]: "a - b = 0 \<longleftrightarrow> a = b"
   467 by (simp add: algebra_simps)
   468 
   469 lemma diff_eq_diff_eq:
   470   "a - b = c - d \<Longrightarrow> a = b \<longleftrightarrow> c = d"
   471   by (auto simp add: algebra_simps)
   472   
   473 end
   474 
   475 
   476 subsection {* (Partially) Ordered Groups *} 
   477 
   478 text {*
   479   The theory of partially ordered groups is taken from the books:
   480   \begin{itemize}
   481   \item \emph{Lattice Theory} by Garret Birkhoff, American Mathematical Society 1979 
   482   \item \emph{Partially Ordered Algebraic Systems}, Pergamon Press 1963
   483   \end{itemize}
   484   Most of the used notions can also be looked up in 
   485   \begin{itemize}
   486   \item \url{http://www.mathworld.com} by Eric Weisstein et. al.
   487   \item \emph{Algebra I} by van der Waerden, Springer.
   488   \end{itemize}
   489 *}
   490 
   491 class ordered_ab_semigroup_add = order + ab_semigroup_add +
   492   assumes add_left_mono: "a \<le> b \<Longrightarrow> c + a \<le> c + b"
   493 begin
   494 
   495 lemma add_right_mono:
   496   "a \<le> b \<Longrightarrow> a + c \<le> b + c"
   497 by (simp add: add_commute [of _ c] add_left_mono)
   498 
   499 text {* non-strict, in both arguments *}
   500 lemma add_mono:
   501   "a \<le> b \<Longrightarrow> c \<le> d \<Longrightarrow> a + c \<le> b + d"
   502   apply (erule add_right_mono [THEN order_trans])
   503   apply (simp add: add_commute add_left_mono)
   504   done
   505 
   506 end
   507 
   508 class ordered_cancel_ab_semigroup_add =
   509   ordered_ab_semigroup_add + cancel_ab_semigroup_add
   510 begin
   511 
   512 lemma add_strict_left_mono:
   513   "a < b \<Longrightarrow> c + a < c + b"
   514 by (auto simp add: less_le add_left_mono)
   515 
   516 lemma add_strict_right_mono:
   517   "a < b \<Longrightarrow> a + c < b + c"
   518 by (simp add: add_commute [of _ c] add_strict_left_mono)
   519 
   520 text{*Strict monotonicity in both arguments*}
   521 lemma add_strict_mono:
   522   "a < b \<Longrightarrow> c < d \<Longrightarrow> a + c < b + d"
   523 apply (erule add_strict_right_mono [THEN less_trans])
   524 apply (erule add_strict_left_mono)
   525 done
   526 
   527 lemma add_less_le_mono:
   528   "a < b \<Longrightarrow> c \<le> d \<Longrightarrow> a + c < b + d"
   529 apply (erule add_strict_right_mono [THEN less_le_trans])
   530 apply (erule add_left_mono)
   531 done
   532 
   533 lemma add_le_less_mono:
   534   "a \<le> b \<Longrightarrow> c < d \<Longrightarrow> a + c < b + d"
   535 apply (erule add_right_mono [THEN le_less_trans])
   536 apply (erule add_strict_left_mono) 
   537 done
   538 
   539 end
   540 
   541 class ordered_ab_semigroup_add_imp_le =
   542   ordered_cancel_ab_semigroup_add +
   543   assumes add_le_imp_le_left: "c + a \<le> c + b \<Longrightarrow> a \<le> b"
   544 begin
   545 
   546 lemma add_less_imp_less_left:
   547   assumes less: "c + a < c + b" shows "a < b"
   548 proof -
   549   from less have le: "c + a <= c + b" by (simp add: order_le_less)
   550   have "a <= b" 
   551     apply (insert le)
   552     apply (drule add_le_imp_le_left)
   553     by (insert le, drule add_le_imp_le_left, assumption)
   554   moreover have "a \<noteq> b"
   555   proof (rule ccontr)
   556     assume "~(a \<noteq> b)"
   557     then have "a = b" by simp
   558     then have "c + a = c + b" by simp
   559     with less show "False"by simp
   560   qed
   561   ultimately show "a < b" by (simp add: order_le_less)
   562 qed
   563 
   564 lemma add_less_imp_less_right:
   565   "a + c < b + c \<Longrightarrow> a < b"
   566 apply (rule add_less_imp_less_left [of c])
   567 apply (simp add: add_commute)  
   568 done
   569 
   570 lemma add_less_cancel_left [simp]:
   571   "c + a < c + b \<longleftrightarrow> a < b"
   572 by (blast intro: add_less_imp_less_left add_strict_left_mono) 
   573 
   574 lemma add_less_cancel_right [simp]:
   575   "a + c < b + c \<longleftrightarrow> a < b"
   576 by (blast intro: add_less_imp_less_right add_strict_right_mono)
   577 
   578 lemma add_le_cancel_left [simp]:
   579   "c + a \<le> c + b \<longleftrightarrow> a \<le> b"
   580 by (auto, drule add_le_imp_le_left, simp_all add: add_left_mono) 
   581 
   582 lemma add_le_cancel_right [simp]:
   583   "a + c \<le> b + c \<longleftrightarrow> a \<le> b"
   584 by (simp add: add_commute [of a c] add_commute [of b c])
   585 
   586 lemma add_le_imp_le_right:
   587   "a + c \<le> b + c \<Longrightarrow> a \<le> b"
   588 by simp
   589 
   590 lemma max_add_distrib_left:
   591   "max x y + z = max (x + z) (y + z)"
   592   unfolding max_def by auto
   593 
   594 lemma min_add_distrib_left:
   595   "min x y + z = min (x + z) (y + z)"
   596   unfolding min_def by auto
   597 
   598 end
   599 
   600 subsection {* Support for reasoning about signs *}
   601 
   602 class ordered_comm_monoid_add =
   603   ordered_cancel_ab_semigroup_add + comm_monoid_add
   604 begin
   605 
   606 lemma add_pos_nonneg:
   607   assumes "0 < a" and "0 \<le> b" shows "0 < a + b"
   608 proof -
   609   have "0 + 0 < a + b" 
   610     using assms by (rule add_less_le_mono)
   611   then show ?thesis by simp
   612 qed
   613 
   614 lemma add_pos_pos:
   615   assumes "0 < a" and "0 < b" shows "0 < a + b"
   616 by (rule add_pos_nonneg) (insert assms, auto)
   617 
   618 lemma add_nonneg_pos:
   619   assumes "0 \<le> a" and "0 < b" shows "0 < a + b"
   620 proof -
   621   have "0 + 0 < a + b" 
   622     using assms by (rule add_le_less_mono)
   623   then show ?thesis by simp
   624 qed
   625 
   626 lemma add_nonneg_nonneg [simp]:
   627   assumes "0 \<le> a" and "0 \<le> b" shows "0 \<le> a + b"
   628 proof -
   629   have "0 + 0 \<le> a + b" 
   630     using assms by (rule add_mono)
   631   then show ?thesis by simp
   632 qed
   633 
   634 lemma add_neg_nonpos:
   635   assumes "a < 0" and "b \<le> 0" shows "a + b < 0"
   636 proof -
   637   have "a + b < 0 + 0"
   638     using assms by (rule add_less_le_mono)
   639   then show ?thesis by simp
   640 qed
   641 
   642 lemma add_neg_neg: 
   643   assumes "a < 0" and "b < 0" shows "a + b < 0"
   644 by (rule add_neg_nonpos) (insert assms, auto)
   645 
   646 lemma add_nonpos_neg:
   647   assumes "a \<le> 0" and "b < 0" shows "a + b < 0"
   648 proof -
   649   have "a + b < 0 + 0"
   650     using assms by (rule add_le_less_mono)
   651   then show ?thesis by simp
   652 qed
   653 
   654 lemma add_nonpos_nonpos:
   655   assumes "a \<le> 0" and "b \<le> 0" shows "a + b \<le> 0"
   656 proof -
   657   have "a + b \<le> 0 + 0"
   658     using assms by (rule add_mono)
   659   then show ?thesis by simp
   660 qed
   661 
   662 lemmas add_sign_intros =
   663   add_pos_nonneg add_pos_pos add_nonneg_pos add_nonneg_nonneg
   664   add_neg_nonpos add_neg_neg add_nonpos_neg add_nonpos_nonpos
   665 
   666 lemma add_nonneg_eq_0_iff:
   667   assumes x: "0 \<le> x" and y: "0 \<le> y"
   668   shows "x + y = 0 \<longleftrightarrow> x = 0 \<and> y = 0"
   669 proof (intro iffI conjI)
   670   have "x = x + 0" by simp
   671   also have "x + 0 \<le> x + y" using y by (rule add_left_mono)
   672   also assume "x + y = 0"
   673   also have "0 \<le> x" using x .
   674   finally show "x = 0" .
   675 next
   676   have "y = 0 + y" by simp
   677   also have "0 + y \<le> x + y" using x by (rule add_right_mono)
   678   also assume "x + y = 0"
   679   also have "0 \<le> y" using y .
   680   finally show "y = 0" .
   681 next
   682   assume "x = 0 \<and> y = 0"
   683   then show "x + y = 0" by simp
   684 qed
   685 
   686 end
   687 
   688 class ordered_ab_group_add =
   689   ab_group_add + ordered_ab_semigroup_add
   690 begin
   691 
   692 subclass ordered_cancel_ab_semigroup_add ..
   693 
   694 subclass ordered_ab_semigroup_add_imp_le
   695 proof
   696   fix a b c :: 'a
   697   assume "c + a \<le> c + b"
   698   hence "(-c) + (c + a) \<le> (-c) + (c + b)" by (rule add_left_mono)
   699   hence "((-c) + c) + a \<le> ((-c) + c) + b" by (simp only: add_assoc)
   700   thus "a \<le> b" by simp
   701 qed
   702 
   703 subclass ordered_comm_monoid_add ..
   704 
   705 lemma max_diff_distrib_left:
   706   shows "max x y - z = max (x - z) (y - z)"
   707 by (simp add: diff_minus, rule max_add_distrib_left) 
   708 
   709 lemma min_diff_distrib_left:
   710   shows "min x y - z = min (x - z) (y - z)"
   711 by (simp add: diff_minus, rule min_add_distrib_left) 
   712 
   713 lemma le_imp_neg_le:
   714   assumes "a \<le> b" shows "-b \<le> -a"
   715 proof -
   716   have "-a+a \<le> -a+b" using `a \<le> b` by (rule add_left_mono) 
   717   hence "0 \<le> -a+b" by simp
   718   hence "0 + (-b) \<le> (-a + b) + (-b)" by (rule add_right_mono) 
   719   thus ?thesis by (simp add: add_assoc)
   720 qed
   721 
   722 lemma neg_le_iff_le [simp]: "- b \<le> - a \<longleftrightarrow> a \<le> b"
   723 proof 
   724   assume "- b \<le> - a"
   725   hence "- (- a) \<le> - (- b)" by (rule le_imp_neg_le)
   726   thus "a\<le>b" by simp
   727 next
   728   assume "a\<le>b"
   729   thus "-b \<le> -a" by (rule le_imp_neg_le)
   730 qed
   731 
   732 lemma neg_le_0_iff_le [simp]: "- a \<le> 0 \<longleftrightarrow> 0 \<le> a"
   733 by (subst neg_le_iff_le [symmetric], simp)
   734 
   735 lemma neg_0_le_iff_le [simp]: "0 \<le> - a \<longleftrightarrow> a \<le> 0"
   736 by (subst neg_le_iff_le [symmetric], simp)
   737 
   738 lemma neg_less_iff_less [simp]: "- b < - a \<longleftrightarrow> a < b"
   739 by (force simp add: less_le) 
   740 
   741 lemma neg_less_0_iff_less [simp]: "- a < 0 \<longleftrightarrow> 0 < a"
   742 by (subst neg_less_iff_less [symmetric], simp)
   743 
   744 lemma neg_0_less_iff_less [simp]: "0 < - a \<longleftrightarrow> a < 0"
   745 by (subst neg_less_iff_less [symmetric], simp)
   746 
   747 text{*The next several equations can make the simplifier loop!*}
   748 
   749 lemma less_minus_iff: "a < - b \<longleftrightarrow> b < - a"
   750 proof -
   751   have "(- (-a) < - b) = (b < - a)" by (rule neg_less_iff_less)
   752   thus ?thesis by simp
   753 qed
   754 
   755 lemma minus_less_iff: "- a < b \<longleftrightarrow> - b < a"
   756 proof -
   757   have "(- a < - (-b)) = (- b < a)" by (rule neg_less_iff_less)
   758   thus ?thesis by simp
   759 qed
   760 
   761 lemma le_minus_iff: "a \<le> - b \<longleftrightarrow> b \<le> - a"
   762 proof -
   763   have mm: "!! a (b::'a). (-(-a)) < -b \<Longrightarrow> -(-b) < -a" by (simp only: minus_less_iff)
   764   have "(- (- a) <= -b) = (b <= - a)" 
   765     apply (auto simp only: le_less)
   766     apply (drule mm)
   767     apply (simp_all)
   768     apply (drule mm[simplified], assumption)
   769     done
   770   then show ?thesis by simp
   771 qed
   772 
   773 lemma minus_le_iff: "- a \<le> b \<longleftrightarrow> - b \<le> a"
   774 by (auto simp add: le_less minus_less_iff)
   775 
   776 lemma diff_less_0_iff_less [simp, no_atp]:
   777   "a - b < 0 \<longleftrightarrow> a < b"
   778 proof -
   779   have "a - b < 0 \<longleftrightarrow> a + (- b) < b + (- b)" by (simp add: diff_minus)
   780   also have "... \<longleftrightarrow> a < b" by (simp only: add_less_cancel_right)
   781   finally show ?thesis .
   782 qed
   783 
   784 lemmas less_iff_diff_less_0 = diff_less_0_iff_less [symmetric]
   785 
   786 lemma diff_less_eq[algebra_simps, field_simps]: "a - b < c \<longleftrightarrow> a < c + b"
   787 apply (subst less_iff_diff_less_0 [of a])
   788 apply (rule less_iff_diff_less_0 [of _ c, THEN ssubst])
   789 apply (simp add: diff_minus add_ac)
   790 done
   791 
   792 lemma less_diff_eq[algebra_simps, field_simps]: "a < c - b \<longleftrightarrow> a + b < c"
   793 apply (subst less_iff_diff_less_0 [of "a + b"])
   794 apply (subst less_iff_diff_less_0 [of a])
   795 apply (simp add: diff_minus add_ac)
   796 done
   797 
   798 lemma diff_le_eq[algebra_simps, field_simps]: "a - b \<le> c \<longleftrightarrow> a \<le> c + b"
   799 by (auto simp add: le_less diff_less_eq diff_add_cancel add_diff_cancel)
   800 
   801 lemma le_diff_eq[algebra_simps, field_simps]: "a \<le> c - b \<longleftrightarrow> a + b \<le> c"
   802 by (auto simp add: le_less less_diff_eq diff_add_cancel add_diff_cancel)
   803 
   804 lemma diff_le_0_iff_le [simp, no_atp]:
   805   "a - b \<le> 0 \<longleftrightarrow> a \<le> b"
   806   by (simp add: algebra_simps)
   807 
   808 lemmas le_iff_diff_le_0 = diff_le_0_iff_le [symmetric]
   809 
   810 lemma diff_eq_diff_less:
   811   "a - b = c - d \<Longrightarrow> a < b \<longleftrightarrow> c < d"
   812   by (auto simp only: less_iff_diff_less_0 [of a b] less_iff_diff_less_0 [of c d])
   813 
   814 lemma diff_eq_diff_less_eq:
   815   "a - b = c - d \<Longrightarrow> a \<le> b \<longleftrightarrow> c \<le> d"
   816   by (auto simp only: le_iff_diff_le_0 [of a b] le_iff_diff_le_0 [of c d])
   817 
   818 end
   819 
   820 use "Tools/abel_cancel.ML"
   821 
   822 simproc_setup abel_cancel_sum
   823   ("a + b::'a::ab_group_add" | "a - b::'a::ab_group_add") =
   824   {* fn phi => Abel_Cancel.sum_proc *}
   825 
   826 simproc_setup abel_cancel_relation
   827   ("a < (b::'a::ordered_ab_group_add)" | "a \<le> (b::'a::ordered_ab_group_add)" | "c = (d::'b::ab_group_add)") =
   828   {* fn phi => Abel_Cancel.rel_proc *}
   829 
   830 class linordered_ab_semigroup_add =
   831   linorder + ordered_ab_semigroup_add
   832 
   833 class linordered_cancel_ab_semigroup_add =
   834   linorder + ordered_cancel_ab_semigroup_add
   835 begin
   836 
   837 subclass linordered_ab_semigroup_add ..
   838 
   839 subclass ordered_ab_semigroup_add_imp_le
   840 proof
   841   fix a b c :: 'a
   842   assume le: "c + a <= c + b"  
   843   show "a <= b"
   844   proof (rule ccontr)
   845     assume w: "~ a \<le> b"
   846     hence "b <= a" by (simp add: linorder_not_le)
   847     hence le2: "c + b <= c + a" by (rule add_left_mono)
   848     have "a = b" 
   849       apply (insert le)
   850       apply (insert le2)
   851       apply (drule antisym, simp_all)
   852       done
   853     with w show False 
   854       by (simp add: linorder_not_le [symmetric])
   855   qed
   856 qed
   857 
   858 end
   859 
   860 class linordered_ab_group_add = linorder + ordered_ab_group_add
   861 begin
   862 
   863 subclass linordered_cancel_ab_semigroup_add ..
   864 
   865 lemma neg_less_eq_nonneg [simp]:
   866   "- a \<le> a \<longleftrightarrow> 0 \<le> a"
   867 proof
   868   assume A: "- a \<le> a" show "0 \<le> a"
   869   proof (rule classical)
   870     assume "\<not> 0 \<le> a"
   871     then have "a < 0" by auto
   872     with A have "- a < 0" by (rule le_less_trans)
   873     then show ?thesis by auto
   874   qed
   875 next
   876   assume A: "0 \<le> a" show "- a \<le> a"
   877   proof (rule order_trans)
   878     show "- a \<le> 0" using A by (simp add: minus_le_iff)
   879   next
   880     show "0 \<le> a" using A .
   881   qed
   882 qed
   883 
   884 lemma neg_less_nonneg [simp]:
   885   "- a < a \<longleftrightarrow> 0 < a"
   886 proof
   887   assume A: "- a < a" show "0 < a"
   888   proof (rule classical)
   889     assume "\<not> 0 < a"
   890     then have "a \<le> 0" by auto
   891     with A have "- a < 0" by (rule less_le_trans)
   892     then show ?thesis by auto
   893   qed
   894 next
   895   assume A: "0 < a" show "- a < a"
   896   proof (rule less_trans)
   897     show "- a < 0" using A by (simp add: minus_le_iff)
   898   next
   899     show "0 < a" using A .
   900   qed
   901 qed
   902 
   903 lemma less_eq_neg_nonpos [simp]:
   904   "a \<le> - a \<longleftrightarrow> a \<le> 0"
   905 proof
   906   assume A: "a \<le> - a" show "a \<le> 0"
   907   proof (rule classical)
   908     assume "\<not> a \<le> 0"
   909     then have "0 < a" by auto
   910     then have "0 < - a" using A by (rule less_le_trans)
   911     then show ?thesis by auto
   912   qed
   913 next
   914   assume A: "a \<le> 0" show "a \<le> - a"
   915   proof (rule order_trans)
   916     show "0 \<le> - a" using A by (simp add: minus_le_iff)
   917   next
   918     show "a \<le> 0" using A .
   919   qed
   920 qed
   921 
   922 lemma equal_neg_zero [simp]:
   923   "a = - a \<longleftrightarrow> a = 0"
   924 proof
   925   assume "a = 0" then show "a = - a" by simp
   926 next
   927   assume A: "a = - a" show "a = 0"
   928   proof (cases "0 \<le> a")
   929     case True with A have "0 \<le> - a" by auto
   930     with le_minus_iff have "a \<le> 0" by simp
   931     with True show ?thesis by (auto intro: order_trans)
   932   next
   933     case False then have B: "a \<le> 0" by auto
   934     with A have "- a \<le> 0" by auto
   935     with B show ?thesis by (auto intro: order_trans)
   936   qed
   937 qed
   938 
   939 lemma neg_equal_zero [simp]:
   940   "- a = a \<longleftrightarrow> a = 0"
   941   by (auto dest: sym)
   942 
   943 lemma double_zero [simp]:
   944   "a + a = 0 \<longleftrightarrow> a = 0"
   945 proof
   946   assume assm: "a + a = 0"
   947   then have a: "- a = a" by (rule minus_unique)
   948   then show "a = 0" by (simp only: neg_equal_zero)
   949 qed simp
   950 
   951 lemma double_zero_sym [simp]:
   952   "0 = a + a \<longleftrightarrow> a = 0"
   953   by (rule, drule sym) simp_all
   954 
   955 lemma zero_less_double_add_iff_zero_less_single_add [simp]:
   956   "0 < a + a \<longleftrightarrow> 0 < a"
   957 proof
   958   assume "0 < a + a"
   959   then have "0 - a < a" by (simp only: diff_less_eq)
   960   then have "- a < a" by simp
   961   then show "0 < a" by (simp only: neg_less_nonneg)
   962 next
   963   assume "0 < a"
   964   with this have "0 + 0 < a + a"
   965     by (rule add_strict_mono)
   966   then show "0 < a + a" by simp
   967 qed
   968 
   969 lemma zero_le_double_add_iff_zero_le_single_add [simp]:
   970   "0 \<le> a + a \<longleftrightarrow> 0 \<le> a"
   971   by (auto simp add: le_less)
   972 
   973 lemma double_add_less_zero_iff_single_add_less_zero [simp]:
   974   "a + a < 0 \<longleftrightarrow> a < 0"
   975 proof -
   976   have "\<not> a + a < 0 \<longleftrightarrow> \<not> a < 0"
   977     by (simp add: not_less)
   978   then show ?thesis by simp
   979 qed
   980 
   981 lemma double_add_le_zero_iff_single_add_le_zero [simp]:
   982   "a + a \<le> 0 \<longleftrightarrow> a \<le> 0" 
   983 proof -
   984   have "\<not> a + a \<le> 0 \<longleftrightarrow> \<not> a \<le> 0"
   985     by (simp add: not_le)
   986   then show ?thesis by simp
   987 qed
   988 
   989 lemma le_minus_self_iff:
   990   "a \<le> - a \<longleftrightarrow> a \<le> 0"
   991 proof -
   992   from add_le_cancel_left [of "- a" "a + a" 0]
   993   have "a \<le> - a \<longleftrightarrow> a + a \<le> 0" 
   994     by (simp add: add_assoc [symmetric])
   995   thus ?thesis by simp
   996 qed
   997 
   998 lemma minus_le_self_iff:
   999   "- a \<le> a \<longleftrightarrow> 0 \<le> a"
  1000 proof -
  1001   from add_le_cancel_left [of "- a" 0 "a + a"]
  1002   have "- a \<le> a \<longleftrightarrow> 0 \<le> a + a" 
  1003     by (simp add: add_assoc [symmetric])
  1004   thus ?thesis by simp
  1005 qed
  1006 
  1007 lemma minus_max_eq_min:
  1008   "- max x y = min (-x) (-y)"
  1009   by (auto simp add: max_def min_def)
  1010 
  1011 lemma minus_min_eq_max:
  1012   "- min x y = max (-x) (-y)"
  1013   by (auto simp add: max_def min_def)
  1014 
  1015 end
  1016 
  1017 context ordered_comm_monoid_add
  1018 begin
  1019 
  1020 lemma add_increasing:
  1021   "0 \<le> a \<Longrightarrow> b \<le> c \<Longrightarrow> b \<le> a + c"
  1022   by (insert add_mono [of 0 a b c], simp)
  1023 
  1024 lemma add_increasing2:
  1025   "0 \<le> c \<Longrightarrow> b \<le> a \<Longrightarrow> b \<le> a + c"
  1026   by (simp add: add_increasing add_commute [of a])
  1027 
  1028 lemma add_strict_increasing:
  1029   "0 < a \<Longrightarrow> b \<le> c \<Longrightarrow> b < a + c"
  1030   by (insert add_less_le_mono [of 0 a b c], simp)
  1031 
  1032 lemma add_strict_increasing2:
  1033   "0 \<le> a \<Longrightarrow> b < c \<Longrightarrow> b < a + c"
  1034   by (insert add_le_less_mono [of 0 a b c], simp)
  1035 
  1036 end
  1037 
  1038 class abs =
  1039   fixes abs :: "'a \<Rightarrow> 'a"
  1040 begin
  1041 
  1042 notation (xsymbols)
  1043   abs  ("\<bar>_\<bar>")
  1044 
  1045 notation (HTML output)
  1046   abs  ("\<bar>_\<bar>")
  1047 
  1048 end
  1049 
  1050 class sgn =
  1051   fixes sgn :: "'a \<Rightarrow> 'a"
  1052 
  1053 class abs_if = minus + uminus + ord + zero + abs +
  1054   assumes abs_if: "\<bar>a\<bar> = (if a < 0 then - a else a)"
  1055 
  1056 class sgn_if = minus + uminus + zero + one + ord + sgn +
  1057   assumes sgn_if: "sgn x = (if x = 0 then 0 else if 0 < x then 1 else - 1)"
  1058 begin
  1059 
  1060 lemma sgn0 [simp]: "sgn 0 = 0"
  1061   by (simp add:sgn_if)
  1062 
  1063 end
  1064 
  1065 class ordered_ab_group_add_abs = ordered_ab_group_add + abs +
  1066   assumes abs_ge_zero [simp]: "\<bar>a\<bar> \<ge> 0"
  1067     and abs_ge_self: "a \<le> \<bar>a\<bar>"
  1068     and abs_leI: "a \<le> b \<Longrightarrow> - a \<le> b \<Longrightarrow> \<bar>a\<bar> \<le> b"
  1069     and abs_minus_cancel [simp]: "\<bar>-a\<bar> = \<bar>a\<bar>"
  1070     and abs_triangle_ineq: "\<bar>a + b\<bar> \<le> \<bar>a\<bar> + \<bar>b\<bar>"
  1071 begin
  1072 
  1073 lemma abs_minus_le_zero: "- \<bar>a\<bar> \<le> 0"
  1074   unfolding neg_le_0_iff_le by simp
  1075 
  1076 lemma abs_of_nonneg [simp]:
  1077   assumes nonneg: "0 \<le> a" shows "\<bar>a\<bar> = a"
  1078 proof (rule antisym)
  1079   from nonneg le_imp_neg_le have "- a \<le> 0" by simp
  1080   from this nonneg have "- a \<le> a" by (rule order_trans)
  1081   then show "\<bar>a\<bar> \<le> a" by (auto intro: abs_leI)
  1082 qed (rule abs_ge_self)
  1083 
  1084 lemma abs_idempotent [simp]: "\<bar>\<bar>a\<bar>\<bar> = \<bar>a\<bar>"
  1085 by (rule antisym)
  1086    (auto intro!: abs_ge_self abs_leI order_trans [of "- \<bar>a\<bar>" 0 "\<bar>a\<bar>"])
  1087 
  1088 lemma abs_eq_0 [simp]: "\<bar>a\<bar> = 0 \<longleftrightarrow> a = 0"
  1089 proof -
  1090   have "\<bar>a\<bar> = 0 \<Longrightarrow> a = 0"
  1091   proof (rule antisym)
  1092     assume zero: "\<bar>a\<bar> = 0"
  1093     with abs_ge_self show "a \<le> 0" by auto
  1094     from zero have "\<bar>-a\<bar> = 0" by simp
  1095     with abs_ge_self [of "- a"] have "- a \<le> 0" by auto
  1096     with neg_le_0_iff_le show "0 \<le> a" by auto
  1097   qed
  1098   then show ?thesis by auto
  1099 qed
  1100 
  1101 lemma abs_zero [simp]: "\<bar>0\<bar> = 0"
  1102 by simp
  1103 
  1104 lemma abs_0_eq [simp, no_atp]: "0 = \<bar>a\<bar> \<longleftrightarrow> a = 0"
  1105 proof -
  1106   have "0 = \<bar>a\<bar> \<longleftrightarrow> \<bar>a\<bar> = 0" by (simp only: eq_ac)
  1107   thus ?thesis by simp
  1108 qed
  1109 
  1110 lemma abs_le_zero_iff [simp]: "\<bar>a\<bar> \<le> 0 \<longleftrightarrow> a = 0" 
  1111 proof
  1112   assume "\<bar>a\<bar> \<le> 0"
  1113   then have "\<bar>a\<bar> = 0" by (rule antisym) simp
  1114   thus "a = 0" by simp
  1115 next
  1116   assume "a = 0"
  1117   thus "\<bar>a\<bar> \<le> 0" by simp
  1118 qed
  1119 
  1120 lemma zero_less_abs_iff [simp]: "0 < \<bar>a\<bar> \<longleftrightarrow> a \<noteq> 0"
  1121 by (simp add: less_le)
  1122 
  1123 lemma abs_not_less_zero [simp]: "\<not> \<bar>a\<bar> < 0"
  1124 proof -
  1125   have a: "\<And>x y. x \<le> y \<Longrightarrow> \<not> y < x" by auto
  1126   show ?thesis by (simp add: a)
  1127 qed
  1128 
  1129 lemma abs_ge_minus_self: "- a \<le> \<bar>a\<bar>"
  1130 proof -
  1131   have "- a \<le> \<bar>-a\<bar>" by (rule abs_ge_self)
  1132   then show ?thesis by simp
  1133 qed
  1134 
  1135 lemma abs_minus_commute: 
  1136   "\<bar>a - b\<bar> = \<bar>b - a\<bar>"
  1137 proof -
  1138   have "\<bar>a - b\<bar> = \<bar>- (a - b)\<bar>" by (simp only: abs_minus_cancel)
  1139   also have "... = \<bar>b - a\<bar>" by simp
  1140   finally show ?thesis .
  1141 qed
  1142 
  1143 lemma abs_of_pos: "0 < a \<Longrightarrow> \<bar>a\<bar> = a"
  1144 by (rule abs_of_nonneg, rule less_imp_le)
  1145 
  1146 lemma abs_of_nonpos [simp]:
  1147   assumes "a \<le> 0" shows "\<bar>a\<bar> = - a"
  1148 proof -
  1149   let ?b = "- a"
  1150   have "- ?b \<le> 0 \<Longrightarrow> \<bar>- ?b\<bar> = - (- ?b)"
  1151   unfolding abs_minus_cancel [of "?b"]
  1152   unfolding neg_le_0_iff_le [of "?b"]
  1153   unfolding minus_minus by (erule abs_of_nonneg)
  1154   then show ?thesis using assms by auto
  1155 qed
  1156   
  1157 lemma abs_of_neg: "a < 0 \<Longrightarrow> \<bar>a\<bar> = - a"
  1158 by (rule abs_of_nonpos, rule less_imp_le)
  1159 
  1160 lemma abs_le_D1: "\<bar>a\<bar> \<le> b \<Longrightarrow> a \<le> b"
  1161 by (insert abs_ge_self, blast intro: order_trans)
  1162 
  1163 lemma abs_le_D2: "\<bar>a\<bar> \<le> b \<Longrightarrow> - a \<le> b"
  1164 by (insert abs_le_D1 [of "- a"], simp)
  1165 
  1166 lemma abs_le_iff: "\<bar>a\<bar> \<le> b \<longleftrightarrow> a \<le> b \<and> - a \<le> b"
  1167 by (blast intro: abs_leI dest: abs_le_D1 abs_le_D2)
  1168 
  1169 lemma abs_triangle_ineq2: "\<bar>a\<bar> - \<bar>b\<bar> \<le> \<bar>a - b\<bar>"
  1170 proof -
  1171   have "\<bar>a\<bar> = \<bar>b + (a - b)\<bar>"
  1172     by (simp add: algebra_simps add_diff_cancel)
  1173   then have "\<bar>a\<bar> \<le> \<bar>b\<bar> + \<bar>a - b\<bar>"
  1174     by (simp add: abs_triangle_ineq)
  1175   then show ?thesis
  1176     by (simp add: algebra_simps)
  1177 qed
  1178 
  1179 lemma abs_triangle_ineq2_sym: "\<bar>a\<bar> - \<bar>b\<bar> \<le> \<bar>b - a\<bar>"
  1180   by (simp only: abs_minus_commute [of b] abs_triangle_ineq2)
  1181 
  1182 lemma abs_triangle_ineq3: "\<bar>\<bar>a\<bar> - \<bar>b\<bar>\<bar> \<le> \<bar>a - b\<bar>"
  1183   by (simp add: abs_le_iff abs_triangle_ineq2 abs_triangle_ineq2_sym)
  1184 
  1185 lemma abs_triangle_ineq4: "\<bar>a - b\<bar> \<le> \<bar>a\<bar> + \<bar>b\<bar>"
  1186 proof -
  1187   have "\<bar>a - b\<bar> = \<bar>a + - b\<bar>" by (subst diff_minus, rule refl)
  1188   also have "... \<le> \<bar>a\<bar> + \<bar>- b\<bar>" by (rule abs_triangle_ineq)
  1189   finally show ?thesis by simp
  1190 qed
  1191 
  1192 lemma abs_diff_triangle_ineq: "\<bar>a + b - (c + d)\<bar> \<le> \<bar>a - c\<bar> + \<bar>b - d\<bar>"
  1193 proof -
  1194   have "\<bar>a + b - (c+d)\<bar> = \<bar>(a-c) + (b-d)\<bar>" by (simp add: diff_minus add_ac)
  1195   also have "... \<le> \<bar>a-c\<bar> + \<bar>b-d\<bar>" by (rule abs_triangle_ineq)
  1196   finally show ?thesis .
  1197 qed
  1198 
  1199 lemma abs_add_abs [simp]:
  1200   "\<bar>\<bar>a\<bar> + \<bar>b\<bar>\<bar> = \<bar>a\<bar> + \<bar>b\<bar>" (is "?L = ?R")
  1201 proof (rule antisym)
  1202   show "?L \<ge> ?R" by(rule abs_ge_self)
  1203 next
  1204   have "?L \<le> \<bar>\<bar>a\<bar>\<bar> + \<bar>\<bar>b\<bar>\<bar>" by(rule abs_triangle_ineq)
  1205   also have "\<dots> = ?R" by simp
  1206   finally show "?L \<le> ?R" .
  1207 qed
  1208 
  1209 end
  1210 
  1211 
  1212 subsection {* Tools setup *}
  1213 
  1214 lemma add_mono_thms_linordered_semiring [no_atp]:
  1215   fixes i j k :: "'a\<Colon>ordered_ab_semigroup_add"
  1216   shows "i \<le> j \<and> k \<le> l \<Longrightarrow> i + k \<le> j + l"
  1217     and "i = j \<and> k \<le> l \<Longrightarrow> i + k \<le> j + l"
  1218     and "i \<le> j \<and> k = l \<Longrightarrow> i + k \<le> j + l"
  1219     and "i = j \<and> k = l \<Longrightarrow> i + k = j + l"
  1220 by (rule add_mono, clarify+)+
  1221 
  1222 lemma add_mono_thms_linordered_field [no_atp]:
  1223   fixes i j k :: "'a\<Colon>ordered_cancel_ab_semigroup_add"
  1224   shows "i < j \<and> k = l \<Longrightarrow> i + k < j + l"
  1225     and "i = j \<and> k < l \<Longrightarrow> i + k < j + l"
  1226     and "i < j \<and> k \<le> l \<Longrightarrow> i + k < j + l"
  1227     and "i \<le> j \<and> k < l \<Longrightarrow> i + k < j + l"
  1228     and "i < j \<and> k < l \<Longrightarrow> i + k < j + l"
  1229 by (auto intro: add_strict_right_mono add_strict_left_mono
  1230   add_less_le_mono add_le_less_mono add_strict_mono)
  1231 
  1232 code_modulename SML
  1233   Groups Arith
  1234 
  1235 code_modulename OCaml
  1236   Groups Arith
  1237 
  1238 code_modulename Haskell
  1239   Groups Arith
  1240 
  1241 
  1242 text {* Legacy *}
  1243 
  1244 lemmas diff_def = diff_minus
  1245 
  1246 end