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