src/HOL/Groups.thy
author wenzelm
Tue Sep 03 01:12:40 2013 +0200 (2013-09-03)
changeset 53374 a14d2a854c02
parent 52435 6646bb548c6b
child 54147 97a8ff4e4ac9
permissions -rw-r--r--
tuned proofs -- clarified flow of facts wrt. calculation;
     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 class ordered_cancel_comm_monoid_diff = comm_monoid_diff + ordered_ab_semigroup_add_imp_le +
   662   assumes le_iff_add: "a \<le> b \<longleftrightarrow> (\<exists>c. b = a + c)"
   663 begin
   664 
   665 context
   666   fixes a b
   667   assumes "a \<le> b"
   668 begin
   669 
   670 lemma add_diff_inverse:
   671   "a + (b - a) = b"
   672   using `a \<le> b` by (auto simp add: le_iff_add)
   673 
   674 lemma add_diff_assoc:
   675   "c + (b - a) = c + b - a"
   676   using `a \<le> b` by (auto simp add: le_iff_add add_left_commute [of c])
   677 
   678 lemma add_diff_assoc2:
   679   "b - a + c = b + c - a"
   680   using `a \<le> b` by (auto simp add: le_iff_add add_assoc)
   681 
   682 lemma diff_add_assoc:
   683   "c + b - a = c + (b - a)"
   684   using `a \<le> b` by (simp add: add_commute add_diff_assoc)
   685 
   686 lemma diff_add_assoc2:
   687   "b + c - a = b - a + c"
   688   using `a \<le> b`by (simp add: add_commute add_diff_assoc)
   689 
   690 lemma diff_diff_right:
   691   "c - (b - a) = c + a - b"
   692   by (simp add: add_diff_inverse add_diff_cancel_left [of a c "b - a", symmetric] add_commute)
   693 
   694 lemma diff_add:
   695   "b - a + a = b"
   696   by (simp add: add_commute add_diff_inverse)
   697 
   698 lemma le_add_diff:
   699   "c \<le> b + c - a"
   700   by (auto simp add: add_commute diff_add_assoc2 le_iff_add)
   701 
   702 lemma le_imp_diff_is_add:
   703   "a \<le> b \<Longrightarrow> b - a = c \<longleftrightarrow> b = c + a"
   704   by (auto simp add: add_commute add_diff_inverse)
   705 
   706 lemma le_diff_conv2:
   707   "c \<le> b - a \<longleftrightarrow> c + a \<le> b" (is "?P \<longleftrightarrow> ?Q")
   708 proof
   709   assume ?P
   710   then have "c + a \<le> b - a + a" by (rule add_right_mono)
   711   then show ?Q by (simp add: add_diff_inverse add_commute)
   712 next
   713   assume ?Q
   714   then have "a + c \<le> a + (b - a)" by (simp add: add_diff_inverse add_commute)
   715   then show ?P by simp
   716 qed
   717 
   718 end
   719 
   720 end
   721 
   722 
   723 subsection {* Support for reasoning about signs *}
   724 
   725 class ordered_comm_monoid_add =
   726   ordered_cancel_ab_semigroup_add + comm_monoid_add
   727 begin
   728 
   729 lemma add_pos_nonneg:
   730   assumes "0 < a" and "0 \<le> b" shows "0 < a + b"
   731 proof -
   732   have "0 + 0 < a + b" 
   733     using assms by (rule add_less_le_mono)
   734   then show ?thesis by simp
   735 qed
   736 
   737 lemma add_pos_pos:
   738   assumes "0 < a" and "0 < b" shows "0 < a + b"
   739 by (rule add_pos_nonneg) (insert assms, auto)
   740 
   741 lemma add_nonneg_pos:
   742   assumes "0 \<le> a" and "0 < b" shows "0 < a + b"
   743 proof -
   744   have "0 + 0 < a + b" 
   745     using assms by (rule add_le_less_mono)
   746   then show ?thesis by simp
   747 qed
   748 
   749 lemma add_nonneg_nonneg [simp]:
   750   assumes "0 \<le> a" and "0 \<le> b" shows "0 \<le> a + b"
   751 proof -
   752   have "0 + 0 \<le> a + b" 
   753     using assms by (rule add_mono)
   754   then show ?thesis by simp
   755 qed
   756 
   757 lemma add_neg_nonpos:
   758   assumes "a < 0" and "b \<le> 0" shows "a + b < 0"
   759 proof -
   760   have "a + b < 0 + 0"
   761     using assms by (rule add_less_le_mono)
   762   then show ?thesis by simp
   763 qed
   764 
   765 lemma add_neg_neg: 
   766   assumes "a < 0" and "b < 0" shows "a + b < 0"
   767 by (rule add_neg_nonpos) (insert assms, auto)
   768 
   769 lemma add_nonpos_neg:
   770   assumes "a \<le> 0" and "b < 0" shows "a + b < 0"
   771 proof -
   772   have "a + b < 0 + 0"
   773     using assms by (rule add_le_less_mono)
   774   then show ?thesis by simp
   775 qed
   776 
   777 lemma add_nonpos_nonpos:
   778   assumes "a \<le> 0" and "b \<le> 0" shows "a + b \<le> 0"
   779 proof -
   780   have "a + b \<le> 0 + 0"
   781     using assms by (rule add_mono)
   782   then show ?thesis by simp
   783 qed
   784 
   785 lemmas add_sign_intros =
   786   add_pos_nonneg add_pos_pos add_nonneg_pos add_nonneg_nonneg
   787   add_neg_nonpos add_neg_neg add_nonpos_neg add_nonpos_nonpos
   788 
   789 lemma add_nonneg_eq_0_iff:
   790   assumes x: "0 \<le> x" and y: "0 \<le> y"
   791   shows "x + y = 0 \<longleftrightarrow> x = 0 \<and> y = 0"
   792 proof (intro iffI conjI)
   793   have "x = x + 0" by simp
   794   also have "x + 0 \<le> x + y" using y by (rule add_left_mono)
   795   also assume "x + y = 0"
   796   also have "0 \<le> x" using x .
   797   finally show "x = 0" .
   798 next
   799   have "y = 0 + y" by simp
   800   also have "0 + y \<le> x + y" using x by (rule add_right_mono)
   801   also assume "x + y = 0"
   802   also have "0 \<le> y" using y .
   803   finally show "y = 0" .
   804 next
   805   assume "x = 0 \<and> y = 0"
   806   then show "x + y = 0" by simp
   807 qed
   808 
   809 end
   810 
   811 class ordered_ab_group_add =
   812   ab_group_add + ordered_ab_semigroup_add
   813 begin
   814 
   815 subclass ordered_cancel_ab_semigroup_add ..
   816 
   817 subclass ordered_ab_semigroup_add_imp_le
   818 proof
   819   fix a b c :: 'a
   820   assume "c + a \<le> c + b"
   821   hence "(-c) + (c + a) \<le> (-c) + (c + b)" by (rule add_left_mono)
   822   hence "((-c) + c) + a \<le> ((-c) + c) + b" by (simp only: add_assoc)
   823   thus "a \<le> b" by simp
   824 qed
   825 
   826 subclass ordered_comm_monoid_add ..
   827 
   828 lemma max_diff_distrib_left:
   829   shows "max x y - z = max (x - z) (y - z)"
   830 by (simp add: diff_minus, rule max_add_distrib_left) 
   831 
   832 lemma min_diff_distrib_left:
   833   shows "min x y - z = min (x - z) (y - z)"
   834 by (simp add: diff_minus, rule min_add_distrib_left) 
   835 
   836 lemma le_imp_neg_le:
   837   assumes "a \<le> b" shows "-b \<le> -a"
   838 proof -
   839   have "-a+a \<le> -a+b" using `a \<le> b` by (rule add_left_mono) 
   840   hence "0 \<le> -a+b" by simp
   841   hence "0 + (-b) \<le> (-a + b) + (-b)" by (rule add_right_mono) 
   842   thus ?thesis by (simp add: add_assoc)
   843 qed
   844 
   845 lemma neg_le_iff_le [simp]: "- b \<le> - a \<longleftrightarrow> a \<le> b"
   846 proof 
   847   assume "- b \<le> - a"
   848   hence "- (- a) \<le> - (- b)" by (rule le_imp_neg_le)
   849   thus "a\<le>b" by simp
   850 next
   851   assume "a\<le>b"
   852   thus "-b \<le> -a" by (rule le_imp_neg_le)
   853 qed
   854 
   855 lemma neg_le_0_iff_le [simp]: "- a \<le> 0 \<longleftrightarrow> 0 \<le> a"
   856 by (subst neg_le_iff_le [symmetric], simp)
   857 
   858 lemma neg_0_le_iff_le [simp]: "0 \<le> - a \<longleftrightarrow> a \<le> 0"
   859 by (subst neg_le_iff_le [symmetric], simp)
   860 
   861 lemma neg_less_iff_less [simp]: "- b < - a \<longleftrightarrow> a < b"
   862 by (force simp add: less_le) 
   863 
   864 lemma neg_less_0_iff_less [simp]: "- a < 0 \<longleftrightarrow> 0 < a"
   865 by (subst neg_less_iff_less [symmetric], simp)
   866 
   867 lemma neg_0_less_iff_less [simp]: "0 < - a \<longleftrightarrow> a < 0"
   868 by (subst neg_less_iff_less [symmetric], simp)
   869 
   870 text{*The next several equations can make the simplifier loop!*}
   871 
   872 lemma less_minus_iff: "a < - b \<longleftrightarrow> b < - a"
   873 proof -
   874   have "(- (-a) < - b) = (b < - a)" by (rule neg_less_iff_less)
   875   thus ?thesis by simp
   876 qed
   877 
   878 lemma minus_less_iff: "- a < b \<longleftrightarrow> - b < a"
   879 proof -
   880   have "(- a < - (-b)) = (- b < a)" by (rule neg_less_iff_less)
   881   thus ?thesis by simp
   882 qed
   883 
   884 lemma le_minus_iff: "a \<le> - b \<longleftrightarrow> b \<le> - a"
   885 proof -
   886   have mm: "!! a (b::'a). (-(-a)) < -b \<Longrightarrow> -(-b) < -a" by (simp only: minus_less_iff)
   887   have "(- (- a) <= -b) = (b <= - a)" 
   888     apply (auto simp only: le_less)
   889     apply (drule mm)
   890     apply (simp_all)
   891     apply (drule mm[simplified], assumption)
   892     done
   893   then show ?thesis by simp
   894 qed
   895 
   896 lemma minus_le_iff: "- a \<le> b \<longleftrightarrow> - b \<le> a"
   897 by (auto simp add: le_less minus_less_iff)
   898 
   899 lemma diff_less_0_iff_less [simp, no_atp]:
   900   "a - b < 0 \<longleftrightarrow> a < b"
   901 proof -
   902   have "a - b < 0 \<longleftrightarrow> a + (- b) < b + (- b)" by (simp add: diff_minus)
   903   also have "... \<longleftrightarrow> a < b" by (simp only: add_less_cancel_right)
   904   finally show ?thesis .
   905 qed
   906 
   907 lemmas less_iff_diff_less_0 = diff_less_0_iff_less [symmetric]
   908 
   909 lemma diff_less_eq[algebra_simps, field_simps]: "a - b < c \<longleftrightarrow> a < c + b"
   910 apply (subst less_iff_diff_less_0 [of a])
   911 apply (rule less_iff_diff_less_0 [of _ c, THEN ssubst])
   912 apply (simp add: diff_minus add_ac)
   913 done
   914 
   915 lemma less_diff_eq[algebra_simps, field_simps]: "a < c - b \<longleftrightarrow> a + b < c"
   916 apply (subst less_iff_diff_less_0 [of "a + b"])
   917 apply (subst less_iff_diff_less_0 [of a])
   918 apply (simp add: diff_minus add_ac)
   919 done
   920 
   921 lemma diff_le_eq[algebra_simps, field_simps]: "a - b \<le> c \<longleftrightarrow> a \<le> c + b"
   922 by (auto simp add: le_less diff_less_eq diff_add_cancel add_diff_cancel)
   923 
   924 lemma le_diff_eq[algebra_simps, field_simps]: "a \<le> c - b \<longleftrightarrow> a + b \<le> c"
   925 by (auto simp add: le_less less_diff_eq diff_add_cancel add_diff_cancel)
   926 
   927 lemma diff_le_0_iff_le [simp, no_atp]:
   928   "a - b \<le> 0 \<longleftrightarrow> a \<le> b"
   929   by (simp add: algebra_simps)
   930 
   931 lemmas le_iff_diff_le_0 = diff_le_0_iff_le [symmetric]
   932 
   933 lemma diff_eq_diff_less:
   934   "a - b = c - d \<Longrightarrow> a < b \<longleftrightarrow> c < d"
   935   by (auto simp only: less_iff_diff_less_0 [of a b] less_iff_diff_less_0 [of c d])
   936 
   937 lemma diff_eq_diff_less_eq:
   938   "a - b = c - d \<Longrightarrow> a \<le> b \<longleftrightarrow> c \<le> d"
   939   by (auto simp only: le_iff_diff_le_0 [of a b] le_iff_diff_le_0 [of c d])
   940 
   941 end
   942 
   943 ML_file "Tools/group_cancel.ML"
   944 
   945 simproc_setup group_cancel_add ("a + b::'a::ab_group_add") =
   946   {* fn phi => fn ss => try Group_Cancel.cancel_add_conv *}
   947 
   948 simproc_setup group_cancel_diff ("a - b::'a::ab_group_add") =
   949   {* fn phi => fn ss => try Group_Cancel.cancel_diff_conv *}
   950 
   951 simproc_setup group_cancel_eq ("a = (b::'a::ab_group_add)") =
   952   {* fn phi => fn ss => try Group_Cancel.cancel_eq_conv *}
   953 
   954 simproc_setup group_cancel_le ("a \<le> (b::'a::ordered_ab_group_add)") =
   955   {* fn phi => fn ss => try Group_Cancel.cancel_le_conv *}
   956 
   957 simproc_setup group_cancel_less ("a < (b::'a::ordered_ab_group_add)") =
   958   {* fn phi => fn ss => try Group_Cancel.cancel_less_conv *}
   959 
   960 class linordered_ab_semigroup_add =
   961   linorder + ordered_ab_semigroup_add
   962 
   963 class linordered_cancel_ab_semigroup_add =
   964   linorder + ordered_cancel_ab_semigroup_add
   965 begin
   966 
   967 subclass linordered_ab_semigroup_add ..
   968 
   969 subclass ordered_ab_semigroup_add_imp_le
   970 proof
   971   fix a b c :: 'a
   972   assume le: "c + a <= c + b"  
   973   show "a <= b"
   974   proof (rule ccontr)
   975     assume w: "~ a \<le> b"
   976     hence "b <= a" by (simp add: linorder_not_le)
   977     hence le2: "c + b <= c + a" by (rule add_left_mono)
   978     have "a = b" 
   979       apply (insert le)
   980       apply (insert le2)
   981       apply (drule antisym, simp_all)
   982       done
   983     with w show False 
   984       by (simp add: linorder_not_le [symmetric])
   985   qed
   986 qed
   987 
   988 end
   989 
   990 class linordered_ab_group_add = linorder + ordered_ab_group_add
   991 begin
   992 
   993 subclass linordered_cancel_ab_semigroup_add ..
   994 
   995 lemma neg_less_eq_nonneg [simp]:
   996   "- a \<le> a \<longleftrightarrow> 0 \<le> a"
   997 proof
   998   assume A: "- a \<le> a" show "0 \<le> a"
   999   proof (rule classical)
  1000     assume "\<not> 0 \<le> a"
  1001     then have "a < 0" by auto
  1002     with A have "- a < 0" by (rule le_less_trans)
  1003     then show ?thesis by auto
  1004   qed
  1005 next
  1006   assume A: "0 \<le> a" show "- a \<le> a"
  1007   proof (rule order_trans)
  1008     show "- a \<le> 0" using A by (simp add: minus_le_iff)
  1009   next
  1010     show "0 \<le> a" using A .
  1011   qed
  1012 qed
  1013 
  1014 lemma neg_less_nonneg [simp]:
  1015   "- a < a \<longleftrightarrow> 0 < a"
  1016 proof
  1017   assume A: "- a < a" show "0 < a"
  1018   proof (rule classical)
  1019     assume "\<not> 0 < a"
  1020     then have "a \<le> 0" by auto
  1021     with A have "- a < 0" by (rule less_le_trans)
  1022     then show ?thesis by auto
  1023   qed
  1024 next
  1025   assume A: "0 < a" show "- a < a"
  1026   proof (rule less_trans)
  1027     show "- a < 0" using A by (simp add: minus_le_iff)
  1028   next
  1029     show "0 < a" using A .
  1030   qed
  1031 qed
  1032 
  1033 lemma less_eq_neg_nonpos [simp]:
  1034   "a \<le> - a \<longleftrightarrow> a \<le> 0"
  1035 proof
  1036   assume A: "a \<le> - a" show "a \<le> 0"
  1037   proof (rule classical)
  1038     assume "\<not> a \<le> 0"
  1039     then have "0 < a" by auto
  1040     then have "0 < - a" using A by (rule less_le_trans)
  1041     then show ?thesis by auto
  1042   qed
  1043 next
  1044   assume A: "a \<le> 0" show "a \<le> - a"
  1045   proof (rule order_trans)
  1046     show "0 \<le> - a" using A by (simp add: minus_le_iff)
  1047   next
  1048     show "a \<le> 0" using A .
  1049   qed
  1050 qed
  1051 
  1052 lemma equal_neg_zero [simp]:
  1053   "a = - a \<longleftrightarrow> a = 0"
  1054 proof
  1055   assume "a = 0" then show "a = - a" by simp
  1056 next
  1057   assume A: "a = - a" show "a = 0"
  1058   proof (cases "0 \<le> a")
  1059     case True with A have "0 \<le> - a" by auto
  1060     with le_minus_iff have "a \<le> 0" by simp
  1061     with True show ?thesis by (auto intro: order_trans)
  1062   next
  1063     case False then have B: "a \<le> 0" by auto
  1064     with A have "- a \<le> 0" by auto
  1065     with B show ?thesis by (auto intro: order_trans)
  1066   qed
  1067 qed
  1068 
  1069 lemma neg_equal_zero [simp]:
  1070   "- a = a \<longleftrightarrow> a = 0"
  1071   by (auto dest: sym)
  1072 
  1073 lemma double_zero [simp]:
  1074   "a + a = 0 \<longleftrightarrow> a = 0"
  1075 proof
  1076   assume assm: "a + a = 0"
  1077   then have a: "- a = a" by (rule minus_unique)
  1078   then show "a = 0" by (simp only: neg_equal_zero)
  1079 qed simp
  1080 
  1081 lemma double_zero_sym [simp]:
  1082   "0 = a + a \<longleftrightarrow> a = 0"
  1083   by (rule, drule sym) simp_all
  1084 
  1085 lemma zero_less_double_add_iff_zero_less_single_add [simp]:
  1086   "0 < a + a \<longleftrightarrow> 0 < a"
  1087 proof
  1088   assume "0 < a + a"
  1089   then have "0 - a < a" by (simp only: diff_less_eq)
  1090   then have "- a < a" by simp
  1091   then show "0 < a" by (simp only: neg_less_nonneg)
  1092 next
  1093   assume "0 < a"
  1094   with this have "0 + 0 < a + a"
  1095     by (rule add_strict_mono)
  1096   then show "0 < a + a" by simp
  1097 qed
  1098 
  1099 lemma zero_le_double_add_iff_zero_le_single_add [simp]:
  1100   "0 \<le> a + a \<longleftrightarrow> 0 \<le> a"
  1101   by (auto simp add: le_less)
  1102 
  1103 lemma double_add_less_zero_iff_single_add_less_zero [simp]:
  1104   "a + a < 0 \<longleftrightarrow> a < 0"
  1105 proof -
  1106   have "\<not> a + a < 0 \<longleftrightarrow> \<not> a < 0"
  1107     by (simp add: not_less)
  1108   then show ?thesis by simp
  1109 qed
  1110 
  1111 lemma double_add_le_zero_iff_single_add_le_zero [simp]:
  1112   "a + a \<le> 0 \<longleftrightarrow> a \<le> 0" 
  1113 proof -
  1114   have "\<not> a + a \<le> 0 \<longleftrightarrow> \<not> a \<le> 0"
  1115     by (simp add: not_le)
  1116   then show ?thesis by simp
  1117 qed
  1118 
  1119 lemma le_minus_self_iff:
  1120   "a \<le> - a \<longleftrightarrow> a \<le> 0"
  1121 proof -
  1122   from add_le_cancel_left [of "- a" "a + a" 0]
  1123   have "a \<le> - a \<longleftrightarrow> a + a \<le> 0" 
  1124     by (simp add: add_assoc [symmetric])
  1125   thus ?thesis by simp
  1126 qed
  1127 
  1128 lemma minus_le_self_iff:
  1129   "- a \<le> a \<longleftrightarrow> 0 \<le> a"
  1130 proof -
  1131   from add_le_cancel_left [of "- a" 0 "a + a"]
  1132   have "- a \<le> a \<longleftrightarrow> 0 \<le> a + a" 
  1133     by (simp add: add_assoc [symmetric])
  1134   thus ?thesis by simp
  1135 qed
  1136 
  1137 lemma minus_max_eq_min:
  1138   "- max x y = min (-x) (-y)"
  1139   by (auto simp add: max_def min_def)
  1140 
  1141 lemma minus_min_eq_max:
  1142   "- min x y = max (-x) (-y)"
  1143   by (auto simp add: max_def min_def)
  1144 
  1145 end
  1146 
  1147 context ordered_comm_monoid_add
  1148 begin
  1149 
  1150 lemma add_increasing:
  1151   "0 \<le> a \<Longrightarrow> b \<le> c \<Longrightarrow> b \<le> a + c"
  1152   by (insert add_mono [of 0 a b c], simp)
  1153 
  1154 lemma add_increasing2:
  1155   "0 \<le> c \<Longrightarrow> b \<le> a \<Longrightarrow> b \<le> a + c"
  1156   by (simp add: add_increasing add_commute [of a])
  1157 
  1158 lemma add_strict_increasing:
  1159   "0 < a \<Longrightarrow> b \<le> c \<Longrightarrow> b < a + c"
  1160   by (insert add_less_le_mono [of 0 a b c], simp)
  1161 
  1162 lemma add_strict_increasing2:
  1163   "0 \<le> a \<Longrightarrow> b < c \<Longrightarrow> b < a + c"
  1164   by (insert add_le_less_mono [of 0 a b c], simp)
  1165 
  1166 end
  1167 
  1168 class abs =
  1169   fixes abs :: "'a \<Rightarrow> 'a"
  1170 begin
  1171 
  1172 notation (xsymbols)
  1173   abs  ("\<bar>_\<bar>")
  1174 
  1175 notation (HTML output)
  1176   abs  ("\<bar>_\<bar>")
  1177 
  1178 end
  1179 
  1180 class sgn =
  1181   fixes sgn :: "'a \<Rightarrow> 'a"
  1182 
  1183 class abs_if = minus + uminus + ord + zero + abs +
  1184   assumes abs_if: "\<bar>a\<bar> = (if a < 0 then - a else a)"
  1185 
  1186 class sgn_if = minus + uminus + zero + one + ord + sgn +
  1187   assumes sgn_if: "sgn x = (if x = 0 then 0 else if 0 < x then 1 else - 1)"
  1188 begin
  1189 
  1190 lemma sgn0 [simp]: "sgn 0 = 0"
  1191   by (simp add:sgn_if)
  1192 
  1193 end
  1194 
  1195 class ordered_ab_group_add_abs = ordered_ab_group_add + abs +
  1196   assumes abs_ge_zero [simp]: "\<bar>a\<bar> \<ge> 0"
  1197     and abs_ge_self: "a \<le> \<bar>a\<bar>"
  1198     and abs_leI: "a \<le> b \<Longrightarrow> - a \<le> b \<Longrightarrow> \<bar>a\<bar> \<le> b"
  1199     and abs_minus_cancel [simp]: "\<bar>-a\<bar> = \<bar>a\<bar>"
  1200     and abs_triangle_ineq: "\<bar>a + b\<bar> \<le> \<bar>a\<bar> + \<bar>b\<bar>"
  1201 begin
  1202 
  1203 lemma abs_minus_le_zero: "- \<bar>a\<bar> \<le> 0"
  1204   unfolding neg_le_0_iff_le by simp
  1205 
  1206 lemma abs_of_nonneg [simp]:
  1207   assumes nonneg: "0 \<le> a" shows "\<bar>a\<bar> = a"
  1208 proof (rule antisym)
  1209   from nonneg le_imp_neg_le have "- a \<le> 0" by simp
  1210   from this nonneg have "- a \<le> a" by (rule order_trans)
  1211   then show "\<bar>a\<bar> \<le> a" by (auto intro: abs_leI)
  1212 qed (rule abs_ge_self)
  1213 
  1214 lemma abs_idempotent [simp]: "\<bar>\<bar>a\<bar>\<bar> = \<bar>a\<bar>"
  1215 by (rule antisym)
  1216    (auto intro!: abs_ge_self abs_leI order_trans [of "- \<bar>a\<bar>" 0 "\<bar>a\<bar>"])
  1217 
  1218 lemma abs_eq_0 [simp]: "\<bar>a\<bar> = 0 \<longleftrightarrow> a = 0"
  1219 proof -
  1220   have "\<bar>a\<bar> = 0 \<Longrightarrow> a = 0"
  1221   proof (rule antisym)
  1222     assume zero: "\<bar>a\<bar> = 0"
  1223     with abs_ge_self show "a \<le> 0" by auto
  1224     from zero have "\<bar>-a\<bar> = 0" by simp
  1225     with abs_ge_self [of "- a"] have "- a \<le> 0" by auto
  1226     with neg_le_0_iff_le show "0 \<le> a" by auto
  1227   qed
  1228   then show ?thesis by auto
  1229 qed
  1230 
  1231 lemma abs_zero [simp]: "\<bar>0\<bar> = 0"
  1232 by simp
  1233 
  1234 lemma abs_0_eq [simp, no_atp]: "0 = \<bar>a\<bar> \<longleftrightarrow> a = 0"
  1235 proof -
  1236   have "0 = \<bar>a\<bar> \<longleftrightarrow> \<bar>a\<bar> = 0" by (simp only: eq_ac)
  1237   thus ?thesis by simp
  1238 qed
  1239 
  1240 lemma abs_le_zero_iff [simp]: "\<bar>a\<bar> \<le> 0 \<longleftrightarrow> a = 0" 
  1241 proof
  1242   assume "\<bar>a\<bar> \<le> 0"
  1243   then have "\<bar>a\<bar> = 0" by (rule antisym) simp
  1244   thus "a = 0" by simp
  1245 next
  1246   assume "a = 0"
  1247   thus "\<bar>a\<bar> \<le> 0" by simp
  1248 qed
  1249 
  1250 lemma zero_less_abs_iff [simp]: "0 < \<bar>a\<bar> \<longleftrightarrow> a \<noteq> 0"
  1251 by (simp add: less_le)
  1252 
  1253 lemma abs_not_less_zero [simp]: "\<not> \<bar>a\<bar> < 0"
  1254 proof -
  1255   have a: "\<And>x y. x \<le> y \<Longrightarrow> \<not> y < x" by auto
  1256   show ?thesis by (simp add: a)
  1257 qed
  1258 
  1259 lemma abs_ge_minus_self: "- a \<le> \<bar>a\<bar>"
  1260 proof -
  1261   have "- a \<le> \<bar>-a\<bar>" by (rule abs_ge_self)
  1262   then show ?thesis by simp
  1263 qed
  1264 
  1265 lemma abs_minus_commute: 
  1266   "\<bar>a - b\<bar> = \<bar>b - a\<bar>"
  1267 proof -
  1268   have "\<bar>a - b\<bar> = \<bar>- (a - b)\<bar>" by (simp only: abs_minus_cancel)
  1269   also have "... = \<bar>b - a\<bar>" by simp
  1270   finally show ?thesis .
  1271 qed
  1272 
  1273 lemma abs_of_pos: "0 < a \<Longrightarrow> \<bar>a\<bar> = a"
  1274 by (rule abs_of_nonneg, rule less_imp_le)
  1275 
  1276 lemma abs_of_nonpos [simp]:
  1277   assumes "a \<le> 0" shows "\<bar>a\<bar> = - a"
  1278 proof -
  1279   let ?b = "- a"
  1280   have "- ?b \<le> 0 \<Longrightarrow> \<bar>- ?b\<bar> = - (- ?b)"
  1281   unfolding abs_minus_cancel [of "?b"]
  1282   unfolding neg_le_0_iff_le [of "?b"]
  1283   unfolding minus_minus by (erule abs_of_nonneg)
  1284   then show ?thesis using assms by auto
  1285 qed
  1286   
  1287 lemma abs_of_neg: "a < 0 \<Longrightarrow> \<bar>a\<bar> = - a"
  1288 by (rule abs_of_nonpos, rule less_imp_le)
  1289 
  1290 lemma abs_le_D1: "\<bar>a\<bar> \<le> b \<Longrightarrow> a \<le> b"
  1291 by (insert abs_ge_self, blast intro: order_trans)
  1292 
  1293 lemma abs_le_D2: "\<bar>a\<bar> \<le> b \<Longrightarrow> - a \<le> b"
  1294 by (insert abs_le_D1 [of "- a"], simp)
  1295 
  1296 lemma abs_le_iff: "\<bar>a\<bar> \<le> b \<longleftrightarrow> a \<le> b \<and> - a \<le> b"
  1297 by (blast intro: abs_leI dest: abs_le_D1 abs_le_D2)
  1298 
  1299 lemma abs_triangle_ineq2: "\<bar>a\<bar> - \<bar>b\<bar> \<le> \<bar>a - b\<bar>"
  1300 proof -
  1301   have "\<bar>a\<bar> = \<bar>b + (a - b)\<bar>"
  1302     by (simp add: algebra_simps add_diff_cancel)
  1303   then have "\<bar>a\<bar> \<le> \<bar>b\<bar> + \<bar>a - b\<bar>"
  1304     by (simp add: abs_triangle_ineq)
  1305   then show ?thesis
  1306     by (simp add: algebra_simps)
  1307 qed
  1308 
  1309 lemma abs_triangle_ineq2_sym: "\<bar>a\<bar> - \<bar>b\<bar> \<le> \<bar>b - a\<bar>"
  1310   by (simp only: abs_minus_commute [of b] abs_triangle_ineq2)
  1311 
  1312 lemma abs_triangle_ineq3: "\<bar>\<bar>a\<bar> - \<bar>b\<bar>\<bar> \<le> \<bar>a - b\<bar>"
  1313   by (simp add: abs_le_iff abs_triangle_ineq2 abs_triangle_ineq2_sym)
  1314 
  1315 lemma abs_triangle_ineq4: "\<bar>a - b\<bar> \<le> \<bar>a\<bar> + \<bar>b\<bar>"
  1316 proof -
  1317   have "\<bar>a - b\<bar> = \<bar>a + - b\<bar>" by (subst diff_minus, rule refl)
  1318   also have "... \<le> \<bar>a\<bar> + \<bar>- b\<bar>" by (rule abs_triangle_ineq)
  1319   finally show ?thesis by simp
  1320 qed
  1321 
  1322 lemma abs_diff_triangle_ineq: "\<bar>a + b - (c + d)\<bar> \<le> \<bar>a - c\<bar> + \<bar>b - d\<bar>"
  1323 proof -
  1324   have "\<bar>a + b - (c+d)\<bar> = \<bar>(a-c) + (b-d)\<bar>" by (simp add: diff_minus add_ac)
  1325   also have "... \<le> \<bar>a-c\<bar> + \<bar>b-d\<bar>" by (rule abs_triangle_ineq)
  1326   finally show ?thesis .
  1327 qed
  1328 
  1329 lemma abs_add_abs [simp]:
  1330   "\<bar>\<bar>a\<bar> + \<bar>b\<bar>\<bar> = \<bar>a\<bar> + \<bar>b\<bar>" (is "?L = ?R")
  1331 proof (rule antisym)
  1332   show "?L \<ge> ?R" by(rule abs_ge_self)
  1333 next
  1334   have "?L \<le> \<bar>\<bar>a\<bar>\<bar> + \<bar>\<bar>b\<bar>\<bar>" by(rule abs_triangle_ineq)
  1335   also have "\<dots> = ?R" by simp
  1336   finally show "?L \<le> ?R" .
  1337 qed
  1338 
  1339 end
  1340 
  1341 
  1342 subsection {* Tools setup *}
  1343 
  1344 lemma add_mono_thms_linordered_semiring [no_atp]:
  1345   fixes i j k :: "'a\<Colon>ordered_ab_semigroup_add"
  1346   shows "i \<le> j \<and> k \<le> l \<Longrightarrow> i + k \<le> j + l"
  1347     and "i = j \<and> k \<le> l \<Longrightarrow> i + k \<le> j + l"
  1348     and "i \<le> j \<and> k = l \<Longrightarrow> i + k \<le> j + l"
  1349     and "i = j \<and> k = l \<Longrightarrow> i + k = j + l"
  1350 by (rule add_mono, clarify+)+
  1351 
  1352 lemma add_mono_thms_linordered_field [no_atp]:
  1353   fixes i j k :: "'a\<Colon>ordered_cancel_ab_semigroup_add"
  1354   shows "i < j \<and> k = l \<Longrightarrow> i + k < j + l"
  1355     and "i = j \<and> k < l \<Longrightarrow> i + k < j + l"
  1356     and "i < j \<and> k \<le> l \<Longrightarrow> i + k < j + l"
  1357     and "i \<le> j \<and> k < l \<Longrightarrow> i + k < j + l"
  1358     and "i < j \<and> k < l \<Longrightarrow> i + k < j + l"
  1359 by (auto intro: add_strict_right_mono add_strict_left_mono
  1360   add_less_le_mono add_le_less_mono add_strict_mono)
  1361 
  1362 code_identifier
  1363   code_module Groups \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith
  1364 
  1365 
  1366 text {* Legacy *}
  1367 
  1368 lemmas diff_def = diff_minus
  1369 
  1370 end
  1371