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