src/HOL/Groups.thy
author wenzelm
Wed Aug 22 22:55:41 2012 +0200 (2012-08-22)
changeset 48891 c0eafbd55de3
parent 48556 62a3fbf9d35b
child 49388 1ffd5a055acf
permissions -rw-r--r--
prefer ML_file over old uses;
     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 begin
    10 
    11 subsection {* Fact collections *}
    12 
    13 ML {*
    14 structure Ac_Simps = Named_Thms
    15 (
    16   val name = @{binding 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 (
    35   val name = @{binding algebra_simps}
    36   val description = "algebra simplification rules"
    37 )
    38 *}
    39 
    40 setup Algebra_Simps.setup
    41 
    42 text{* Lemmas @{text field_simps} multiply with denominators in (in)equations
    43 if they can be proved to be non-zero (for equations) or positive/negative
    44 (for inequations). Can be too aggressive and is therefore separate from the
    45 more benign @{text algebra_simps}. *}
    46 
    47 ML {*
    48 structure Field_Simps = Named_Thms
    49 (
    50   val name = @{binding field_simps}
    51   val description = "algebra simplification rules for fields"
    52 )
    53 *}
    54 
    55 setup Field_Simps.setup
    56 
    57 
    58 subsection {* Abstract structures *}
    59 
    60 text {*
    61   These locales provide basic structures for interpretation into
    62   bigger structures;  extensions require careful thinking, otherwise
    63   undesired effects may occur due to interpretation.
    64 *}
    65 
    66 locale semigroup =
    67   fixes f :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "*" 70)
    68   assumes assoc [ac_simps]: "a * b * c = a * (b * c)"
    69 
    70 locale abel_semigroup = semigroup +
    71   assumes commute [ac_simps]: "a * b = b * a"
    72 begin
    73 
    74 lemma left_commute [ac_simps]:
    75   "b * (a * c) = a * (b * c)"
    76 proof -
    77   have "(b * a) * c = (a * b) * c"
    78     by (simp only: commute)
    79   then show ?thesis
    80     by (simp only: assoc)
    81 qed
    82 
    83 end
    84 
    85 locale monoid = semigroup +
    86   fixes z :: 'a ("1")
    87   assumes left_neutral [simp]: "1 * a = a"
    88   assumes right_neutral [simp]: "a * 1 = a"
    89 
    90 locale comm_monoid = abel_semigroup +
    91   fixes z :: 'a ("1")
    92   assumes comm_neutral: "a * 1 = a"
    93 
    94 sublocale comm_monoid < monoid proof
    95 qed (simp_all add: commute comm_neutral)
    96 
    97 
    98 subsection {* Generic operations *}
    99 
   100 class zero = 
   101   fixes zero :: 'a  ("0")
   102 
   103 class one =
   104   fixes one  :: 'a  ("1")
   105 
   106 hide_const (open) zero one
   107 
   108 lemma Let_0 [simp]: "Let 0 f = f 0"
   109   unfolding Let_def ..
   110 
   111 lemma Let_1 [simp]: "Let 1 f = f 1"
   112   unfolding Let_def ..
   113 
   114 setup {*
   115   Reorient_Proc.add
   116     (fn Const(@{const_name Groups.zero}, _) => true
   117       | Const(@{const_name Groups.one}, _) => true
   118       | _ => false)
   119 *}
   120 
   121 simproc_setup reorient_zero ("0 = x") = Reorient_Proc.proc
   122 simproc_setup reorient_one ("1 = x") = Reorient_Proc.proc
   123 
   124 typed_print_translation (advanced) {*
   125   let
   126     fun tr' c = (c, fn ctxt => fn T => fn ts =>
   127       if not (null ts) orelse T = dummyT
   128         orelse not (Config.get ctxt show_types) andalso can Term.dest_Type T
   129       then raise Match
   130       else
   131         Syntax.const @{syntax_const "_constrain"} $ Syntax.const c $
   132           Syntax_Phases.term_of_typ ctxt T);
   133   in map tr' [@{const_syntax Groups.one}, @{const_syntax Groups.zero}] end;
   134 *} -- {* show types that are presumably too general *}
   135 
   136 class plus =
   137   fixes plus :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "+" 65)
   138 
   139 class minus =
   140   fixes minus :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "-" 65)
   141 
   142 class uminus =
   143   fixes uminus :: "'a \<Rightarrow> 'a"  ("- _" [81] 80)
   144 
   145 class times =
   146   fixes times :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "*" 70)
   147 
   148 
   149 subsection {* Semigroups and Monoids *}
   150 
   151 class semigroup_add = plus +
   152   assumes add_assoc [algebra_simps, field_simps]: "(a + b) + c = a + (b + c)"
   153 
   154 sublocale semigroup_add < add!: semigroup plus proof
   155 qed (fact add_assoc)
   156 
   157 class ab_semigroup_add = semigroup_add +
   158   assumes add_commute [algebra_simps, field_simps]: "a + b = b + a"
   159 
   160 sublocale ab_semigroup_add < add!: abel_semigroup plus proof
   161 qed (fact add_commute)
   162 
   163 context ab_semigroup_add
   164 begin
   165 
   166 lemmas add_left_commute [algebra_simps, field_simps] = add.left_commute
   167 
   168 theorems add_ac = add_assoc add_commute add_left_commute
   169 
   170 end
   171 
   172 theorems add_ac = add_assoc add_commute add_left_commute
   173 
   174 class semigroup_mult = times +
   175   assumes mult_assoc [algebra_simps, field_simps]: "(a * b) * c = a * (b * c)"
   176 
   177 sublocale semigroup_mult < mult!: semigroup times proof
   178 qed (fact mult_assoc)
   179 
   180 class ab_semigroup_mult = semigroup_mult +
   181   assumes mult_commute [algebra_simps, field_simps]: "a * b = b * a"
   182 
   183 sublocale ab_semigroup_mult < mult!: abel_semigroup times proof
   184 qed (fact mult_commute)
   185 
   186 context ab_semigroup_mult
   187 begin
   188 
   189 lemmas mult_left_commute [algebra_simps, field_simps] = mult.left_commute
   190 
   191 theorems mult_ac = mult_assoc mult_commute mult_left_commute
   192 
   193 end
   194 
   195 theorems mult_ac = mult_assoc mult_commute mult_left_commute
   196 
   197 class monoid_add = zero + semigroup_add +
   198   assumes add_0_left: "0 + a = a"
   199     and add_0_right: "a + 0 = a"
   200 
   201 sublocale monoid_add < add!: monoid plus 0 proof
   202 qed (fact add_0_left add_0_right)+
   203 
   204 lemma zero_reorient: "0 = x \<longleftrightarrow> x = 0"
   205 by (rule eq_commute)
   206 
   207 class comm_monoid_add = zero + ab_semigroup_add +
   208   assumes add_0: "0 + a = a"
   209 
   210 sublocale comm_monoid_add < add!: comm_monoid plus 0 proof
   211 qed (insert add_0, simp add: ac_simps)
   212 
   213 subclass (in comm_monoid_add) monoid_add proof
   214 qed (fact add.left_neutral add.right_neutral)+
   215 
   216 class monoid_mult = one + semigroup_mult +
   217   assumes mult_1_left: "1 * a  = a"
   218     and mult_1_right: "a * 1 = a"
   219 
   220 sublocale monoid_mult < mult!: monoid times 1 proof
   221 qed (fact mult_1_left mult_1_right)+
   222 
   223 lemma one_reorient: "1 = x \<longleftrightarrow> x = 1"
   224 by (rule eq_commute)
   225 
   226 class comm_monoid_mult = one + ab_semigroup_mult +
   227   assumes mult_1: "1 * a = a"
   228 
   229 sublocale comm_monoid_mult < mult!: comm_monoid times 1 proof
   230 qed (insert mult_1, simp add: ac_simps)
   231 
   232 subclass (in comm_monoid_mult) monoid_mult proof
   233 qed (fact mult.left_neutral mult.right_neutral)+
   234 
   235 class cancel_semigroup_add = semigroup_add +
   236   assumes add_left_imp_eq: "a + b = a + c \<Longrightarrow> b = c"
   237   assumes add_right_imp_eq: "b + a = c + a \<Longrightarrow> b = c"
   238 begin
   239 
   240 lemma add_left_cancel [simp]:
   241   "a + b = a + c \<longleftrightarrow> b = c"
   242 by (blast dest: add_left_imp_eq)
   243 
   244 lemma add_right_cancel [simp]:
   245   "b + a = c + a \<longleftrightarrow> b = c"
   246 by (blast dest: add_right_imp_eq)
   247 
   248 end
   249 
   250 class cancel_ab_semigroup_add = ab_semigroup_add +
   251   assumes add_imp_eq: "a + b = a + c \<Longrightarrow> b = c"
   252 begin
   253 
   254 subclass cancel_semigroup_add
   255 proof
   256   fix a b c :: 'a
   257   assume "a + b = a + c" 
   258   then show "b = c" by (rule add_imp_eq)
   259 next
   260   fix a b c :: 'a
   261   assume "b + a = c + a"
   262   then have "a + b = a + c" by (simp only: add_commute)
   263   then show "b = c" by (rule add_imp_eq)
   264 qed
   265 
   266 end
   267 
   268 class cancel_comm_monoid_add = cancel_ab_semigroup_add + comm_monoid_add
   269 
   270 
   271 subsection {* Groups *}
   272 
   273 class group_add = minus + uminus + monoid_add +
   274   assumes left_minus [simp]: "- a + a = 0"
   275   assumes diff_minus: "a - b = a + (- b)"
   276 begin
   277 
   278 lemma minus_unique:
   279   assumes "a + b = 0" shows "- a = b"
   280 proof -
   281   have "- a = - a + (a + b)" using assms by simp
   282   also have "\<dots> = b" by (simp add: add_assoc [symmetric])
   283   finally show ?thesis .
   284 qed
   285 
   286 lemmas equals_zero_I = minus_unique (* legacy name *)
   287 
   288 lemma minus_zero [simp]: "- 0 = 0"
   289 proof -
   290   have "0 + 0 = 0" by (rule add_0_right)
   291   thus "- 0 = 0" by (rule minus_unique)
   292 qed
   293 
   294 lemma minus_minus [simp]: "- (- a) = a"
   295 proof -
   296   have "- a + a = 0" by (rule left_minus)
   297   thus "- (- a) = a" by (rule minus_unique)
   298 qed
   299 
   300 lemma right_minus [simp]: "a + - a = 0"
   301 proof -
   302   have "a + - a = - (- a) + - a" by simp
   303   also have "\<dots> = 0" by (rule left_minus)
   304   finally show ?thesis .
   305 qed
   306 
   307 subclass cancel_semigroup_add
   308 proof
   309   fix a b c :: 'a
   310   assume "a + b = a + c"
   311   then have "- a + a + b = - a + a + c"
   312     unfolding add_assoc by simp
   313   then show "b = c" by simp
   314 next
   315   fix a b c :: 'a
   316   assume "b + a = c + a"
   317   then have "b + a + - a = c + a  + - a" by simp
   318   then show "b = c" unfolding add_assoc by simp
   319 qed
   320 
   321 lemma minus_add_cancel: "- a + (a + b) = b"
   322 by (simp add: add_assoc [symmetric])
   323 
   324 lemma add_minus_cancel: "a + (- a + b) = b"
   325 by (simp add: add_assoc [symmetric])
   326 
   327 lemma minus_add: "- (a + b) = - b + - a"
   328 proof -
   329   have "(a + b) + (- b + - a) = 0"
   330     by (simp add: add_assoc add_minus_cancel)
   331   thus "- (a + b) = - b + - a"
   332     by (rule minus_unique)
   333 qed
   334 
   335 lemma right_minus_eq: "a - b = 0 \<longleftrightarrow> a = b"
   336 proof
   337   assume "a - b = 0"
   338   have "a = (a - b) + b" by (simp add:diff_minus add_assoc)
   339   also have "\<dots> = b" using `a - b = 0` by simp
   340   finally show "a = b" .
   341 next
   342   assume "a = b" thus "a - b = 0" by (simp add: diff_minus)
   343 qed
   344 
   345 lemma diff_self [simp]: "a - a = 0"
   346 by (simp add: diff_minus)
   347 
   348 lemma diff_0 [simp]: "0 - a = - a"
   349 by (simp add: diff_minus)
   350 
   351 lemma diff_0_right [simp]: "a - 0 = a" 
   352 by (simp add: diff_minus)
   353 
   354 lemma diff_minus_eq_add [simp]: "a - - b = a + b"
   355 by (simp add: diff_minus)
   356 
   357 lemma neg_equal_iff_equal [simp]:
   358   "- a = - b \<longleftrightarrow> a = b" 
   359 proof 
   360   assume "- a = - b"
   361   hence "- (- a) = - (- b)" by simp
   362   thus "a = b" by simp
   363 next
   364   assume "a = b"
   365   thus "- a = - b" by simp
   366 qed
   367 
   368 lemma neg_equal_0_iff_equal [simp]:
   369   "- a = 0 \<longleftrightarrow> a = 0"
   370 by (subst neg_equal_iff_equal [symmetric], simp)
   371 
   372 lemma neg_0_equal_iff_equal [simp]:
   373   "0 = - a \<longleftrightarrow> 0 = a"
   374 by (subst neg_equal_iff_equal [symmetric], simp)
   375 
   376 text{*The next two equations can make the simplifier loop!*}
   377 
   378 lemma equation_minus_iff:
   379   "a = - b \<longleftrightarrow> b = - a"
   380 proof -
   381   have "- (- a) = - b \<longleftrightarrow> - a = b" by (rule neg_equal_iff_equal)
   382   thus ?thesis by (simp add: eq_commute)
   383 qed
   384 
   385 lemma minus_equation_iff:
   386   "- a = b \<longleftrightarrow> - b = a"
   387 proof -
   388   have "- a = - (- b) \<longleftrightarrow> a = -b" by (rule neg_equal_iff_equal)
   389   thus ?thesis by (simp add: eq_commute)
   390 qed
   391 
   392 lemma diff_add_cancel: "a - b + b = a"
   393 by (simp add: diff_minus add_assoc)
   394 
   395 lemma add_diff_cancel: "a + b - b = a"
   396 by (simp add: diff_minus add_assoc)
   397 
   398 declare diff_minus[symmetric, algebra_simps, field_simps]
   399 
   400 lemma eq_neg_iff_add_eq_0: "a = - b \<longleftrightarrow> a + b = 0"
   401 proof
   402   assume "a = - b" then show "a + b = 0" by simp
   403 next
   404   assume "a + b = 0"
   405   moreover have "a + (b + - b) = (a + b) + - b"
   406     by (simp only: add_assoc)
   407   ultimately show "a = - b" by simp
   408 qed
   409 
   410 lemma add_eq_0_iff: "x + y = 0 \<longleftrightarrow> y = - x"
   411   unfolding eq_neg_iff_add_eq_0 [symmetric]
   412   by (rule equation_minus_iff)
   413 
   414 lemma minus_diff_eq [simp]: "- (a - b) = b - a"
   415   by (simp add: diff_minus minus_add)
   416 
   417 lemma add_diff_eq[algebra_simps, field_simps]: "a + (b - c) = (a + b) - c"
   418   by (simp add: diff_minus add_assoc)
   419 
   420 lemma diff_eq_eq[algebra_simps, field_simps]: "a - b = c \<longleftrightarrow> a = c + b"
   421   by (auto simp add: diff_minus add_assoc)
   422 
   423 lemma eq_diff_eq[algebra_simps, field_simps]: "a = c - b \<longleftrightarrow> a + b = c"
   424   by (auto simp add: diff_minus add_assoc)
   425 
   426 lemma diff_diff_eq2[algebra_simps, field_simps]: "a - (b - c) = (a + c) - b"
   427   by (simp add: diff_minus minus_add add_assoc)
   428 
   429 lemma eq_iff_diff_eq_0: "a = b \<longleftrightarrow> a - b = 0"
   430   by (fact right_minus_eq [symmetric])
   431 
   432 lemma diff_eq_diff_eq:
   433   "a - b = c - d \<Longrightarrow> a = b \<longleftrightarrow> c = d"
   434   by (simp add: eq_iff_diff_eq_0 [of a b] eq_iff_diff_eq_0 [of c d])
   435 
   436 end
   437 
   438 class ab_group_add = minus + uminus + comm_monoid_add +
   439   assumes ab_left_minus: "- a + a = 0"
   440   assumes ab_diff_minus: "a - b = a + (- b)"
   441 begin
   442 
   443 subclass group_add
   444   proof qed (simp_all add: ab_left_minus ab_diff_minus)
   445 
   446 subclass cancel_comm_monoid_add
   447 proof
   448   fix a b c :: 'a
   449   assume "a + b = a + c"
   450   then have "- a + a + b = - a + a + c"
   451     unfolding add_assoc by simp
   452   then show "b = c" by simp
   453 qed
   454 
   455 lemma uminus_add_conv_diff[algebra_simps, field_simps]:
   456   "- a + b = b - a"
   457 by (simp add:diff_minus add_commute)
   458 
   459 lemma minus_add_distrib [simp]:
   460   "- (a + b) = - a + - b"
   461 by (rule minus_unique) (simp add: add_ac)
   462 
   463 lemma diff_add_eq[algebra_simps, field_simps]: "(a - b) + c = (a + c) - b"
   464 by (simp add: diff_minus add_ac)
   465 
   466 lemma diff_diff_eq[algebra_simps, field_simps]: "(a - b) - c = a - (b + c)"
   467 by (simp add: diff_minus add_ac)
   468 
   469 (* FIXME: duplicates right_minus_eq from class group_add *)
   470 (* but only this one is declared as a simp rule. *)
   471 lemma diff_eq_0_iff_eq [simp, no_atp]: "a - b = 0 \<longleftrightarrow> a = b"
   472   by (rule right_minus_eq)
   473 
   474 lemma add_diff_cancel_left: "(c + a) - (c + b) = a - b"
   475   by (simp add: diff_minus add_ac)
   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 ML_file "Tools/group_cancel.ML"
   833 
   834 simproc_setup group_cancel_add ("a + b::'a::ab_group_add") =
   835   {* fn phi => fn ss => try Group_Cancel.cancel_add_conv *}
   836 
   837 simproc_setup group_cancel_diff ("a - b::'a::ab_group_add") =
   838   {* fn phi => fn ss => try Group_Cancel.cancel_diff_conv *}
   839 
   840 simproc_setup group_cancel_eq ("a = (b::'a::ab_group_add)") =
   841   {* fn phi => fn ss => try Group_Cancel.cancel_eq_conv *}
   842 
   843 simproc_setup group_cancel_le ("a \<le> (b::'a::ordered_ab_group_add)") =
   844   {* fn phi => fn ss => try Group_Cancel.cancel_le_conv *}
   845 
   846 simproc_setup group_cancel_less ("a < (b::'a::ordered_ab_group_add)") =
   847   {* fn phi => fn ss => try Group_Cancel.cancel_less_conv *}
   848 
   849 class linordered_ab_semigroup_add =
   850   linorder + ordered_ab_semigroup_add
   851 
   852 class linordered_cancel_ab_semigroup_add =
   853   linorder + ordered_cancel_ab_semigroup_add
   854 begin
   855 
   856 subclass linordered_ab_semigroup_add ..
   857 
   858 subclass ordered_ab_semigroup_add_imp_le
   859 proof
   860   fix a b c :: 'a
   861   assume le: "c + a <= c + b"  
   862   show "a <= b"
   863   proof (rule ccontr)
   864     assume w: "~ a \<le> b"
   865     hence "b <= a" by (simp add: linorder_not_le)
   866     hence le2: "c + b <= c + a" by (rule add_left_mono)
   867     have "a = b" 
   868       apply (insert le)
   869       apply (insert le2)
   870       apply (drule antisym, simp_all)
   871       done
   872     with w show False 
   873       by (simp add: linorder_not_le [symmetric])
   874   qed
   875 qed
   876 
   877 end
   878 
   879 class linordered_ab_group_add = linorder + ordered_ab_group_add
   880 begin
   881 
   882 subclass linordered_cancel_ab_semigroup_add ..
   883 
   884 lemma neg_less_eq_nonneg [simp]:
   885   "- a \<le> a \<longleftrightarrow> 0 \<le> a"
   886 proof
   887   assume A: "- a \<le> a" show "0 \<le> a"
   888   proof (rule classical)
   889     assume "\<not> 0 \<le> a"
   890     then have "a < 0" by auto
   891     with A have "- a < 0" by (rule le_less_trans)
   892     then show ?thesis by auto
   893   qed
   894 next
   895   assume A: "0 \<le> a" show "- a \<le> a"
   896   proof (rule order_trans)
   897     show "- a \<le> 0" using A by (simp add: minus_le_iff)
   898   next
   899     show "0 \<le> a" using A .
   900   qed
   901 qed
   902 
   903 lemma neg_less_nonneg [simp]:
   904   "- a < a \<longleftrightarrow> 0 < a"
   905 proof
   906   assume A: "- a < a" show "0 < a"
   907   proof (rule classical)
   908     assume "\<not> 0 < a"
   909     then have "a \<le> 0" by auto
   910     with A have "- a < 0" by (rule less_le_trans)
   911     then show ?thesis by auto
   912   qed
   913 next
   914   assume A: "0 < a" show "- a < a"
   915   proof (rule less_trans)
   916     show "- a < 0" using A by (simp add: minus_le_iff)
   917   next
   918     show "0 < a" using A .
   919   qed
   920 qed
   921 
   922 lemma less_eq_neg_nonpos [simp]:
   923   "a \<le> - a \<longleftrightarrow> a \<le> 0"
   924 proof
   925   assume A: "a \<le> - a" show "a \<le> 0"
   926   proof (rule classical)
   927     assume "\<not> a \<le> 0"
   928     then have "0 < a" by auto
   929     then have "0 < - a" using A by (rule less_le_trans)
   930     then show ?thesis by auto
   931   qed
   932 next
   933   assume A: "a \<le> 0" show "a \<le> - a"
   934   proof (rule order_trans)
   935     show "0 \<le> - a" using A by (simp add: minus_le_iff)
   936   next
   937     show "a \<le> 0" using A .
   938   qed
   939 qed
   940 
   941 lemma equal_neg_zero [simp]:
   942   "a = - a \<longleftrightarrow> a = 0"
   943 proof
   944   assume "a = 0" then show "a = - a" by simp
   945 next
   946   assume A: "a = - a" show "a = 0"
   947   proof (cases "0 \<le> a")
   948     case True with A have "0 \<le> - a" by auto
   949     with le_minus_iff have "a \<le> 0" by simp
   950     with True show ?thesis by (auto intro: order_trans)
   951   next
   952     case False then have B: "a \<le> 0" by auto
   953     with A have "- a \<le> 0" by auto
   954     with B show ?thesis by (auto intro: order_trans)
   955   qed
   956 qed
   957 
   958 lemma neg_equal_zero [simp]:
   959   "- a = a \<longleftrightarrow> a = 0"
   960   by (auto dest: sym)
   961 
   962 lemma double_zero [simp]:
   963   "a + a = 0 \<longleftrightarrow> a = 0"
   964 proof
   965   assume assm: "a + a = 0"
   966   then have a: "- a = a" by (rule minus_unique)
   967   then show "a = 0" by (simp only: neg_equal_zero)
   968 qed simp
   969 
   970 lemma double_zero_sym [simp]:
   971   "0 = a + a \<longleftrightarrow> a = 0"
   972   by (rule, drule sym) simp_all
   973 
   974 lemma zero_less_double_add_iff_zero_less_single_add [simp]:
   975   "0 < a + a \<longleftrightarrow> 0 < a"
   976 proof
   977   assume "0 < a + a"
   978   then have "0 - a < a" by (simp only: diff_less_eq)
   979   then have "- a < a" by simp
   980   then show "0 < a" by (simp only: neg_less_nonneg)
   981 next
   982   assume "0 < a"
   983   with this have "0 + 0 < a + a"
   984     by (rule add_strict_mono)
   985   then show "0 < a + a" by simp
   986 qed
   987 
   988 lemma zero_le_double_add_iff_zero_le_single_add [simp]:
   989   "0 \<le> a + a \<longleftrightarrow> 0 \<le> a"
   990   by (auto simp add: le_less)
   991 
   992 lemma double_add_less_zero_iff_single_add_less_zero [simp]:
   993   "a + a < 0 \<longleftrightarrow> a < 0"
   994 proof -
   995   have "\<not> a + a < 0 \<longleftrightarrow> \<not> a < 0"
   996     by (simp add: not_less)
   997   then show ?thesis by simp
   998 qed
   999 
  1000 lemma double_add_le_zero_iff_single_add_le_zero [simp]:
  1001   "a + a \<le> 0 \<longleftrightarrow> a \<le> 0" 
  1002 proof -
  1003   have "\<not> a + a \<le> 0 \<longleftrightarrow> \<not> a \<le> 0"
  1004     by (simp add: not_le)
  1005   then show ?thesis by simp
  1006 qed
  1007 
  1008 lemma le_minus_self_iff:
  1009   "a \<le> - a \<longleftrightarrow> a \<le> 0"
  1010 proof -
  1011   from add_le_cancel_left [of "- a" "a + a" 0]
  1012   have "a \<le> - a \<longleftrightarrow> a + a \<le> 0" 
  1013     by (simp add: add_assoc [symmetric])
  1014   thus ?thesis by simp
  1015 qed
  1016 
  1017 lemma minus_le_self_iff:
  1018   "- a \<le> a \<longleftrightarrow> 0 \<le> a"
  1019 proof -
  1020   from add_le_cancel_left [of "- a" 0 "a + a"]
  1021   have "- a \<le> a \<longleftrightarrow> 0 \<le> a + a" 
  1022     by (simp add: add_assoc [symmetric])
  1023   thus ?thesis by simp
  1024 qed
  1025 
  1026 lemma minus_max_eq_min:
  1027   "- max x y = min (-x) (-y)"
  1028   by (auto simp add: max_def min_def)
  1029 
  1030 lemma minus_min_eq_max:
  1031   "- min x y = max (-x) (-y)"
  1032   by (auto simp add: max_def min_def)
  1033 
  1034 end
  1035 
  1036 context ordered_comm_monoid_add
  1037 begin
  1038 
  1039 lemma add_increasing:
  1040   "0 \<le> a \<Longrightarrow> b \<le> c \<Longrightarrow> b \<le> a + c"
  1041   by (insert add_mono [of 0 a b c], simp)
  1042 
  1043 lemma add_increasing2:
  1044   "0 \<le> c \<Longrightarrow> b \<le> a \<Longrightarrow> b \<le> a + c"
  1045   by (simp add: add_increasing add_commute [of a])
  1046 
  1047 lemma add_strict_increasing:
  1048   "0 < a \<Longrightarrow> b \<le> c \<Longrightarrow> b < a + c"
  1049   by (insert add_less_le_mono [of 0 a b c], simp)
  1050 
  1051 lemma add_strict_increasing2:
  1052   "0 \<le> a \<Longrightarrow> b < c \<Longrightarrow> b < a + c"
  1053   by (insert add_le_less_mono [of 0 a b c], simp)
  1054 
  1055 end
  1056 
  1057 class abs =
  1058   fixes abs :: "'a \<Rightarrow> 'a"
  1059 begin
  1060 
  1061 notation (xsymbols)
  1062   abs  ("\<bar>_\<bar>")
  1063 
  1064 notation (HTML output)
  1065   abs  ("\<bar>_\<bar>")
  1066 
  1067 end
  1068 
  1069 class sgn =
  1070   fixes sgn :: "'a \<Rightarrow> 'a"
  1071 
  1072 class abs_if = minus + uminus + ord + zero + abs +
  1073   assumes abs_if: "\<bar>a\<bar> = (if a < 0 then - a else a)"
  1074 
  1075 class sgn_if = minus + uminus + zero + one + ord + sgn +
  1076   assumes sgn_if: "sgn x = (if x = 0 then 0 else if 0 < x then 1 else - 1)"
  1077 begin
  1078 
  1079 lemma sgn0 [simp]: "sgn 0 = 0"
  1080   by (simp add:sgn_if)
  1081 
  1082 end
  1083 
  1084 class ordered_ab_group_add_abs = ordered_ab_group_add + abs +
  1085   assumes abs_ge_zero [simp]: "\<bar>a\<bar> \<ge> 0"
  1086     and abs_ge_self: "a \<le> \<bar>a\<bar>"
  1087     and abs_leI: "a \<le> b \<Longrightarrow> - a \<le> b \<Longrightarrow> \<bar>a\<bar> \<le> b"
  1088     and abs_minus_cancel [simp]: "\<bar>-a\<bar> = \<bar>a\<bar>"
  1089     and abs_triangle_ineq: "\<bar>a + b\<bar> \<le> \<bar>a\<bar> + \<bar>b\<bar>"
  1090 begin
  1091 
  1092 lemma abs_minus_le_zero: "- \<bar>a\<bar> \<le> 0"
  1093   unfolding neg_le_0_iff_le by simp
  1094 
  1095 lemma abs_of_nonneg [simp]:
  1096   assumes nonneg: "0 \<le> a" shows "\<bar>a\<bar> = a"
  1097 proof (rule antisym)
  1098   from nonneg le_imp_neg_le have "- a \<le> 0" by simp
  1099   from this nonneg have "- a \<le> a" by (rule order_trans)
  1100   then show "\<bar>a\<bar> \<le> a" by (auto intro: abs_leI)
  1101 qed (rule abs_ge_self)
  1102 
  1103 lemma abs_idempotent [simp]: "\<bar>\<bar>a\<bar>\<bar> = \<bar>a\<bar>"
  1104 by (rule antisym)
  1105    (auto intro!: abs_ge_self abs_leI order_trans [of "- \<bar>a\<bar>" 0 "\<bar>a\<bar>"])
  1106 
  1107 lemma abs_eq_0 [simp]: "\<bar>a\<bar> = 0 \<longleftrightarrow> a = 0"
  1108 proof -
  1109   have "\<bar>a\<bar> = 0 \<Longrightarrow> a = 0"
  1110   proof (rule antisym)
  1111     assume zero: "\<bar>a\<bar> = 0"
  1112     with abs_ge_self show "a \<le> 0" by auto
  1113     from zero have "\<bar>-a\<bar> = 0" by simp
  1114     with abs_ge_self [of "- a"] have "- a \<le> 0" by auto
  1115     with neg_le_0_iff_le show "0 \<le> a" by auto
  1116   qed
  1117   then show ?thesis by auto
  1118 qed
  1119 
  1120 lemma abs_zero [simp]: "\<bar>0\<bar> = 0"
  1121 by simp
  1122 
  1123 lemma abs_0_eq [simp, no_atp]: "0 = \<bar>a\<bar> \<longleftrightarrow> a = 0"
  1124 proof -
  1125   have "0 = \<bar>a\<bar> \<longleftrightarrow> \<bar>a\<bar> = 0" by (simp only: eq_ac)
  1126   thus ?thesis by simp
  1127 qed
  1128 
  1129 lemma abs_le_zero_iff [simp]: "\<bar>a\<bar> \<le> 0 \<longleftrightarrow> a = 0" 
  1130 proof
  1131   assume "\<bar>a\<bar> \<le> 0"
  1132   then have "\<bar>a\<bar> = 0" by (rule antisym) simp
  1133   thus "a = 0" by simp
  1134 next
  1135   assume "a = 0"
  1136   thus "\<bar>a\<bar> \<le> 0" by simp
  1137 qed
  1138 
  1139 lemma zero_less_abs_iff [simp]: "0 < \<bar>a\<bar> \<longleftrightarrow> a \<noteq> 0"
  1140 by (simp add: less_le)
  1141 
  1142 lemma abs_not_less_zero [simp]: "\<not> \<bar>a\<bar> < 0"
  1143 proof -
  1144   have a: "\<And>x y. x \<le> y \<Longrightarrow> \<not> y < x" by auto
  1145   show ?thesis by (simp add: a)
  1146 qed
  1147 
  1148 lemma abs_ge_minus_self: "- a \<le> \<bar>a\<bar>"
  1149 proof -
  1150   have "- a \<le> \<bar>-a\<bar>" by (rule abs_ge_self)
  1151   then show ?thesis by simp
  1152 qed
  1153 
  1154 lemma abs_minus_commute: 
  1155   "\<bar>a - b\<bar> = \<bar>b - a\<bar>"
  1156 proof -
  1157   have "\<bar>a - b\<bar> = \<bar>- (a - b)\<bar>" by (simp only: abs_minus_cancel)
  1158   also have "... = \<bar>b - a\<bar>" by simp
  1159   finally show ?thesis .
  1160 qed
  1161 
  1162 lemma abs_of_pos: "0 < a \<Longrightarrow> \<bar>a\<bar> = a"
  1163 by (rule abs_of_nonneg, rule less_imp_le)
  1164 
  1165 lemma abs_of_nonpos [simp]:
  1166   assumes "a \<le> 0" shows "\<bar>a\<bar> = - a"
  1167 proof -
  1168   let ?b = "- a"
  1169   have "- ?b \<le> 0 \<Longrightarrow> \<bar>- ?b\<bar> = - (- ?b)"
  1170   unfolding abs_minus_cancel [of "?b"]
  1171   unfolding neg_le_0_iff_le [of "?b"]
  1172   unfolding minus_minus by (erule abs_of_nonneg)
  1173   then show ?thesis using assms by auto
  1174 qed
  1175   
  1176 lemma abs_of_neg: "a < 0 \<Longrightarrow> \<bar>a\<bar> = - a"
  1177 by (rule abs_of_nonpos, rule less_imp_le)
  1178 
  1179 lemma abs_le_D1: "\<bar>a\<bar> \<le> b \<Longrightarrow> a \<le> b"
  1180 by (insert abs_ge_self, blast intro: order_trans)
  1181 
  1182 lemma abs_le_D2: "\<bar>a\<bar> \<le> b \<Longrightarrow> - a \<le> b"
  1183 by (insert abs_le_D1 [of "- a"], simp)
  1184 
  1185 lemma abs_le_iff: "\<bar>a\<bar> \<le> b \<longleftrightarrow> a \<le> b \<and> - a \<le> b"
  1186 by (blast intro: abs_leI dest: abs_le_D1 abs_le_D2)
  1187 
  1188 lemma abs_triangle_ineq2: "\<bar>a\<bar> - \<bar>b\<bar> \<le> \<bar>a - b\<bar>"
  1189 proof -
  1190   have "\<bar>a\<bar> = \<bar>b + (a - b)\<bar>"
  1191     by (simp add: algebra_simps add_diff_cancel)
  1192   then have "\<bar>a\<bar> \<le> \<bar>b\<bar> + \<bar>a - b\<bar>"
  1193     by (simp add: abs_triangle_ineq)
  1194   then show ?thesis
  1195     by (simp add: algebra_simps)
  1196 qed
  1197 
  1198 lemma abs_triangle_ineq2_sym: "\<bar>a\<bar> - \<bar>b\<bar> \<le> \<bar>b - a\<bar>"
  1199   by (simp only: abs_minus_commute [of b] abs_triangle_ineq2)
  1200 
  1201 lemma abs_triangle_ineq3: "\<bar>\<bar>a\<bar> - \<bar>b\<bar>\<bar> \<le> \<bar>a - b\<bar>"
  1202   by (simp add: abs_le_iff abs_triangle_ineq2 abs_triangle_ineq2_sym)
  1203 
  1204 lemma abs_triangle_ineq4: "\<bar>a - b\<bar> \<le> \<bar>a\<bar> + \<bar>b\<bar>"
  1205 proof -
  1206   have "\<bar>a - b\<bar> = \<bar>a + - b\<bar>" by (subst diff_minus, rule refl)
  1207   also have "... \<le> \<bar>a\<bar> + \<bar>- b\<bar>" by (rule abs_triangle_ineq)
  1208   finally show ?thesis by simp
  1209 qed
  1210 
  1211 lemma abs_diff_triangle_ineq: "\<bar>a + b - (c + d)\<bar> \<le> \<bar>a - c\<bar> + \<bar>b - d\<bar>"
  1212 proof -
  1213   have "\<bar>a + b - (c+d)\<bar> = \<bar>(a-c) + (b-d)\<bar>" by (simp add: diff_minus add_ac)
  1214   also have "... \<le> \<bar>a-c\<bar> + \<bar>b-d\<bar>" by (rule abs_triangle_ineq)
  1215   finally show ?thesis .
  1216 qed
  1217 
  1218 lemma abs_add_abs [simp]:
  1219   "\<bar>\<bar>a\<bar> + \<bar>b\<bar>\<bar> = \<bar>a\<bar> + \<bar>b\<bar>" (is "?L = ?R")
  1220 proof (rule antisym)
  1221   show "?L \<ge> ?R" by(rule abs_ge_self)
  1222 next
  1223   have "?L \<le> \<bar>\<bar>a\<bar>\<bar> + \<bar>\<bar>b\<bar>\<bar>" by(rule abs_triangle_ineq)
  1224   also have "\<dots> = ?R" by simp
  1225   finally show "?L \<le> ?R" .
  1226 qed
  1227 
  1228 end
  1229 
  1230 
  1231 subsection {* Tools setup *}
  1232 
  1233 lemma add_mono_thms_linordered_semiring [no_atp]:
  1234   fixes i j k :: "'a\<Colon>ordered_ab_semigroup_add"
  1235   shows "i \<le> j \<and> k \<le> l \<Longrightarrow> i + k \<le> j + l"
  1236     and "i = j \<and> k \<le> l \<Longrightarrow> i + k \<le> j + l"
  1237     and "i \<le> j \<and> k = l \<Longrightarrow> i + k \<le> j + l"
  1238     and "i = j \<and> k = l \<Longrightarrow> i + k = j + l"
  1239 by (rule add_mono, clarify+)+
  1240 
  1241 lemma add_mono_thms_linordered_field [no_atp]:
  1242   fixes i j k :: "'a\<Colon>ordered_cancel_ab_semigroup_add"
  1243   shows "i < j \<and> k = l \<Longrightarrow> i + k < j + l"
  1244     and "i = j \<and> k < l \<Longrightarrow> i + k < j + l"
  1245     and "i < j \<and> k \<le> l \<Longrightarrow> i + k < j + l"
  1246     and "i \<le> j \<and> k < l \<Longrightarrow> i + k < j + l"
  1247     and "i < j \<and> k < l \<Longrightarrow> i + k < j + l"
  1248 by (auto intro: add_strict_right_mono add_strict_left_mono
  1249   add_less_le_mono add_le_less_mono add_strict_mono)
  1250 
  1251 code_modulename SML
  1252   Groups Arith
  1253 
  1254 code_modulename OCaml
  1255   Groups Arith
  1256 
  1257 code_modulename Haskell
  1258   Groups Arith
  1259 
  1260 
  1261 text {* Legacy *}
  1262 
  1263 lemmas diff_def = diff_minus
  1264 
  1265 end