src/HOL/Groups.thy
 author wenzelm Mon Aug 22 23:39:05 2011 +0200 (2011-08-22) changeset 44433 9fbee4aab115 parent 44348 40101794c52f child 44848 f4d0b060c7ca permissions -rw-r--r--
special treatment of structure index 1 in Pure, including legacy warning;
1 (*  Title:   HOL/Groups.thy
2     Author:  Gertrud Bauer, Steven Obua, Lawrence C Paulson, Markus Wenzel, Jeremy Avigad
3 *)
5 header {* Groups, also combined with orderings *}
7 theory Groups
8 imports Orderings
9 uses ("Tools/abel_cancel.ML")
10 begin
12 subsection {* Fact collections *}
14 ML {*
15 structure Ac_Simps = Named_Thms(
16   val name = "ac_simps"
17   val description = "associativity and commutativity simplification rules"
18 )
19 *}
21 setup Ac_Simps.setup
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.
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}. *}
32 ML {*
33 structure Algebra_Simps = Named_Thms(
34   val name = "algebra_simps"
35   val description = "algebra simplification rules"
36 )
37 *}
39 setup Algebra_Simps.setup
41 text{* Lemmas @{text field_simps} multiply with denominators in (in)equations
42 if they can be proved to be non-zero (for equations) or positive/negative
43 (for inequations). Can be too aggressive and is therefore separate from the
44 more benign @{text algebra_simps}. *}
46 ML {*
47 structure Field_Simps = Named_Thms(
48   val name = "field_simps"
49   val description = "algebra simplification rules for fields"
50 )
51 *}
53 setup Field_Simps.setup
56 subsection {* Abstract structures *}
58 text {*
59   These locales provide basic structures for interpretation into
60   bigger structures;  extensions require careful thinking, otherwise
61   undesired effects may occur due to interpretation.
62 *}
64 locale semigroup =
65   fixes f :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "*" 70)
66   assumes assoc [ac_simps]: "a * b * c = a * (b * c)"
68 locale abel_semigroup = semigroup +
69   assumes commute [ac_simps]: "a * b = b * a"
70 begin
72 lemma left_commute [ac_simps]:
73   "b * (a * c) = a * (b * c)"
74 proof -
75   have "(b * a) * c = (a * b) * c"
76     by (simp only: commute)
77   then show ?thesis
78     by (simp only: assoc)
79 qed
81 end
83 locale monoid = semigroup +
84   fixes z :: 'a ("1")
85   assumes left_neutral [simp]: "1 * a = a"
86   assumes right_neutral [simp]: "a * 1 = a"
88 locale comm_monoid = abel_semigroup +
89   fixes z :: 'a ("1")
90   assumes comm_neutral: "a * 1 = a"
92 sublocale comm_monoid < monoid proof
93 qed (simp_all add: commute comm_neutral)
96 subsection {* Generic operations *}
98 class zero =
99   fixes zero :: 'a  ("0")
101 class one =
102   fixes one  :: 'a  ("1")
104 hide_const (open) zero one
106 lemma Let_0 [simp]: "Let 0 f = f 0"
107   unfolding Let_def ..
109 lemma Let_1 [simp]: "Let 1 f = f 1"
110   unfolding Let_def ..
112 setup {*
114     (fn Const(@{const_name Groups.zero}, _) => true
115       | Const(@{const_name Groups.one}, _) => true
116       | _ => false)
117 *}
119 simproc_setup reorient_zero ("0 = x") = Reorient_Proc.proc
120 simproc_setup reorient_one ("1 = x") = Reorient_Proc.proc
123   let
124     fun tr' c = (c, fn ctxt => fn T => fn ts =>
125       if not (null ts) orelse T = dummyT
126         orelse not (Config.get ctxt show_types) andalso can Term.dest_Type T
127       then raise Match
128       else
129         Syntax.const @{syntax_const "_constrain"} $Syntax.const c$
130           Syntax_Phases.term_of_typ ctxt T);
131   in map tr' [@{const_syntax Groups.one}, @{const_syntax Groups.zero}] end;
132 *} -- {* show types that are presumably too general *}
134 class plus =
135   fixes plus :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "+" 65)
137 class minus =
138   fixes minus :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "-" 65)
140 class uminus =
141   fixes uminus :: "'a \<Rightarrow> 'a"  ("- _" [81] 80)
143 class times =
144   fixes times :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "*" 70)
147 subsection {* Semigroups and Monoids *}
149 class semigroup_add = plus +
150   assumes add_assoc [algebra_simps, field_simps]: "(a + b) + c = a + (b + c)"
156   assumes add_commute [algebra_simps, field_simps]: "a + b = b + a"
162 begin
168 end
172 class semigroup_mult = times +
173   assumes mult_assoc [algebra_simps, field_simps]: "(a * b) * c = a * (b * c)"
175 sublocale semigroup_mult < mult!: semigroup times proof
176 qed (fact mult_assoc)
178 class ab_semigroup_mult = semigroup_mult +
179   assumes mult_commute [algebra_simps, field_simps]: "a * b = b * a"
181 sublocale ab_semigroup_mult < mult!: abel_semigroup times proof
182 qed (fact mult_commute)
184 context ab_semigroup_mult
185 begin
187 lemmas mult_left_commute [algebra_simps, field_simps] = mult.left_commute
189 theorems mult_ac = mult_assoc mult_commute mult_left_commute
191 end
193 theorems mult_ac = mult_assoc mult_commute mult_left_commute
196   assumes add_0_left: "0 + a = a"
197     and add_0_right: "a + 0 = a"
202 lemma zero_reorient: "0 = x \<longleftrightarrow> x = 0"
203 by (rule eq_commute)
206   assumes add_0: "0 + a = a"
214 class monoid_mult = one + semigroup_mult +
215   assumes mult_1_left: "1 * a  = a"
216     and mult_1_right: "a * 1 = a"
218 sublocale monoid_mult < mult!: monoid times 1 proof
219 qed (fact mult_1_left mult_1_right)+
221 lemma one_reorient: "1 = x \<longleftrightarrow> x = 1"
222 by (rule eq_commute)
224 class comm_monoid_mult = one + ab_semigroup_mult +
225   assumes mult_1: "1 * a = a"
227 sublocale comm_monoid_mult < mult!: comm_monoid times 1 proof
228 qed (insert mult_1, simp add: ac_simps)
230 subclass (in comm_monoid_mult) monoid_mult proof
231 qed (fact mult.left_neutral mult.right_neutral)+
234   assumes add_left_imp_eq: "a + b = a + c \<Longrightarrow> b = c"
235   assumes add_right_imp_eq: "b + a = c + a \<Longrightarrow> b = c"
236 begin
239   "a + b = a + c \<longleftrightarrow> b = c"
243   "b + a = c + a \<longleftrightarrow> b = c"
246 end
249   assumes add_imp_eq: "a + b = a + c \<Longrightarrow> b = c"
250 begin
253 proof
254   fix a b c :: 'a
255   assume "a + b = a + c"
256   then show "b = c" by (rule add_imp_eq)
257 next
258   fix a b c :: 'a
259   assume "b + a = c + a"
260   then have "a + b = a + c" by (simp only: add_commute)
261   then show "b = c" by (rule add_imp_eq)
262 qed
264 end
269 subsection {* Groups *}
272   assumes left_minus [simp]: "- a + a = 0"
273   assumes diff_minus: "a - b = a + (- b)"
274 begin
276 lemma minus_unique:
277   assumes "a + b = 0" shows "- a = b"
278 proof -
279   have "- a = - a + (a + b)" using assms by simp
281   finally show ?thesis .
282 qed
285 lemmas equals_zero_I = minus_unique (* legacy name *)
287 lemma minus_zero [simp]: "- 0 = 0"
288 proof -
289   have "0 + 0 = 0" by (rule add_0_right)
290   thus "- 0 = 0" by (rule minus_unique)
291 qed
293 lemma minus_minus [simp]: "- (- a) = a"
294 proof -
295   have "- a + a = 0" by (rule left_minus)
296   thus "- (- a) = a" by (rule minus_unique)
297 qed
299 lemma right_minus [simp]: "a + - a = 0"
300 proof -
301   have "a + - a = - (- a) + - a" by simp
302   also have "\<dots> = 0" by (rule left_minus)
303   finally show ?thesis .
304 qed
307 proof
308   fix a b c :: 'a
309   assume "a + b = a + c"
310   then have "- a + a + b = - a + a + c"
312   then show "b = c" by simp
313 next
314   fix a b c :: 'a
315   assume "b + a = c + a"
316   then have "b + a + - a = c + a  + - a" by simp
317   then show "b = c" unfolding add_assoc by simp
318 qed
320 lemma minus_add_cancel: "- a + (a + b) = b"
323 lemma add_minus_cancel: "a + (- a + b) = b"
326 lemma minus_add: "- (a + b) = - b + - a"
327 proof -
328   have "(a + b) + (- b + - a) = 0"
330   thus "- (a + b) = - b + - a"
331     by (rule minus_unique)
332 qed
334 lemma right_minus_eq: "a - b = 0 \<longleftrightarrow> a = b"
335 proof
336   assume "a - b = 0"
337   have "a = (a - b) + b" by (simp add:diff_minus add_assoc)
338   also have "\<dots> = b" using a - b = 0 by simp
339   finally show "a = b" .
340 next
341   assume "a = b" thus "a - b = 0" by (simp add: diff_minus)
342 qed
344 lemma diff_self [simp]: "a - a = 0"
347 lemma diff_0 [simp]: "0 - a = - a"
350 lemma diff_0_right [simp]: "a - 0 = a"
353 lemma diff_minus_eq_add [simp]: "a - - b = a + b"
356 lemma neg_equal_iff_equal [simp]:
357   "- a = - b \<longleftrightarrow> a = b"
358 proof
359   assume "- a = - b"
360   hence "- (- a) = - (- b)" by simp
361   thus "a = b" by simp
362 next
363   assume "a = b"
364   thus "- a = - b" by simp
365 qed
367 lemma neg_equal_0_iff_equal [simp]:
368   "- a = 0 \<longleftrightarrow> a = 0"
369 by (subst neg_equal_iff_equal [symmetric], simp)
371 lemma neg_0_equal_iff_equal [simp]:
372   "0 = - a \<longleftrightarrow> 0 = a"
373 by (subst neg_equal_iff_equal [symmetric], simp)
375 text{*The next two equations can make the simplifier loop!*}
377 lemma equation_minus_iff:
378   "a = - b \<longleftrightarrow> b = - a"
379 proof -
380   have "- (- a) = - b \<longleftrightarrow> - a = b" by (rule neg_equal_iff_equal)
381   thus ?thesis by (simp add: eq_commute)
382 qed
384 lemma minus_equation_iff:
385   "- a = b \<longleftrightarrow> - b = a"
386 proof -
387   have "- a = - (- b) \<longleftrightarrow> a = -b" by (rule neg_equal_iff_equal)
388   thus ?thesis by (simp add: eq_commute)
389 qed
391 lemma diff_add_cancel: "a - b + b = a"
394 lemma add_diff_cancel: "a + b - b = a"
397 declare diff_minus[symmetric, algebra_simps, field_simps]
399 lemma eq_neg_iff_add_eq_0: "a = - b \<longleftrightarrow> a + b = 0"
400 proof
401   assume "a = - b" then show "a + b = 0" by simp
402 next
403   assume "a + b = 0"
404   moreover have "a + (b + - b) = (a + b) + - b"
406   ultimately show "a = - b" by simp
407 qed
409 lemma add_eq_0_iff: "x + y = 0 \<longleftrightarrow> y = - x"
411   by (rule equation_minus_iff)
413 end
416   assumes ab_left_minus: "- a + a = 0"
417   assumes ab_diff_minus: "a - b = a + (- b)"
418 begin
421   proof qed (simp_all add: ab_left_minus ab_diff_minus)
424 proof
425   fix a b c :: 'a
426   assume "a + b = a + c"
427   then have "- a + a + b = - a + a + c"
429   then show "b = c" by simp
430 qed
433   "- a + b = b - a"
437   "- (a + b) = - a + - b"
440 lemma minus_diff_eq [simp]:
441   "- (a - b) = b - a"
444 lemma add_diff_eq[algebra_simps, field_simps]: "a + (b - c) = (a + b) - c"
447 lemma diff_add_eq[algebra_simps, field_simps]: "(a - b) + c = (a + c) - b"
450 lemma diff_eq_eq[algebra_simps, field_simps]: "a - b = c \<longleftrightarrow> a = c + b"
453 lemma eq_diff_eq[algebra_simps, field_simps]: "a = c - b \<longleftrightarrow> a + b = c"
456 lemma diff_diff_eq[algebra_simps, field_simps]: "(a - b) - c = a - (b + c)"
459 lemma diff_diff_eq2[algebra_simps, field_simps]: "a - (b - c) = (a + c) - b"
462 lemma eq_iff_diff_eq_0: "a = b \<longleftrightarrow> a - b = 0"
465 (* FIXME: duplicates right_minus_eq from class group_add *)
466 (* but only this one is declared as a simp rule. *)
467 lemma diff_eq_0_iff_eq [simp, no_atp]: "a - b = 0 \<longleftrightarrow> a = b"
468   by (rule right_minus_eq)
470 lemma diff_eq_diff_eq:
471   "a - b = c - d \<Longrightarrow> a = b \<longleftrightarrow> c = d"
472   by (auto simp add: algebra_simps)
474 end
477 subsection {* (Partially) Ordered Groups *}
479 text {*
480   The theory of partially ordered groups is taken from the books:
481   \begin{itemize}
482   \item \emph{Lattice Theory} by Garret Birkhoff, American Mathematical Society 1979
483   \item \emph{Partially Ordered Algebraic Systems}, Pergamon Press 1963
484   \end{itemize}
485   Most of the used notions can also be looked up in
486   \begin{itemize}
487   \item \url{http://www.mathworld.com} by Eric Weisstein et. al.
488   \item \emph{Algebra I} by van der Waerden, Springer.
489   \end{itemize}
490 *}
493   assumes add_left_mono: "a \<le> b \<Longrightarrow> c + a \<le> c + b"
494 begin
497   "a \<le> b \<Longrightarrow> a + c \<le> b + c"
500 text {* non-strict, in both arguments *}
502   "a \<le> b \<Longrightarrow> c \<le> d \<Longrightarrow> a + c \<le> b + d"
503   apply (erule add_right_mono [THEN order_trans])
505   done
507 end
511 begin
514   "a < b \<Longrightarrow> c + a < c + b"
518   "a < b \<Longrightarrow> a + c < b + c"
521 text{*Strict monotonicity in both arguments*}
523   "a < b \<Longrightarrow> c < d \<Longrightarrow> a + c < b + d"
524 apply (erule add_strict_right_mono [THEN less_trans])
526 done
529   "a < b \<Longrightarrow> c \<le> d \<Longrightarrow> a + c < b + d"
530 apply (erule add_strict_right_mono [THEN less_le_trans])
532 done
535   "a \<le> b \<Longrightarrow> c < d \<Longrightarrow> a + c < b + d"
536 apply (erule add_right_mono [THEN le_less_trans])
538 done
540 end
544   assumes add_le_imp_le_left: "c + a \<le> c + b \<Longrightarrow> a \<le> b"
545 begin
548   assumes less: "c + a < c + b" shows "a < b"
549 proof -
550   from less have le: "c + a <= c + b" by (simp add: order_le_less)
551   have "a <= b"
552     apply (insert le)
554     by (insert le, drule add_le_imp_le_left, assumption)
555   moreover have "a \<noteq> b"
556   proof (rule ccontr)
557     assume "~(a \<noteq> b)"
558     then have "a = b" by simp
559     then have "c + a = c + b" by simp
560     with less show "False"by simp
561   qed
562   ultimately show "a < b" by (simp add: order_le_less)
563 qed
566   "a + c < b + c \<Longrightarrow> a < b"
567 apply (rule add_less_imp_less_left [of c])
569 done
572   "c + a < c + b \<longleftrightarrow> a < b"
576   "a + c < b + c \<longleftrightarrow> a < b"
580   "c + a \<le> c + b \<longleftrightarrow> a \<le> b"
584   "a + c \<le> b + c \<longleftrightarrow> a \<le> b"
588   "a + c \<le> b + c \<Longrightarrow> a \<le> b"
589 by simp
592   "max x y + z = max (x + z) (y + z)"
593   unfolding max_def by auto
596   "min x y + z = min (x + z) (y + z)"
597   unfolding min_def by auto
599 end
601 subsection {* Support for reasoning about signs *}
605 begin
608   assumes "0 < a" and "0 \<le> b" shows "0 < a + b"
609 proof -
610   have "0 + 0 < a + b"
611     using assms by (rule add_less_le_mono)
612   then show ?thesis by simp
613 qed
616   assumes "0 < a" and "0 < b" shows "0 < a + b"
617 by (rule add_pos_nonneg) (insert assms, auto)
620   assumes "0 \<le> a" and "0 < b" shows "0 < a + b"
621 proof -
622   have "0 + 0 < a + b"
623     using assms by (rule add_le_less_mono)
624   then show ?thesis by simp
625 qed
628   assumes "0 \<le> a" and "0 \<le> b" shows "0 \<le> a + b"
629 proof -
630   have "0 + 0 \<le> a + b"
631     using assms by (rule add_mono)
632   then show ?thesis by simp
633 qed
636   assumes "a < 0" and "b \<le> 0" shows "a + b < 0"
637 proof -
638   have "a + b < 0 + 0"
639     using assms by (rule add_less_le_mono)
640   then show ?thesis by simp
641 qed
644   assumes "a < 0" and "b < 0" shows "a + b < 0"
645 by (rule add_neg_nonpos) (insert assms, auto)
648   assumes "a \<le> 0" and "b < 0" shows "a + b < 0"
649 proof -
650   have "a + b < 0 + 0"
651     using assms by (rule add_le_less_mono)
652   then show ?thesis by simp
653 qed
656   assumes "a \<le> 0" and "b \<le> 0" shows "a + b \<le> 0"
657 proof -
658   have "a + b \<le> 0 + 0"
659     using assms by (rule add_mono)
660   then show ?thesis by simp
661 qed
668   assumes x: "0 \<le> x" and y: "0 \<le> y"
669   shows "x + y = 0 \<longleftrightarrow> x = 0 \<and> y = 0"
670 proof (intro iffI conjI)
671   have "x = x + 0" by simp
672   also have "x + 0 \<le> x + y" using y by (rule add_left_mono)
673   also assume "x + y = 0"
674   also have "0 \<le> x" using x .
675   finally show "x = 0" .
676 next
677   have "y = 0 + y" by simp
678   also have "0 + y \<le> x + y" using x by (rule add_right_mono)
679   also assume "x + y = 0"
680   also have "0 \<le> y" using y .
681   finally show "y = 0" .
682 next
683   assume "x = 0 \<and> y = 0"
684   then show "x + y = 0" by simp
685 qed
687 end
691 begin
696 proof
697   fix a b c :: 'a
698   assume "c + a \<le> c + b"
699   hence "(-c) + (c + a) \<le> (-c) + (c + b)" by (rule add_left_mono)
700   hence "((-c) + c) + a \<le> ((-c) + c) + b" by (simp only: add_assoc)
701   thus "a \<le> b" by simp
702 qed
706 lemma max_diff_distrib_left:
707   shows "max x y - z = max (x - z) (y - z)"
710 lemma min_diff_distrib_left:
711   shows "min x y - z = min (x - z) (y - z)"
714 lemma le_imp_neg_le:
715   assumes "a \<le> b" shows "-b \<le> -a"
716 proof -
717   have "-a+a \<le> -a+b" using a \<le> b by (rule add_left_mono)
718   hence "0 \<le> -a+b" by simp
719   hence "0 + (-b) \<le> (-a + b) + (-b)" by (rule add_right_mono)
721 qed
723 lemma neg_le_iff_le [simp]: "- b \<le> - a \<longleftrightarrow> a \<le> b"
724 proof
725   assume "- b \<le> - a"
726   hence "- (- a) \<le> - (- b)" by (rule le_imp_neg_le)
727   thus "a\<le>b" by simp
728 next
729   assume "a\<le>b"
730   thus "-b \<le> -a" by (rule le_imp_neg_le)
731 qed
733 lemma neg_le_0_iff_le [simp]: "- a \<le> 0 \<longleftrightarrow> 0 \<le> a"
734 by (subst neg_le_iff_le [symmetric], simp)
736 lemma neg_0_le_iff_le [simp]: "0 \<le> - a \<longleftrightarrow> a \<le> 0"
737 by (subst neg_le_iff_le [symmetric], simp)
739 lemma neg_less_iff_less [simp]: "- b < - a \<longleftrightarrow> a < b"
740 by (force simp add: less_le)
742 lemma neg_less_0_iff_less [simp]: "- a < 0 \<longleftrightarrow> 0 < a"
743 by (subst neg_less_iff_less [symmetric], simp)
745 lemma neg_0_less_iff_less [simp]: "0 < - a \<longleftrightarrow> a < 0"
746 by (subst neg_less_iff_less [symmetric], simp)
748 text{*The next several equations can make the simplifier loop!*}
750 lemma less_minus_iff: "a < - b \<longleftrightarrow> b < - a"
751 proof -
752   have "(- (-a) < - b) = (b < - a)" by (rule neg_less_iff_less)
753   thus ?thesis by simp
754 qed
756 lemma minus_less_iff: "- a < b \<longleftrightarrow> - b < a"
757 proof -
758   have "(- a < - (-b)) = (- b < a)" by (rule neg_less_iff_less)
759   thus ?thesis by simp
760 qed
762 lemma le_minus_iff: "a \<le> - b \<longleftrightarrow> b \<le> - a"
763 proof -
764   have mm: "!! a (b::'a). (-(-a)) < -b \<Longrightarrow> -(-b) < -a" by (simp only: minus_less_iff)
765   have "(- (- a) <= -b) = (b <= - a)"
766     apply (auto simp only: le_less)
767     apply (drule mm)
768     apply (simp_all)
769     apply (drule mm[simplified], assumption)
770     done
771   then show ?thesis by simp
772 qed
774 lemma minus_le_iff: "- a \<le> b \<longleftrightarrow> - b \<le> a"
775 by (auto simp add: le_less minus_less_iff)
777 lemma diff_less_0_iff_less [simp, no_atp]:
778   "a - b < 0 \<longleftrightarrow> a < b"
779 proof -
780   have "a - b < 0 \<longleftrightarrow> a + (- b) < b + (- b)" by (simp add: diff_minus)
781   also have "... \<longleftrightarrow> a < b" by (simp only: add_less_cancel_right)
782   finally show ?thesis .
783 qed
785 lemmas less_iff_diff_less_0 = diff_less_0_iff_less [symmetric]
787 lemma diff_less_eq[algebra_simps, field_simps]: "a - b < c \<longleftrightarrow> a < c + b"
788 apply (subst less_iff_diff_less_0 [of a])
789 apply (rule less_iff_diff_less_0 [of _ c, THEN ssubst])
791 done
793 lemma less_diff_eq[algebra_simps, field_simps]: "a < c - b \<longleftrightarrow> a + b < c"
794 apply (subst less_iff_diff_less_0 [of "a + b"])
795 apply (subst less_iff_diff_less_0 [of a])
797 done
799 lemma diff_le_eq[algebra_simps, field_simps]: "a - b \<le> c \<longleftrightarrow> a \<le> c + b"
802 lemma le_diff_eq[algebra_simps, field_simps]: "a \<le> c - b \<longleftrightarrow> a + b \<le> c"
805 lemma diff_le_0_iff_le [simp, no_atp]:
806   "a - b \<le> 0 \<longleftrightarrow> a \<le> b"
809 lemmas le_iff_diff_le_0 = diff_le_0_iff_le [symmetric]
811 lemma diff_eq_diff_less:
812   "a - b = c - d \<Longrightarrow> a < b \<longleftrightarrow> c < d"
813   by (auto simp only: less_iff_diff_less_0 [of a b] less_iff_diff_less_0 [of c d])
815 lemma diff_eq_diff_less_eq:
816   "a - b = c - d \<Longrightarrow> a \<le> b \<longleftrightarrow> c \<le> d"
817   by (auto simp only: le_iff_diff_le_0 [of a b] le_iff_diff_le_0 [of c d])
819 end
821 use "Tools/abel_cancel.ML"
823 simproc_setup abel_cancel_sum
825   {* fn phi => Abel_Cancel.sum_proc *}
827 simproc_setup abel_cancel_relation
829   {* fn phi => Abel_Cancel.rel_proc *}
836 begin
841 proof
842   fix a b c :: 'a
843   assume le: "c + a <= c + b"
844   show "a <= b"
845   proof (rule ccontr)
846     assume w: "~ a \<le> b"
847     hence "b <= a" by (simp add: linorder_not_le)
848     hence le2: "c + b <= c + a" by (rule add_left_mono)
849     have "a = b"
850       apply (insert le)
851       apply (insert le2)
852       apply (drule antisym, simp_all)
853       done
854     with w show False
855       by (simp add: linorder_not_le [symmetric])
856   qed
857 qed
859 end
862 begin
866 lemma neg_less_eq_nonneg [simp]:
867   "- a \<le> a \<longleftrightarrow> 0 \<le> a"
868 proof
869   assume A: "- a \<le> a" show "0 \<le> a"
870   proof (rule classical)
871     assume "\<not> 0 \<le> a"
872     then have "a < 0" by auto
873     with A have "- a < 0" by (rule le_less_trans)
874     then show ?thesis by auto
875   qed
876 next
877   assume A: "0 \<le> a" show "- a \<le> a"
878   proof (rule order_trans)
879     show "- a \<le> 0" using A by (simp add: minus_le_iff)
880   next
881     show "0 \<le> a" using A .
882   qed
883 qed
885 lemma neg_less_nonneg [simp]:
886   "- a < a \<longleftrightarrow> 0 < a"
887 proof
888   assume A: "- a < a" show "0 < a"
889   proof (rule classical)
890     assume "\<not> 0 < a"
891     then have "a \<le> 0" by auto
892     with A have "- a < 0" by (rule less_le_trans)
893     then show ?thesis by auto
894   qed
895 next
896   assume A: "0 < a" show "- a < a"
897   proof (rule less_trans)
898     show "- a < 0" using A by (simp add: minus_le_iff)
899   next
900     show "0 < a" using A .
901   qed
902 qed
904 lemma less_eq_neg_nonpos [simp]:
905   "a \<le> - a \<longleftrightarrow> a \<le> 0"
906 proof
907   assume A: "a \<le> - a" show "a \<le> 0"
908   proof (rule classical)
909     assume "\<not> a \<le> 0"
910     then have "0 < a" by auto
911     then have "0 < - a" using A by (rule less_le_trans)
912     then show ?thesis by auto
913   qed
914 next
915   assume A: "a \<le> 0" show "a \<le> - a"
916   proof (rule order_trans)
917     show "0 \<le> - a" using A by (simp add: minus_le_iff)
918   next
919     show "a \<le> 0" using A .
920   qed
921 qed
923 lemma equal_neg_zero [simp]:
924   "a = - a \<longleftrightarrow> a = 0"
925 proof
926   assume "a = 0" then show "a = - a" by simp
927 next
928   assume A: "a = - a" show "a = 0"
929   proof (cases "0 \<le> a")
930     case True with A have "0 \<le> - a" by auto
931     with le_minus_iff have "a \<le> 0" by simp
932     with True show ?thesis by (auto intro: order_trans)
933   next
934     case False then have B: "a \<le> 0" by auto
935     with A have "- a \<le> 0" by auto
936     with B show ?thesis by (auto intro: order_trans)
937   qed
938 qed
940 lemma neg_equal_zero [simp]:
941   "- a = a \<longleftrightarrow> a = 0"
942   by (auto dest: sym)
944 lemma double_zero [simp]:
945   "a + a = 0 \<longleftrightarrow> a = 0"
946 proof
947   assume assm: "a + a = 0"
948   then have a: "- a = a" by (rule minus_unique)
949   then show "a = 0" by (simp only: neg_equal_zero)
950 qed simp
952 lemma double_zero_sym [simp]:
953   "0 = a + a \<longleftrightarrow> a = 0"
954   by (rule, drule sym) simp_all
957   "0 < a + a \<longleftrightarrow> 0 < a"
958 proof
959   assume "0 < a + a"
960   then have "0 - a < a" by (simp only: diff_less_eq)
961   then have "- a < a" by simp
962   then show "0 < a" by (simp only: neg_less_nonneg)
963 next
964   assume "0 < a"
965   with this have "0 + 0 < a + a"
967   then show "0 < a + a" by simp
968 qed
971   "0 \<le> a + a \<longleftrightarrow> 0 \<le> a"
972   by (auto simp add: le_less)
975   "a + a < 0 \<longleftrightarrow> a < 0"
976 proof -
977   have "\<not> a + a < 0 \<longleftrightarrow> \<not> a < 0"
979   then show ?thesis by simp
980 qed
983   "a + a \<le> 0 \<longleftrightarrow> a \<le> 0"
984 proof -
985   have "\<not> a + a \<le> 0 \<longleftrightarrow> \<not> a \<le> 0"
987   then show ?thesis by simp
988 qed
990 lemma le_minus_self_iff:
991   "a \<le> - a \<longleftrightarrow> a \<le> 0"
992 proof -
993   from add_le_cancel_left [of "- a" "a + a" 0]
994   have "a \<le> - a \<longleftrightarrow> a + a \<le> 0"
996   thus ?thesis by simp
997 qed
999 lemma minus_le_self_iff:
1000   "- a \<le> a \<longleftrightarrow> 0 \<le> a"
1001 proof -
1002   from add_le_cancel_left [of "- a" 0 "a + a"]
1003   have "- a \<le> a \<longleftrightarrow> 0 \<le> a + a"
1005   thus ?thesis by simp
1006 qed
1008 lemma minus_max_eq_min:
1009   "- max x y = min (-x) (-y)"
1010   by (auto simp add: max_def min_def)
1012 lemma minus_min_eq_max:
1013   "- min x y = max (-x) (-y)"
1014   by (auto simp add: max_def min_def)
1016 end
1019 begin
1022   "0 \<le> a \<Longrightarrow> b \<le> c \<Longrightarrow> b \<le> a + c"
1023   by (insert add_mono [of 0 a b c], simp)
1026   "0 \<le> c \<Longrightarrow> b \<le> a \<Longrightarrow> b \<le> a + c"
1030   "0 < a \<Longrightarrow> b \<le> c \<Longrightarrow> b < a + c"
1031   by (insert add_less_le_mono [of 0 a b c], simp)
1034   "0 \<le> a \<Longrightarrow> b < c \<Longrightarrow> b < a + c"
1035   by (insert add_le_less_mono [of 0 a b c], simp)
1037 end
1039 class abs =
1040   fixes abs :: "'a \<Rightarrow> 'a"
1041 begin
1043 notation (xsymbols)
1044   abs  ("\<bar>_\<bar>")
1046 notation (HTML output)
1047   abs  ("\<bar>_\<bar>")
1049 end
1051 class sgn =
1052   fixes sgn :: "'a \<Rightarrow> 'a"
1054 class abs_if = minus + uminus + ord + zero + abs +
1055   assumes abs_if: "\<bar>a\<bar> = (if a < 0 then - a else a)"
1057 class sgn_if = minus + uminus + zero + one + ord + sgn +
1058   assumes sgn_if: "sgn x = (if x = 0 then 0 else if 0 < x then 1 else - 1)"
1059 begin
1061 lemma sgn0 [simp]: "sgn 0 = 0"
1064 end
1067   assumes abs_ge_zero [simp]: "\<bar>a\<bar> \<ge> 0"
1068     and abs_ge_self: "a \<le> \<bar>a\<bar>"
1069     and abs_leI: "a \<le> b \<Longrightarrow> - a \<le> b \<Longrightarrow> \<bar>a\<bar> \<le> b"
1070     and abs_minus_cancel [simp]: "\<bar>-a\<bar> = \<bar>a\<bar>"
1071     and abs_triangle_ineq: "\<bar>a + b\<bar> \<le> \<bar>a\<bar> + \<bar>b\<bar>"
1072 begin
1074 lemma abs_minus_le_zero: "- \<bar>a\<bar> \<le> 0"
1075   unfolding neg_le_0_iff_le by simp
1077 lemma abs_of_nonneg [simp]:
1078   assumes nonneg: "0 \<le> a" shows "\<bar>a\<bar> = a"
1079 proof (rule antisym)
1080   from nonneg le_imp_neg_le have "- a \<le> 0" by simp
1081   from this nonneg have "- a \<le> a" by (rule order_trans)
1082   then show "\<bar>a\<bar> \<le> a" by (auto intro: abs_leI)
1083 qed (rule abs_ge_self)
1085 lemma abs_idempotent [simp]: "\<bar>\<bar>a\<bar>\<bar> = \<bar>a\<bar>"
1086 by (rule antisym)
1087    (auto intro!: abs_ge_self abs_leI order_trans [of "- \<bar>a\<bar>" 0 "\<bar>a\<bar>"])
1089 lemma abs_eq_0 [simp]: "\<bar>a\<bar> = 0 \<longleftrightarrow> a = 0"
1090 proof -
1091   have "\<bar>a\<bar> = 0 \<Longrightarrow> a = 0"
1092   proof (rule antisym)
1093     assume zero: "\<bar>a\<bar> = 0"
1094     with abs_ge_self show "a \<le> 0" by auto
1095     from zero have "\<bar>-a\<bar> = 0" by simp
1096     with abs_ge_self [of "- a"] have "- a \<le> 0" by auto
1097     with neg_le_0_iff_le show "0 \<le> a" by auto
1098   qed
1099   then show ?thesis by auto
1100 qed
1102 lemma abs_zero [simp]: "\<bar>0\<bar> = 0"
1103 by simp
1105 lemma abs_0_eq [simp, no_atp]: "0 = \<bar>a\<bar> \<longleftrightarrow> a = 0"
1106 proof -
1107   have "0 = \<bar>a\<bar> \<longleftrightarrow> \<bar>a\<bar> = 0" by (simp only: eq_ac)
1108   thus ?thesis by simp
1109 qed
1111 lemma abs_le_zero_iff [simp]: "\<bar>a\<bar> \<le> 0 \<longleftrightarrow> a = 0"
1112 proof
1113   assume "\<bar>a\<bar> \<le> 0"
1114   then have "\<bar>a\<bar> = 0" by (rule antisym) simp
1115   thus "a = 0" by simp
1116 next
1117   assume "a = 0"
1118   thus "\<bar>a\<bar> \<le> 0" by simp
1119 qed
1121 lemma zero_less_abs_iff [simp]: "0 < \<bar>a\<bar> \<longleftrightarrow> a \<noteq> 0"
1124 lemma abs_not_less_zero [simp]: "\<not> \<bar>a\<bar> < 0"
1125 proof -
1126   have a: "\<And>x y. x \<le> y \<Longrightarrow> \<not> y < x" by auto
1127   show ?thesis by (simp add: a)
1128 qed
1130 lemma abs_ge_minus_self: "- a \<le> \<bar>a\<bar>"
1131 proof -
1132   have "- a \<le> \<bar>-a\<bar>" by (rule abs_ge_self)
1133   then show ?thesis by simp
1134 qed
1136 lemma abs_minus_commute:
1137   "\<bar>a - b\<bar> = \<bar>b - a\<bar>"
1138 proof -
1139   have "\<bar>a - b\<bar> = \<bar>- (a - b)\<bar>" by (simp only: abs_minus_cancel)
1140   also have "... = \<bar>b - a\<bar>" by simp
1141   finally show ?thesis .
1142 qed
1144 lemma abs_of_pos: "0 < a \<Longrightarrow> \<bar>a\<bar> = a"
1145 by (rule abs_of_nonneg, rule less_imp_le)
1147 lemma abs_of_nonpos [simp]:
1148   assumes "a \<le> 0" shows "\<bar>a\<bar> = - a"
1149 proof -
1150   let ?b = "- a"
1151   have "- ?b \<le> 0 \<Longrightarrow> \<bar>- ?b\<bar> = - (- ?b)"
1152   unfolding abs_minus_cancel [of "?b"]
1153   unfolding neg_le_0_iff_le [of "?b"]
1154   unfolding minus_minus by (erule abs_of_nonneg)
1155   then show ?thesis using assms by auto
1156 qed
1158 lemma abs_of_neg: "a < 0 \<Longrightarrow> \<bar>a\<bar> = - a"
1159 by (rule abs_of_nonpos, rule less_imp_le)
1161 lemma abs_le_D1: "\<bar>a\<bar> \<le> b \<Longrightarrow> a \<le> b"
1162 by (insert abs_ge_self, blast intro: order_trans)
1164 lemma abs_le_D2: "\<bar>a\<bar> \<le> b \<Longrightarrow> - a \<le> b"
1165 by (insert abs_le_D1 [of "- a"], simp)
1167 lemma abs_le_iff: "\<bar>a\<bar> \<le> b \<longleftrightarrow> a \<le> b \<and> - a \<le> b"
1168 by (blast intro: abs_leI dest: abs_le_D1 abs_le_D2)
1170 lemma abs_triangle_ineq2: "\<bar>a\<bar> - \<bar>b\<bar> \<le> \<bar>a - b\<bar>"
1171 proof -
1172   have "\<bar>a\<bar> = \<bar>b + (a - b)\<bar>"
1174   then have "\<bar>a\<bar> \<le> \<bar>b\<bar> + \<bar>a - b\<bar>"
1176   then show ?thesis
1178 qed
1180 lemma abs_triangle_ineq2_sym: "\<bar>a\<bar> - \<bar>b\<bar> \<le> \<bar>b - a\<bar>"
1181   by (simp only: abs_minus_commute [of b] abs_triangle_ineq2)
1183 lemma abs_triangle_ineq3: "\<bar>\<bar>a\<bar> - \<bar>b\<bar>\<bar> \<le> \<bar>a - b\<bar>"
1184   by (simp add: abs_le_iff abs_triangle_ineq2 abs_triangle_ineq2_sym)
1186 lemma abs_triangle_ineq4: "\<bar>a - b\<bar> \<le> \<bar>a\<bar> + \<bar>b\<bar>"
1187 proof -
1188   have "\<bar>a - b\<bar> = \<bar>a + - b\<bar>" by (subst diff_minus, rule refl)
1189   also have "... \<le> \<bar>a\<bar> + \<bar>- b\<bar>" by (rule abs_triangle_ineq)
1190   finally show ?thesis by simp
1191 qed
1193 lemma abs_diff_triangle_ineq: "\<bar>a + b - (c + d)\<bar> \<le> \<bar>a - c\<bar> + \<bar>b - d\<bar>"
1194 proof -
1195   have "\<bar>a + b - (c+d)\<bar> = \<bar>(a-c) + (b-d)\<bar>" by (simp add: diff_minus add_ac)
1196   also have "... \<le> \<bar>a-c\<bar> + \<bar>b-d\<bar>" by (rule abs_triangle_ineq)
1197   finally show ?thesis .
1198 qed
1201   "\<bar>\<bar>a\<bar> + \<bar>b\<bar>\<bar> = \<bar>a\<bar> + \<bar>b\<bar>" (is "?L = ?R")
1202 proof (rule antisym)
1203   show "?L \<ge> ?R" by(rule abs_ge_self)
1204 next
1205   have "?L \<le> \<bar>\<bar>a\<bar>\<bar> + \<bar>\<bar>b\<bar>\<bar>" by(rule abs_triangle_ineq)
1206   also have "\<dots> = ?R" by simp
1207   finally show "?L \<le> ?R" .
1208 qed
1210 end
1213 subsection {* Tools setup *}
1216   fixes i j k :: "'a\<Colon>ordered_ab_semigroup_add"
1217   shows "i \<le> j \<and> k \<le> l \<Longrightarrow> i + k \<le> j + l"
1218     and "i = j \<and> k \<le> l \<Longrightarrow> i + k \<le> j + l"
1219     and "i \<le> j \<and> k = l \<Longrightarrow> i + k \<le> j + l"
1220     and "i = j \<and> k = l \<Longrightarrow> i + k = j + l"
1224   fixes i j k :: "'a\<Colon>ordered_cancel_ab_semigroup_add"
1225   shows "i < j \<and> k = l \<Longrightarrow> i + k < j + l"
1226     and "i = j \<and> k < l \<Longrightarrow> i + k < j + l"
1227     and "i < j \<and> k \<le> l \<Longrightarrow> i + k < j + l"
1228     and "i \<le> j \<and> k < l \<Longrightarrow> i + k < j + l"
1229     and "i < j \<and> k < l \<Longrightarrow> i + k < j + l"