src/HOL/Groups.thy
author huffman
Fri Jul 27 15:42:39 2012 +0200 (2012-07-27)
changeset 48556 62a3fbf9d35b
parent 45548 3e2722d66169
child 48891 c0eafbd55de3
permissions -rw-r--r--
replace abel_cancel simprocs with functionally equivalent, but simpler and faster ones
     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/group_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 lemma add_diff_cancel_left: "(c + a) - (c + b) = a - b"
   476   by (simp add: diff_minus add_ac)
   477 
   478 end
   479 
   480 
   481 subsection {* (Partially) Ordered Groups *} 
   482 
   483 text {*
   484   The theory of partially ordered groups is taken from the books:
   485   \begin{itemize}
   486   \item \emph{Lattice Theory} by Garret Birkhoff, American Mathematical Society 1979 
   487   \item \emph{Partially Ordered Algebraic Systems}, Pergamon Press 1963
   488   \end{itemize}
   489   Most of the used notions can also be looked up in 
   490   \begin{itemize}
   491   \item \url{http://www.mathworld.com} by Eric Weisstein et. al.
   492   \item \emph{Algebra I} by van der Waerden, Springer.
   493   \end{itemize}
   494 *}
   495 
   496 class ordered_ab_semigroup_add = order + ab_semigroup_add +
   497   assumes add_left_mono: "a \<le> b \<Longrightarrow> c + a \<le> c + b"
   498 begin
   499 
   500 lemma add_right_mono:
   501   "a \<le> b \<Longrightarrow> a + c \<le> b + c"
   502 by (simp add: add_commute [of _ c] add_left_mono)
   503 
   504 text {* non-strict, in both arguments *}
   505 lemma add_mono:
   506   "a \<le> b \<Longrightarrow> c \<le> d \<Longrightarrow> a + c \<le> b + d"
   507   apply (erule add_right_mono [THEN order_trans])
   508   apply (simp add: add_commute add_left_mono)
   509   done
   510 
   511 end
   512 
   513 class ordered_cancel_ab_semigroup_add =
   514   ordered_ab_semigroup_add + cancel_ab_semigroup_add
   515 begin
   516 
   517 lemma add_strict_left_mono:
   518   "a < b \<Longrightarrow> c + a < c + b"
   519 by (auto simp add: less_le add_left_mono)
   520 
   521 lemma add_strict_right_mono:
   522   "a < b \<Longrightarrow> a + c < b + c"
   523 by (simp add: add_commute [of _ c] add_strict_left_mono)
   524 
   525 text{*Strict monotonicity in both arguments*}
   526 lemma add_strict_mono:
   527   "a < b \<Longrightarrow> c < d \<Longrightarrow> a + c < b + d"
   528 apply (erule add_strict_right_mono [THEN less_trans])
   529 apply (erule add_strict_left_mono)
   530 done
   531 
   532 lemma add_less_le_mono:
   533   "a < b \<Longrightarrow> c \<le> d \<Longrightarrow> a + c < b + d"
   534 apply (erule add_strict_right_mono [THEN less_le_trans])
   535 apply (erule add_left_mono)
   536 done
   537 
   538 lemma add_le_less_mono:
   539   "a \<le> b \<Longrightarrow> c < d \<Longrightarrow> a + c < b + d"
   540 apply (erule add_right_mono [THEN le_less_trans])
   541 apply (erule add_strict_left_mono) 
   542 done
   543 
   544 end
   545 
   546 class ordered_ab_semigroup_add_imp_le =
   547   ordered_cancel_ab_semigroup_add +
   548   assumes add_le_imp_le_left: "c + a \<le> c + b \<Longrightarrow> a \<le> b"
   549 begin
   550 
   551 lemma add_less_imp_less_left:
   552   assumes less: "c + a < c + b" shows "a < b"
   553 proof -
   554   from less have le: "c + a <= c + b" by (simp add: order_le_less)
   555   have "a <= b" 
   556     apply (insert le)
   557     apply (drule add_le_imp_le_left)
   558     by (insert le, drule add_le_imp_le_left, assumption)
   559   moreover have "a \<noteq> b"
   560   proof (rule ccontr)
   561     assume "~(a \<noteq> b)"
   562     then have "a = b" by simp
   563     then have "c + a = c + b" by simp
   564     with less show "False"by simp
   565   qed
   566   ultimately show "a < b" by (simp add: order_le_less)
   567 qed
   568 
   569 lemma add_less_imp_less_right:
   570   "a + c < b + c \<Longrightarrow> a < b"
   571 apply (rule add_less_imp_less_left [of c])
   572 apply (simp add: add_commute)  
   573 done
   574 
   575 lemma add_less_cancel_left [simp]:
   576   "c + a < c + b \<longleftrightarrow> a < b"
   577 by (blast intro: add_less_imp_less_left add_strict_left_mono) 
   578 
   579 lemma add_less_cancel_right [simp]:
   580   "a + c < b + c \<longleftrightarrow> a < b"
   581 by (blast intro: add_less_imp_less_right add_strict_right_mono)
   582 
   583 lemma add_le_cancel_left [simp]:
   584   "c + a \<le> c + b \<longleftrightarrow> a \<le> b"
   585 by (auto, drule add_le_imp_le_left, simp_all add: add_left_mono) 
   586 
   587 lemma add_le_cancel_right [simp]:
   588   "a + c \<le> b + c \<longleftrightarrow> a \<le> b"
   589 by (simp add: add_commute [of a c] add_commute [of b c])
   590 
   591 lemma add_le_imp_le_right:
   592   "a + c \<le> b + c \<Longrightarrow> a \<le> b"
   593 by simp
   594 
   595 lemma max_add_distrib_left:
   596   "max x y + z = max (x + z) (y + z)"
   597   unfolding max_def by auto
   598 
   599 lemma min_add_distrib_left:
   600   "min x y + z = min (x + z) (y + z)"
   601   unfolding min_def by auto
   602 
   603 lemma max_add_distrib_right:
   604   "x + max y z = max (x + y) (x + z)"
   605   unfolding max_def by auto
   606 
   607 lemma min_add_distrib_right:
   608   "x + min y z = min (x + y) (x + z)"
   609   unfolding min_def by auto
   610 
   611 end
   612 
   613 subsection {* Support for reasoning about signs *}
   614 
   615 class ordered_comm_monoid_add =
   616   ordered_cancel_ab_semigroup_add + comm_monoid_add
   617 begin
   618 
   619 lemma add_pos_nonneg:
   620   assumes "0 < a" and "0 \<le> b" shows "0 < a + b"
   621 proof -
   622   have "0 + 0 < a + b" 
   623     using assms by (rule add_less_le_mono)
   624   then show ?thesis by simp
   625 qed
   626 
   627 lemma add_pos_pos:
   628   assumes "0 < a" and "0 < b" shows "0 < a + b"
   629 by (rule add_pos_nonneg) (insert assms, auto)
   630 
   631 lemma add_nonneg_pos:
   632   assumes "0 \<le> a" and "0 < b" shows "0 < a + b"
   633 proof -
   634   have "0 + 0 < a + b" 
   635     using assms by (rule add_le_less_mono)
   636   then show ?thesis by simp
   637 qed
   638 
   639 lemma add_nonneg_nonneg [simp]:
   640   assumes "0 \<le> a" and "0 \<le> b" shows "0 \<le> a + b"
   641 proof -
   642   have "0 + 0 \<le> a + b" 
   643     using assms by (rule add_mono)
   644   then show ?thesis by simp
   645 qed
   646 
   647 lemma add_neg_nonpos:
   648   assumes "a < 0" and "b \<le> 0" shows "a + b < 0"
   649 proof -
   650   have "a + b < 0 + 0"
   651     using assms by (rule add_less_le_mono)
   652   then show ?thesis by simp
   653 qed
   654 
   655 lemma add_neg_neg: 
   656   assumes "a < 0" and "b < 0" shows "a + b < 0"
   657 by (rule add_neg_nonpos) (insert assms, auto)
   658 
   659 lemma add_nonpos_neg:
   660   assumes "a \<le> 0" and "b < 0" shows "a + b < 0"
   661 proof -
   662   have "a + b < 0 + 0"
   663     using assms by (rule add_le_less_mono)
   664   then show ?thesis by simp
   665 qed
   666 
   667 lemma add_nonpos_nonpos:
   668   assumes "a \<le> 0" and "b \<le> 0" shows "a + b \<le> 0"
   669 proof -
   670   have "a + b \<le> 0 + 0"
   671     using assms by (rule add_mono)
   672   then show ?thesis by simp
   673 qed
   674 
   675 lemmas add_sign_intros =
   676   add_pos_nonneg add_pos_pos add_nonneg_pos add_nonneg_nonneg
   677   add_neg_nonpos add_neg_neg add_nonpos_neg add_nonpos_nonpos
   678 
   679 lemma add_nonneg_eq_0_iff:
   680   assumes x: "0 \<le> x" and y: "0 \<le> y"
   681   shows "x + y = 0 \<longleftrightarrow> x = 0 \<and> y = 0"
   682 proof (intro iffI conjI)
   683   have "x = x + 0" by simp
   684   also have "x + 0 \<le> x + y" using y by (rule add_left_mono)
   685   also assume "x + y = 0"
   686   also have "0 \<le> x" using x .
   687   finally show "x = 0" .
   688 next
   689   have "y = 0 + y" by simp
   690   also have "0 + y \<le> x + y" using x by (rule add_right_mono)
   691   also assume "x + y = 0"
   692   also have "0 \<le> y" using y .
   693   finally show "y = 0" .
   694 next
   695   assume "x = 0 \<and> y = 0"
   696   then show "x + y = 0" by simp
   697 qed
   698 
   699 end
   700 
   701 class ordered_ab_group_add =
   702   ab_group_add + ordered_ab_semigroup_add
   703 begin
   704 
   705 subclass ordered_cancel_ab_semigroup_add ..
   706 
   707 subclass ordered_ab_semigroup_add_imp_le
   708 proof
   709   fix a b c :: 'a
   710   assume "c + a \<le> c + b"
   711   hence "(-c) + (c + a) \<le> (-c) + (c + b)" by (rule add_left_mono)
   712   hence "((-c) + c) + a \<le> ((-c) + c) + b" by (simp only: add_assoc)
   713   thus "a \<le> b" by simp
   714 qed
   715 
   716 subclass ordered_comm_monoid_add ..
   717 
   718 lemma max_diff_distrib_left:
   719   shows "max x y - z = max (x - z) (y - z)"
   720 by (simp add: diff_minus, rule max_add_distrib_left) 
   721 
   722 lemma min_diff_distrib_left:
   723   shows "min x y - z = min (x - z) (y - z)"
   724 by (simp add: diff_minus, rule min_add_distrib_left) 
   725 
   726 lemma le_imp_neg_le:
   727   assumes "a \<le> b" shows "-b \<le> -a"
   728 proof -
   729   have "-a+a \<le> -a+b" using `a \<le> b` by (rule add_left_mono) 
   730   hence "0 \<le> -a+b" by simp
   731   hence "0 + (-b) \<le> (-a + b) + (-b)" by (rule add_right_mono) 
   732   thus ?thesis by (simp add: add_assoc)
   733 qed
   734 
   735 lemma neg_le_iff_le [simp]: "- b \<le> - a \<longleftrightarrow> a \<le> b"
   736 proof 
   737   assume "- b \<le> - a"
   738   hence "- (- a) \<le> - (- b)" by (rule le_imp_neg_le)
   739   thus "a\<le>b" by simp
   740 next
   741   assume "a\<le>b"
   742   thus "-b \<le> -a" by (rule le_imp_neg_le)
   743 qed
   744 
   745 lemma neg_le_0_iff_le [simp]: "- a \<le> 0 \<longleftrightarrow> 0 \<le> a"
   746 by (subst neg_le_iff_le [symmetric], simp)
   747 
   748 lemma neg_0_le_iff_le [simp]: "0 \<le> - a \<longleftrightarrow> a \<le> 0"
   749 by (subst neg_le_iff_le [symmetric], simp)
   750 
   751 lemma neg_less_iff_less [simp]: "- b < - a \<longleftrightarrow> a < b"
   752 by (force simp add: less_le) 
   753 
   754 lemma neg_less_0_iff_less [simp]: "- a < 0 \<longleftrightarrow> 0 < a"
   755 by (subst neg_less_iff_less [symmetric], simp)
   756 
   757 lemma neg_0_less_iff_less [simp]: "0 < - a \<longleftrightarrow> a < 0"
   758 by (subst neg_less_iff_less [symmetric], simp)
   759 
   760 text{*The next several equations can make the simplifier loop!*}
   761 
   762 lemma less_minus_iff: "a < - b \<longleftrightarrow> b < - a"
   763 proof -
   764   have "(- (-a) < - b) = (b < - a)" by (rule neg_less_iff_less)
   765   thus ?thesis by simp
   766 qed
   767 
   768 lemma minus_less_iff: "- a < b \<longleftrightarrow> - b < a"
   769 proof -
   770   have "(- a < - (-b)) = (- b < a)" by (rule neg_less_iff_less)
   771   thus ?thesis by simp
   772 qed
   773 
   774 lemma le_minus_iff: "a \<le> - b \<longleftrightarrow> b \<le> - a"
   775 proof -
   776   have mm: "!! a (b::'a). (-(-a)) < -b \<Longrightarrow> -(-b) < -a" by (simp only: minus_less_iff)
   777   have "(- (- a) <= -b) = (b <= - a)" 
   778     apply (auto simp only: le_less)
   779     apply (drule mm)
   780     apply (simp_all)
   781     apply (drule mm[simplified], assumption)
   782     done
   783   then show ?thesis by simp
   784 qed
   785 
   786 lemma minus_le_iff: "- a \<le> b \<longleftrightarrow> - b \<le> a"
   787 by (auto simp add: le_less minus_less_iff)
   788 
   789 lemma diff_less_0_iff_less [simp, no_atp]:
   790   "a - b < 0 \<longleftrightarrow> a < b"
   791 proof -
   792   have "a - b < 0 \<longleftrightarrow> a + (- b) < b + (- b)" by (simp add: diff_minus)
   793   also have "... \<longleftrightarrow> a < b" by (simp only: add_less_cancel_right)
   794   finally show ?thesis .
   795 qed
   796 
   797 lemmas less_iff_diff_less_0 = diff_less_0_iff_less [symmetric]
   798 
   799 lemma diff_less_eq[algebra_simps, field_simps]: "a - b < c \<longleftrightarrow> a < c + b"
   800 apply (subst less_iff_diff_less_0 [of a])
   801 apply (rule less_iff_diff_less_0 [of _ c, THEN ssubst])
   802 apply (simp add: diff_minus add_ac)
   803 done
   804 
   805 lemma less_diff_eq[algebra_simps, field_simps]: "a < c - b \<longleftrightarrow> a + b < c"
   806 apply (subst less_iff_diff_less_0 [of "a + b"])
   807 apply (subst less_iff_diff_less_0 [of a])
   808 apply (simp add: diff_minus add_ac)
   809 done
   810 
   811 lemma diff_le_eq[algebra_simps, field_simps]: "a - b \<le> c \<longleftrightarrow> a \<le> c + b"
   812 by (auto simp add: le_less diff_less_eq diff_add_cancel add_diff_cancel)
   813 
   814 lemma le_diff_eq[algebra_simps, field_simps]: "a \<le> c - b \<longleftrightarrow> a + b \<le> c"
   815 by (auto simp add: le_less less_diff_eq diff_add_cancel add_diff_cancel)
   816 
   817 lemma diff_le_0_iff_le [simp, no_atp]:
   818   "a - b \<le> 0 \<longleftrightarrow> a \<le> b"
   819   by (simp add: algebra_simps)
   820 
   821 lemmas le_iff_diff_le_0 = diff_le_0_iff_le [symmetric]
   822 
   823 lemma diff_eq_diff_less:
   824   "a - b = c - d \<Longrightarrow> a < b \<longleftrightarrow> c < d"
   825   by (auto simp only: less_iff_diff_less_0 [of a b] less_iff_diff_less_0 [of c d])
   826 
   827 lemma diff_eq_diff_less_eq:
   828   "a - b = c - d \<Longrightarrow> a \<le> b \<longleftrightarrow> c \<le> d"
   829   by (auto simp only: le_iff_diff_le_0 [of a b] le_iff_diff_le_0 [of c d])
   830 
   831 end
   832 
   833 use "Tools/group_cancel.ML"
   834 
   835 simproc_setup group_cancel_add ("a + b::'a::ab_group_add") =
   836   {* fn phi => fn ss => try Group_Cancel.cancel_add_conv *}
   837 
   838 simproc_setup group_cancel_diff ("a - b::'a::ab_group_add") =
   839   {* fn phi => fn ss => try Group_Cancel.cancel_diff_conv *}
   840 
   841 simproc_setup group_cancel_eq ("a = (b::'a::ab_group_add)") =
   842   {* fn phi => fn ss => try Group_Cancel.cancel_eq_conv *}
   843 
   844 simproc_setup group_cancel_le ("a \<le> (b::'a::ordered_ab_group_add)") =
   845   {* fn phi => fn ss => try Group_Cancel.cancel_le_conv *}
   846 
   847 simproc_setup group_cancel_less ("a < (b::'a::ordered_ab_group_add)") =
   848   {* fn phi => fn ss => try Group_Cancel.cancel_less_conv *}
   849 
   850 class linordered_ab_semigroup_add =
   851   linorder + ordered_ab_semigroup_add
   852 
   853 class linordered_cancel_ab_semigroup_add =
   854   linorder + ordered_cancel_ab_semigroup_add
   855 begin
   856 
   857 subclass linordered_ab_semigroup_add ..
   858 
   859 subclass ordered_ab_semigroup_add_imp_le
   860 proof
   861   fix a b c :: 'a
   862   assume le: "c + a <= c + b"  
   863   show "a <= b"
   864   proof (rule ccontr)
   865     assume w: "~ a \<le> b"
   866     hence "b <= a" by (simp add: linorder_not_le)
   867     hence le2: "c + b <= c + a" by (rule add_left_mono)
   868     have "a = b" 
   869       apply (insert le)
   870       apply (insert le2)
   871       apply (drule antisym, simp_all)
   872       done
   873     with w show False 
   874       by (simp add: linorder_not_le [symmetric])
   875   qed
   876 qed
   877 
   878 end
   879 
   880 class linordered_ab_group_add = linorder + ordered_ab_group_add
   881 begin
   882 
   883 subclass linordered_cancel_ab_semigroup_add ..
   884 
   885 lemma neg_less_eq_nonneg [simp]:
   886   "- a \<le> a \<longleftrightarrow> 0 \<le> a"
   887 proof
   888   assume A: "- a \<le> a" show "0 \<le> a"
   889   proof (rule classical)
   890     assume "\<not> 0 \<le> a"
   891     then have "a < 0" by auto
   892     with A have "- a < 0" by (rule le_less_trans)
   893     then show ?thesis by auto
   894   qed
   895 next
   896   assume A: "0 \<le> a" show "- a \<le> a"
   897   proof (rule order_trans)
   898     show "- a \<le> 0" using A by (simp add: minus_le_iff)
   899   next
   900     show "0 \<le> a" using A .
   901   qed
   902 qed
   903 
   904 lemma neg_less_nonneg [simp]:
   905   "- a < a \<longleftrightarrow> 0 < a"
   906 proof
   907   assume A: "- a < a" show "0 < a"
   908   proof (rule classical)
   909     assume "\<not> 0 < a"
   910     then have "a \<le> 0" by auto
   911     with A have "- a < 0" by (rule less_le_trans)
   912     then show ?thesis by auto
   913   qed
   914 next
   915   assume A: "0 < a" show "- a < a"
   916   proof (rule less_trans)
   917     show "- a < 0" using A by (simp add: minus_le_iff)
   918   next
   919     show "0 < a" using A .
   920   qed
   921 qed
   922 
   923 lemma less_eq_neg_nonpos [simp]:
   924   "a \<le> - a \<longleftrightarrow> a \<le> 0"
   925 proof
   926   assume A: "a \<le> - a" show "a \<le> 0"
   927   proof (rule classical)
   928     assume "\<not> a \<le> 0"
   929     then have "0 < a" by auto
   930     then have "0 < - a" using A by (rule less_le_trans)
   931     then show ?thesis by auto
   932   qed
   933 next
   934   assume A: "a \<le> 0" show "a \<le> - a"
   935   proof (rule order_trans)
   936     show "0 \<le> - a" using A by (simp add: minus_le_iff)
   937   next
   938     show "a \<le> 0" using A .
   939   qed
   940 qed
   941 
   942 lemma equal_neg_zero [simp]:
   943   "a = - a \<longleftrightarrow> a = 0"
   944 proof
   945   assume "a = 0" then show "a = - a" by simp
   946 next
   947   assume A: "a = - a" show "a = 0"
   948   proof (cases "0 \<le> a")
   949     case True with A have "0 \<le> - a" by auto
   950     with le_minus_iff have "a \<le> 0" by simp
   951     with True show ?thesis by (auto intro: order_trans)
   952   next
   953     case False then have B: "a \<le> 0" by auto
   954     with A have "- a \<le> 0" by auto
   955     with B show ?thesis by (auto intro: order_trans)
   956   qed
   957 qed
   958 
   959 lemma neg_equal_zero [simp]:
   960   "- a = a \<longleftrightarrow> a = 0"
   961   by (auto dest: sym)
   962 
   963 lemma double_zero [simp]:
   964   "a + a = 0 \<longleftrightarrow> a = 0"
   965 proof
   966   assume assm: "a + a = 0"
   967   then have a: "- a = a" by (rule minus_unique)
   968   then show "a = 0" by (simp only: neg_equal_zero)
   969 qed simp
   970 
   971 lemma double_zero_sym [simp]:
   972   "0 = a + a \<longleftrightarrow> a = 0"
   973   by (rule, drule sym) simp_all
   974 
   975 lemma zero_less_double_add_iff_zero_less_single_add [simp]:
   976   "0 < a + a \<longleftrightarrow> 0 < a"
   977 proof
   978   assume "0 < a + a"
   979   then have "0 - a < a" by (simp only: diff_less_eq)
   980   then have "- a < a" by simp
   981   then show "0 < a" by (simp only: neg_less_nonneg)
   982 next
   983   assume "0 < a"
   984   with this have "0 + 0 < a + a"
   985     by (rule add_strict_mono)
   986   then show "0 < a + a" by simp
   987 qed
   988 
   989 lemma zero_le_double_add_iff_zero_le_single_add [simp]:
   990   "0 \<le> a + a \<longleftrightarrow> 0 \<le> a"
   991   by (auto simp add: le_less)
   992 
   993 lemma double_add_less_zero_iff_single_add_less_zero [simp]:
   994   "a + a < 0 \<longleftrightarrow> a < 0"
   995 proof -
   996   have "\<not> a + a < 0 \<longleftrightarrow> \<not> a < 0"
   997     by (simp add: not_less)
   998   then show ?thesis by simp
   999 qed
  1000 
  1001 lemma double_add_le_zero_iff_single_add_le_zero [simp]:
  1002   "a + a \<le> 0 \<longleftrightarrow> a \<le> 0" 
  1003 proof -
  1004   have "\<not> a + a \<le> 0 \<longleftrightarrow> \<not> a \<le> 0"
  1005     by (simp add: not_le)
  1006   then show ?thesis by simp
  1007 qed
  1008 
  1009 lemma le_minus_self_iff:
  1010   "a \<le> - a \<longleftrightarrow> a \<le> 0"
  1011 proof -
  1012   from add_le_cancel_left [of "- a" "a + a" 0]
  1013   have "a \<le> - a \<longleftrightarrow> a + a \<le> 0" 
  1014     by (simp add: add_assoc [symmetric])
  1015   thus ?thesis by simp
  1016 qed
  1017 
  1018 lemma minus_le_self_iff:
  1019   "- a \<le> a \<longleftrightarrow> 0 \<le> a"
  1020 proof -
  1021   from add_le_cancel_left [of "- a" 0 "a + a"]
  1022   have "- a \<le> a \<longleftrightarrow> 0 \<le> a + a" 
  1023     by (simp add: add_assoc [symmetric])
  1024   thus ?thesis by simp
  1025 qed
  1026 
  1027 lemma minus_max_eq_min:
  1028   "- max x y = min (-x) (-y)"
  1029   by (auto simp add: max_def min_def)
  1030 
  1031 lemma minus_min_eq_max:
  1032   "- min x y = max (-x) (-y)"
  1033   by (auto simp add: max_def min_def)
  1034 
  1035 end
  1036 
  1037 context ordered_comm_monoid_add
  1038 begin
  1039 
  1040 lemma add_increasing:
  1041   "0 \<le> a \<Longrightarrow> b \<le> c \<Longrightarrow> b \<le> a + c"
  1042   by (insert add_mono [of 0 a b c], simp)
  1043 
  1044 lemma add_increasing2:
  1045   "0 \<le> c \<Longrightarrow> b \<le> a \<Longrightarrow> b \<le> a + c"
  1046   by (simp add: add_increasing add_commute [of a])
  1047 
  1048 lemma add_strict_increasing:
  1049   "0 < a \<Longrightarrow> b \<le> c \<Longrightarrow> b < a + c"
  1050   by (insert add_less_le_mono [of 0 a b c], simp)
  1051 
  1052 lemma add_strict_increasing2:
  1053   "0 \<le> a \<Longrightarrow> b < c \<Longrightarrow> b < a + c"
  1054   by (insert add_le_less_mono [of 0 a b c], simp)
  1055 
  1056 end
  1057 
  1058 class abs =
  1059   fixes abs :: "'a \<Rightarrow> 'a"
  1060 begin
  1061 
  1062 notation (xsymbols)
  1063   abs  ("\<bar>_\<bar>")
  1064 
  1065 notation (HTML output)
  1066   abs  ("\<bar>_\<bar>")
  1067 
  1068 end
  1069 
  1070 class sgn =
  1071   fixes sgn :: "'a \<Rightarrow> 'a"
  1072 
  1073 class abs_if = minus + uminus + ord + zero + abs +
  1074   assumes abs_if: "\<bar>a\<bar> = (if a < 0 then - a else a)"
  1075 
  1076 class sgn_if = minus + uminus + zero + one + ord + sgn +
  1077   assumes sgn_if: "sgn x = (if x = 0 then 0 else if 0 < x then 1 else - 1)"
  1078 begin
  1079 
  1080 lemma sgn0 [simp]: "sgn 0 = 0"
  1081   by (simp add:sgn_if)
  1082 
  1083 end
  1084 
  1085 class ordered_ab_group_add_abs = ordered_ab_group_add + abs +
  1086   assumes abs_ge_zero [simp]: "\<bar>a\<bar> \<ge> 0"
  1087     and abs_ge_self: "a \<le> \<bar>a\<bar>"
  1088     and abs_leI: "a \<le> b \<Longrightarrow> - a \<le> b \<Longrightarrow> \<bar>a\<bar> \<le> b"
  1089     and abs_minus_cancel [simp]: "\<bar>-a\<bar> = \<bar>a\<bar>"
  1090     and abs_triangle_ineq: "\<bar>a + b\<bar> \<le> \<bar>a\<bar> + \<bar>b\<bar>"
  1091 begin
  1092 
  1093 lemma abs_minus_le_zero: "- \<bar>a\<bar> \<le> 0"
  1094   unfolding neg_le_0_iff_le by simp
  1095 
  1096 lemma abs_of_nonneg [simp]:
  1097   assumes nonneg: "0 \<le> a" shows "\<bar>a\<bar> = a"
  1098 proof (rule antisym)
  1099   from nonneg le_imp_neg_le have "- a \<le> 0" by simp
  1100   from this nonneg have "- a \<le> a" by (rule order_trans)
  1101   then show "\<bar>a\<bar> \<le> a" by (auto intro: abs_leI)
  1102 qed (rule abs_ge_self)
  1103 
  1104 lemma abs_idempotent [simp]: "\<bar>\<bar>a\<bar>\<bar> = \<bar>a\<bar>"
  1105 by (rule antisym)
  1106    (auto intro!: abs_ge_self abs_leI order_trans [of "- \<bar>a\<bar>" 0 "\<bar>a\<bar>"])
  1107 
  1108 lemma abs_eq_0 [simp]: "\<bar>a\<bar> = 0 \<longleftrightarrow> a = 0"
  1109 proof -
  1110   have "\<bar>a\<bar> = 0 \<Longrightarrow> a = 0"
  1111   proof (rule antisym)
  1112     assume zero: "\<bar>a\<bar> = 0"
  1113     with abs_ge_self show "a \<le> 0" by auto
  1114     from zero have "\<bar>-a\<bar> = 0" by simp
  1115     with abs_ge_self [of "- a"] have "- a \<le> 0" by auto
  1116     with neg_le_0_iff_le show "0 \<le> a" by auto
  1117   qed
  1118   then show ?thesis by auto
  1119 qed
  1120 
  1121 lemma abs_zero [simp]: "\<bar>0\<bar> = 0"
  1122 by simp
  1123 
  1124 lemma abs_0_eq [simp, no_atp]: "0 = \<bar>a\<bar> \<longleftrightarrow> a = 0"
  1125 proof -
  1126   have "0 = \<bar>a\<bar> \<longleftrightarrow> \<bar>a\<bar> = 0" by (simp only: eq_ac)
  1127   thus ?thesis by simp
  1128 qed
  1129 
  1130 lemma abs_le_zero_iff [simp]: "\<bar>a\<bar> \<le> 0 \<longleftrightarrow> a = 0" 
  1131 proof
  1132   assume "\<bar>a\<bar> \<le> 0"
  1133   then have "\<bar>a\<bar> = 0" by (rule antisym) simp
  1134   thus "a = 0" by simp
  1135 next
  1136   assume "a = 0"
  1137   thus "\<bar>a\<bar> \<le> 0" by simp
  1138 qed
  1139 
  1140 lemma zero_less_abs_iff [simp]: "0 < \<bar>a\<bar> \<longleftrightarrow> a \<noteq> 0"
  1141 by (simp add: less_le)
  1142 
  1143 lemma abs_not_less_zero [simp]: "\<not> \<bar>a\<bar> < 0"
  1144 proof -
  1145   have a: "\<And>x y. x \<le> y \<Longrightarrow> \<not> y < x" by auto
  1146   show ?thesis by (simp add: a)
  1147 qed
  1148 
  1149 lemma abs_ge_minus_self: "- a \<le> \<bar>a\<bar>"
  1150 proof -
  1151   have "- a \<le> \<bar>-a\<bar>" by (rule abs_ge_self)
  1152   then show ?thesis by simp
  1153 qed
  1154 
  1155 lemma abs_minus_commute: 
  1156   "\<bar>a - b\<bar> = \<bar>b - a\<bar>"
  1157 proof -
  1158   have "\<bar>a - b\<bar> = \<bar>- (a - b)\<bar>" by (simp only: abs_minus_cancel)
  1159   also have "... = \<bar>b - a\<bar>" by simp
  1160   finally show ?thesis .
  1161 qed
  1162 
  1163 lemma abs_of_pos: "0 < a \<Longrightarrow> \<bar>a\<bar> = a"
  1164 by (rule abs_of_nonneg, rule less_imp_le)
  1165 
  1166 lemma abs_of_nonpos [simp]:
  1167   assumes "a \<le> 0" shows "\<bar>a\<bar> = - a"
  1168 proof -
  1169   let ?b = "- a"
  1170   have "- ?b \<le> 0 \<Longrightarrow> \<bar>- ?b\<bar> = - (- ?b)"
  1171   unfolding abs_minus_cancel [of "?b"]
  1172   unfolding neg_le_0_iff_le [of "?b"]
  1173   unfolding minus_minus by (erule abs_of_nonneg)
  1174   then show ?thesis using assms by auto
  1175 qed
  1176   
  1177 lemma abs_of_neg: "a < 0 \<Longrightarrow> \<bar>a\<bar> = - a"
  1178 by (rule abs_of_nonpos, rule less_imp_le)
  1179 
  1180 lemma abs_le_D1: "\<bar>a\<bar> \<le> b \<Longrightarrow> a \<le> b"
  1181 by (insert abs_ge_self, blast intro: order_trans)
  1182 
  1183 lemma abs_le_D2: "\<bar>a\<bar> \<le> b \<Longrightarrow> - a \<le> b"
  1184 by (insert abs_le_D1 [of "- a"], simp)
  1185 
  1186 lemma abs_le_iff: "\<bar>a\<bar> \<le> b \<longleftrightarrow> a \<le> b \<and> - a \<le> b"
  1187 by (blast intro: abs_leI dest: abs_le_D1 abs_le_D2)
  1188 
  1189 lemma abs_triangle_ineq2: "\<bar>a\<bar> - \<bar>b\<bar> \<le> \<bar>a - b\<bar>"
  1190 proof -
  1191   have "\<bar>a\<bar> = \<bar>b + (a - b)\<bar>"
  1192     by (simp add: algebra_simps add_diff_cancel)
  1193   then have "\<bar>a\<bar> \<le> \<bar>b\<bar> + \<bar>a - b\<bar>"
  1194     by (simp add: abs_triangle_ineq)
  1195   then show ?thesis
  1196     by (simp add: algebra_simps)
  1197 qed
  1198 
  1199 lemma abs_triangle_ineq2_sym: "\<bar>a\<bar> - \<bar>b\<bar> \<le> \<bar>b - a\<bar>"
  1200   by (simp only: abs_minus_commute [of b] abs_triangle_ineq2)
  1201 
  1202 lemma abs_triangle_ineq3: "\<bar>\<bar>a\<bar> - \<bar>b\<bar>\<bar> \<le> \<bar>a - b\<bar>"
  1203   by (simp add: abs_le_iff abs_triangle_ineq2 abs_triangle_ineq2_sym)
  1204 
  1205 lemma abs_triangle_ineq4: "\<bar>a - b\<bar> \<le> \<bar>a\<bar> + \<bar>b\<bar>"
  1206 proof -
  1207   have "\<bar>a - b\<bar> = \<bar>a + - b\<bar>" by (subst diff_minus, rule refl)
  1208   also have "... \<le> \<bar>a\<bar> + \<bar>- b\<bar>" by (rule abs_triangle_ineq)
  1209   finally show ?thesis by simp
  1210 qed
  1211 
  1212 lemma abs_diff_triangle_ineq: "\<bar>a + b - (c + d)\<bar> \<le> \<bar>a - c\<bar> + \<bar>b - d\<bar>"
  1213 proof -
  1214   have "\<bar>a + b - (c+d)\<bar> = \<bar>(a-c) + (b-d)\<bar>" by (simp add: diff_minus add_ac)
  1215   also have "... \<le> \<bar>a-c\<bar> + \<bar>b-d\<bar>" by (rule abs_triangle_ineq)
  1216   finally show ?thesis .
  1217 qed
  1218 
  1219 lemma abs_add_abs [simp]:
  1220   "\<bar>\<bar>a\<bar> + \<bar>b\<bar>\<bar> = \<bar>a\<bar> + \<bar>b\<bar>" (is "?L = ?R")
  1221 proof (rule antisym)
  1222   show "?L \<ge> ?R" by(rule abs_ge_self)
  1223 next
  1224   have "?L \<le> \<bar>\<bar>a\<bar>\<bar> + \<bar>\<bar>b\<bar>\<bar>" by(rule abs_triangle_ineq)
  1225   also have "\<dots> = ?R" by simp
  1226   finally show "?L \<le> ?R" .
  1227 qed
  1228 
  1229 end
  1230 
  1231 
  1232 subsection {* Tools setup *}
  1233 
  1234 lemma add_mono_thms_linordered_semiring [no_atp]:
  1235   fixes i j k :: "'a\<Colon>ordered_ab_semigroup_add"
  1236   shows "i \<le> j \<and> k \<le> l \<Longrightarrow> i + k \<le> j + l"
  1237     and "i = j \<and> k \<le> l \<Longrightarrow> i + k \<le> j + l"
  1238     and "i \<le> j \<and> k = l \<Longrightarrow> i + k \<le> j + l"
  1239     and "i = j \<and> k = l \<Longrightarrow> i + k = j + l"
  1240 by (rule add_mono, clarify+)+
  1241 
  1242 lemma add_mono_thms_linordered_field [no_atp]:
  1243   fixes i j k :: "'a\<Colon>ordered_cancel_ab_semigroup_add"
  1244   shows "i < j \<and> k = l \<Longrightarrow> i + k < j + l"
  1245     and "i = j \<and> k < l \<Longrightarrow> i + k < j + l"
  1246     and "i < j \<and> k \<le> l \<Longrightarrow> i + k < j + l"
  1247     and "i \<le> j \<and> k < l \<Longrightarrow> i + k < j + l"
  1248     and "i < j \<and> k < l \<Longrightarrow> i + k < j + l"
  1249 by (auto intro: add_strict_right_mono add_strict_left_mono
  1250   add_less_le_mono add_le_less_mono add_strict_mono)
  1251 
  1252 code_modulename SML
  1253   Groups Arith
  1254 
  1255 code_modulename OCaml
  1256   Groups Arith
  1257 
  1258 code_modulename Haskell
  1259   Groups Arith
  1260 
  1261 
  1262 text {* Legacy *}
  1263 
  1264 lemmas diff_def = diff_minus
  1265 
  1266 end