src/HOL/Groups.thy
 author haftmann Fri Jul 04 20:18:47 2014 +0200 (2014-07-04) changeset 57512 cc97b347b301 parent 56950 c49edf06f8e4 child 57514 bdc2c6b40bf2 permissions -rw-r--r--
reduced name variants for assoc and commute on plus and mult
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 begin
11 subsection {* Fact collections *}
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 *}
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 (
35   val name = @{binding algebra_simps}
36   val description = "algebra simplification rules"
37 )
38 *}
40 setup Algebra_Simps.setup
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}. *}
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 *}
55 setup Field_Simps.setup
58 subsection {* Abstract structures *}
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 *}
66 locale semigroup =
67   fixes f :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "*" 70)
68   assumes assoc [ac_simps]: "a * b * c = a * (b * c)"
70 locale abel_semigroup = semigroup +
71   assumes commute [ac_simps]: "a * b = b * a"
72 begin
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
83 end
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"
90 locale comm_monoid = abel_semigroup +
91   fixes z :: 'a ("1")
92   assumes comm_neutral: "a * 1 = a"
93 begin
95 sublocale monoid
96   by default (simp_all add: commute comm_neutral)
98 end
101 subsection {* Generic operations *}
103 class zero =
104   fixes zero :: 'a  ("0")
106 class one =
107   fixes one  :: 'a  ("1")
109 hide_const (open) zero one
111 lemma Let_0 [simp]: "Let 0 f = f 0"
112   unfolding Let_def ..
114 lemma Let_1 [simp]: "Let 1 f = f 1"
115   unfolding Let_def ..
117 setup {*
119     (fn Const(@{const_name Groups.zero}, _) => true
120       | Const(@{const_name Groups.one}, _) => true
121       | _ => false)
122 *}
124 simproc_setup reorient_zero ("0 = x") = Reorient_Proc.proc
125 simproc_setup reorient_one ("1 = x") = Reorient_Proc.proc
127 typed_print_translation {*
128   let
129     fun tr' c = (c, fn ctxt => fn T => fn ts =>
130       if null ts andalso Printer.type_emphasis ctxt T then
131         Syntax.const @{syntax_const "_constrain"} $Syntax.const c$
132           Syntax_Phases.term_of_typ ctxt T
133       else raise Match);
134   in map tr' [@{const_syntax Groups.one}, @{const_syntax Groups.zero}] end;
135 *} -- {* show types that are presumably too general *}
137 class plus =
138   fixes plus :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "+" 65)
140 class minus =
141   fixes minus :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "-" 65)
143 class uminus =
144   fixes uminus :: "'a \<Rightarrow> 'a"  ("- _" [81] 80)
146 class times =
147   fixes times :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "*" 70)
150 subsection {* Semigroups and Monoids *}
152 class semigroup_add = plus +
153   assumes add_assoc [algebra_simps, field_simps]: "(a + b) + c = a + (b + c)"
154 begin
159 end
164   assumes add_commute [algebra_simps, field_simps]: "a + b = b + a"
165 begin
174 end
180 class semigroup_mult = times +
181   assumes mult_assoc [algebra_simps, field_simps]: "(a * b) * c = a * (b * c)"
182 begin
184 sublocale mult!: semigroup times
185   by default (fact mult_assoc)
187 end
189 hide_fact mult_assoc
191 class ab_semigroup_mult = semigroup_mult +
192   assumes mult_commute [algebra_simps, field_simps]: "a * b = b * a"
193 begin
195 sublocale mult!: abel_semigroup times
196   by default (fact mult_commute)
198 declare mult.left_commute [algebra_simps, field_simps]
200 theorems mult_ac = mult.assoc mult.commute mult.left_commute
202 end
204 hide_fact mult_commute
206 theorems mult_ac = mult.assoc mult.commute mult.left_commute
209   assumes add_0_left: "0 + a = a"
210     and add_0_right: "a + 0 = a"
211 begin
213 sublocale add!: monoid plus 0
216 end
218 lemma zero_reorient: "0 = x \<longleftrightarrow> x = 0"
219   by (fact eq_commute)
222   assumes add_0: "0 + a = a"
223 begin
225 sublocale add!: comm_monoid plus 0
231 end
233 class comm_monoid_diff = comm_monoid_add + minus +
234   assumes diff_zero [simp]: "a - 0 = a"
235     and zero_diff [simp]: "0 - a = 0"
236     and add_diff_cancel_left [simp]: "(c + a) - (c + b) = a - b"
237     and diff_diff_add: "a - b - c = a - (b + c)"
238 begin
241   "(a + c) - (b + c) = a - b"
245   "(b + a) - b = a"
246 proof -
247   have "(b + a) - (b + 0) = a" by (simp only: add_diff_cancel_left diff_zero)
248   then show ?thesis by simp
249 qed
252   "(a + b) - b = a"
256   "a - (a + b) = 0"
257 proof -
258   have "a - (a + b) = (a + 0) - (a + b)" by simp
259   also have "\<dots> = 0" by (simp only: add_diff_cancel_left zero_diff)
260   finally show ?thesis .
261 qed
263 lemma diff_cancel [simp]:
264   "a - a = 0"
265 proof -
266   have "(a + 0) - (a + 0) = 0" by (simp only: add_diff_cancel_left diff_zero)
267   then show ?thesis by simp
268 qed
270 lemma diff_right_commute:
271   "a - c - b = a - b - c"
275   assumes "c + b = a"
276   shows "c = a - b"
277 proof -
278   from assms have "(b + c) - (b + 0) = a - b" by (simp add: add.commute)
279   then show "c = a - b" by simp
280 qed
282 end
284 class monoid_mult = one + semigroup_mult +
285   assumes mult_1_left: "1 * a  = a"
286     and mult_1_right: "a * 1 = a"
287 begin
289 sublocale mult!: monoid times 1
290   by default (fact mult_1_left mult_1_right)+
292 end
294 lemma one_reorient: "1 = x \<longleftrightarrow> x = 1"
295   by (fact eq_commute)
297 class comm_monoid_mult = one + ab_semigroup_mult +
298   assumes mult_1: "1 * a = a"
299 begin
301 sublocale mult!: comm_monoid times 1
302   by default (insert mult_1, simp add: ac_simps)
304 subclass monoid_mult
305   by default (fact mult.left_neutral mult.right_neutral)+
307 end
310   assumes add_left_imp_eq: "a + b = a + c \<Longrightarrow> b = c"
311   assumes add_right_imp_eq: "b + a = c + a \<Longrightarrow> b = c"
312 begin
315   "a + b = a + c \<longleftrightarrow> b = c"
319   "b + a = c + a \<longleftrightarrow> b = c"
322 end
325   assumes add_imp_eq: "a + b = a + c \<Longrightarrow> b = c"
326 begin
329 proof
330   fix a b c :: 'a
331   assume "a + b = a + c"
332   then show "b = c" by (rule add_imp_eq)
333 next
334   fix a b c :: 'a
335   assume "b + a = c + a"
336   then have "a + b = a + c" by (simp only: add.commute)
337   then show "b = c" by (rule add_imp_eq)
338 qed
340 end
345 subsection {* Groups *}
348   assumes left_minus [simp]: "- a + a = 0"
349   assumes add_uminus_conv_diff [simp]: "a + (- b) = a - b"
350 begin
353   "a - b = a + (- b)"
354   by simp
356 lemma minus_unique:
357   assumes "a + b = 0" shows "- a = b"
358 proof -
359   have "- a = - a + (a + b)" using assms by simp
361   finally show ?thesis .
362 qed
364 lemma minus_zero [simp]: "- 0 = 0"
365 proof -
366   have "0 + 0 = 0" by (rule add_0_right)
367   thus "- 0 = 0" by (rule minus_unique)
368 qed
370 lemma minus_minus [simp]: "- (- a) = a"
371 proof -
372   have "- a + a = 0" by (rule left_minus)
373   thus "- (- a) = a" by (rule minus_unique)
374 qed
376 lemma right_minus: "a + - a = 0"
377 proof -
378   have "a + - a = - (- a) + - a" by simp
379   also have "\<dots> = 0" by (rule left_minus)
380   finally show ?thesis .
381 qed
383 lemma diff_self [simp]:
384   "a - a = 0"
385   using right_minus [of a] by simp
388 proof
389   fix a b c :: 'a
390   assume "a + b = a + c"
391   then have "- a + a + b = - a + a + c"
393   then show "b = c" by simp
394 next
395   fix a b c :: 'a
396   assume "b + a = c + a"
397   then have "b + a + - a = c + a  + - a" by simp
398   then show "b = c" unfolding add.assoc by simp
399 qed
402   "- a + (a + b) = b"
406   "a + (- a + b) = b"
410   "a - b + b = a"
414   "a + b - b = a"
418   "- (a + b) = - b + - a"
419 proof -
420   have "(a + b) + (- b + - a) = 0"
422   then show "- (a + b) = - b + - a"
423     by (rule minus_unique)
424 qed
426 lemma right_minus_eq [simp]:
427   "a - b = 0 \<longleftrightarrow> a = b"
428 proof
429   assume "a - b = 0"
430   have "a = (a - b) + b" by (simp add: add.assoc)
431   also have "\<dots> = b" using a - b = 0 by simp
432   finally show "a = b" .
433 next
434   assume "a = b" thus "a - b = 0" by simp
435 qed
437 lemma eq_iff_diff_eq_0:
438   "a = b \<longleftrightarrow> a - b = 0"
439   by (fact right_minus_eq [symmetric])
441 lemma diff_0 [simp]:
442   "0 - a = - a"
445 lemma diff_0_right [simp]:
446   "a - 0 = a"
450   "a - - b = a + b"
451   by (simp only: diff_conv_add_uminus minus_minus)
453 lemma neg_equal_iff_equal [simp]:
454   "- a = - b \<longleftrightarrow> a = b"
455 proof
456   assume "- a = - b"
457   hence "- (- a) = - (- b)" by simp
458   thus "a = b" by simp
459 next
460   assume "a = b"
461   thus "- a = - b" by simp
462 qed
464 lemma neg_equal_0_iff_equal [simp]:
465   "- a = 0 \<longleftrightarrow> a = 0"
466   by (subst neg_equal_iff_equal [symmetric]) simp
468 lemma neg_0_equal_iff_equal [simp]:
469   "0 = - a \<longleftrightarrow> 0 = a"
470   by (subst neg_equal_iff_equal [symmetric]) simp
472 text{*The next two equations can make the simplifier loop!*}
474 lemma equation_minus_iff:
475   "a = - b \<longleftrightarrow> b = - a"
476 proof -
477   have "- (- a) = - b \<longleftrightarrow> - a = b" by (rule neg_equal_iff_equal)
478   thus ?thesis by (simp add: eq_commute)
479 qed
481 lemma minus_equation_iff:
482   "- a = b \<longleftrightarrow> - b = a"
483 proof -
484   have "- a = - (- b) \<longleftrightarrow> a = -b" by (rule neg_equal_iff_equal)
485   thus ?thesis by (simp add: eq_commute)
486 qed
489   "a = - b \<longleftrightarrow> a + b = 0"
490 proof
491   assume "a = - b" then show "a + b = 0" by simp
492 next
493   assume "a + b = 0"
494   moreover have "a + (b + - b) = (a + b) + - b"
496   ultimately show "a = - b" by simp
497 qed
500   "a + b = 0 \<longleftrightarrow> a = - b"
504   "- a = b \<longleftrightarrow> a + b = 0"
508   "a + b = 0 \<longleftrightarrow> b = - a"
511 lemma minus_diff_eq [simp]:
512   "- (a - b) = b - a"
516   "a + (b - c) = (a + b) - c"
520   "a - (b + c) = a - c - b"
523 lemma diff_eq_eq [algebra_simps, field_simps]:
524   "a - b = c \<longleftrightarrow> a = c + b"
525   by auto
527 lemma eq_diff_eq [algebra_simps, field_simps]:
528   "a = c - b \<longleftrightarrow> a + b = c"
529   by auto
531 lemma diff_diff_eq2 [algebra_simps, field_simps]:
532   "a - (b - c) = (a + c) - b"
535 lemma diff_eq_diff_eq:
536   "a - b = c - d \<Longrightarrow> a = b \<longleftrightarrow> c = d"
537   by (simp only: eq_iff_diff_eq_0 [of a b] eq_iff_diff_eq_0 [of c d])
539 end
542   assumes ab_left_minus: "- a + a = 0"
543   assumes ab_add_uminus_conv_diff: "a - b = a + (- b)"
544 begin
550 proof
551   fix a b c :: 'a
552   assume "a + b = a + c"
553   then have "- a + a + b = - a + a + c"
555   then show "b = c" by simp
556 qed
559   "- a + b = b - a"
563   "- (a + b) = - a + - b"
567   "(a - b) + c = (a + c) - b"
570 lemma diff_diff_eq [algebra_simps, field_simps]:
571   "(a - b) - c = a - (b + c)"
575   "a - (b + c) = a - b - c"
579   "(c + a) - (c + b) = a - b"
582 end
585 subsection {* (Partially) Ordered Groups *}
587 text {*
588   The theory of partially ordered groups is taken from the books:
589   \begin{itemize}
590   \item \emph{Lattice Theory} by Garret Birkhoff, American Mathematical Society 1979
591   \item \emph{Partially Ordered Algebraic Systems}, Pergamon Press 1963
592   \end{itemize}
593   Most of the used notions can also be looked up in
594   \begin{itemize}
595   \item @{url "http://www.mathworld.com"} by Eric Weisstein et. al.
596   \item \emph{Algebra I} by van der Waerden, Springer.
597   \end{itemize}
598 *}
601   assumes add_left_mono: "a \<le> b \<Longrightarrow> c + a \<le> c + b"
602 begin
605   "a \<le> b \<Longrightarrow> a + c \<le> b + c"
608 text {* non-strict, in both arguments *}
610   "a \<le> b \<Longrightarrow> c \<le> d \<Longrightarrow> a + c \<le> b + d"
611   apply (erule add_right_mono [THEN order_trans])
613   done
615 end
619 begin
622   "a < b \<Longrightarrow> c + a < c + b"
626   "a < b \<Longrightarrow> a + c < b + c"
629 text{*Strict monotonicity in both arguments*}
631   "a < b \<Longrightarrow> c < d \<Longrightarrow> a + c < b + d"
632 apply (erule add_strict_right_mono [THEN less_trans])
634 done
637   "a < b \<Longrightarrow> c \<le> d \<Longrightarrow> a + c < b + d"
638 apply (erule add_strict_right_mono [THEN less_le_trans])
640 done
643   "a \<le> b \<Longrightarrow> c < d \<Longrightarrow> a + c < b + d"
644 apply (erule add_right_mono [THEN le_less_trans])
646 done
648 end
652   assumes add_le_imp_le_left: "c + a \<le> c + b \<Longrightarrow> a \<le> b"
653 begin
656   assumes less: "c + a < c + b" shows "a < b"
657 proof -
658   from less have le: "c + a <= c + b" by (simp add: order_le_less)
659   have "a <= b"
660     apply (insert le)
662     by (insert le, drule add_le_imp_le_left, assumption)
663   moreover have "a \<noteq> b"
664   proof (rule ccontr)
665     assume "~(a \<noteq> b)"
666     then have "a = b" by simp
667     then have "c + a = c + b" by simp
668     with less show "False"by simp
669   qed
670   ultimately show "a < b" by (simp add: order_le_less)
671 qed
674   "a + c < b + c \<Longrightarrow> a < b"
675 apply (rule add_less_imp_less_left [of c])
677 done
680   "c + a < c + b \<longleftrightarrow> a < b"
684   "a + c < b + c \<longleftrightarrow> a < b"
688   "c + a \<le> c + b \<longleftrightarrow> a \<le> b"
692   "a + c \<le> b + c \<longleftrightarrow> a \<le> b"
696   "a + c \<le> b + c \<Longrightarrow> a \<le> b"
697 by simp
700   "max x y + z = max (x + z) (y + z)"
701   unfolding max_def by auto
704   "min x y + z = min (x + z) (y + z)"
705   unfolding min_def by auto
708   "x + max y z = max (x + y) (x + z)"
709   unfolding max_def by auto
712   "x + min y z = min (x + y) (x + z)"
713   unfolding min_def by auto
715 end
717 class ordered_cancel_comm_monoid_diff = comm_monoid_diff + ordered_ab_semigroup_add_imp_le +
718   assumes le_iff_add: "a \<le> b \<longleftrightarrow> (\<exists>c. b = a + c)"
719 begin
721 context
722   fixes a b
723   assumes "a \<le> b"
724 begin
727   "a + (b - a) = b"
728   using a \<le> b by (auto simp add: le_iff_add)
731   "c + (b - a) = c + b - a"
732   using a \<le> b by (auto simp add: le_iff_add add.left_commute [of c])
735   "b - a + c = b + c - a"
736   using a \<le> b by (auto simp add: le_iff_add add.assoc)
739   "c + b - a = c + (b - a)"
740   using a \<le> b by (simp add: add.commute add_diff_assoc)
743   "b + c - a = b - a + c"
744   using a \<le> bby (simp add: add.commute add_diff_assoc)
746 lemma diff_diff_right:
747   "c - (b - a) = c + a - b"
751   "b - a + a = b"
755   "c \<le> b + c - a"
759   "a \<le> b \<Longrightarrow> b - a = c \<longleftrightarrow> b = c + a"
762 lemma le_diff_conv2:
763   "c \<le> b - a \<longleftrightarrow> c + a \<le> b" (is "?P \<longleftrightarrow> ?Q")
764 proof
765   assume ?P
766   then have "c + a \<le> b - a + a" by (rule add_right_mono)
768 next
769   assume ?Q
770   then have "a + c \<le> a + (b - a)" by (simp add: add_diff_inverse add.commute)
771   then show ?P by simp
772 qed
774 end
776 end
779 subsection {* Support for reasoning about signs *}
783 begin
786   assumes "0 < a" and "0 \<le> b" shows "0 < a + b"
787 proof -
788   have "0 + 0 < a + b"
789     using assms by (rule add_less_le_mono)
790   then show ?thesis by simp
791 qed
794   assumes "0 < a" and "0 < b" shows "0 < a + b"
795 by (rule add_pos_nonneg) (insert assms, auto)
798   assumes "0 \<le> a" and "0 < b" shows "0 < a + b"
799 proof -
800   have "0 + 0 < a + b"
801     using assms by (rule add_le_less_mono)
802   then show ?thesis by simp
803 qed
806   assumes "0 \<le> a" and "0 \<le> b" shows "0 \<le> a + b"
807 proof -
808   have "0 + 0 \<le> a + b"
809     using assms by (rule add_mono)
810   then show ?thesis by simp
811 qed
814   assumes "a < 0" and "b \<le> 0" shows "a + b < 0"
815 proof -
816   have "a + b < 0 + 0"
817     using assms by (rule add_less_le_mono)
818   then show ?thesis by simp
819 qed
822   assumes "a < 0" and "b < 0" shows "a + b < 0"
823 by (rule add_neg_nonpos) (insert assms, auto)
826   assumes "a \<le> 0" and "b < 0" shows "a + b < 0"
827 proof -
828   have "a + b < 0 + 0"
829     using assms by (rule add_le_less_mono)
830   then show ?thesis by simp
831 qed
834   assumes "a \<le> 0" and "b \<le> 0" shows "a + b \<le> 0"
835 proof -
836   have "a + b \<le> 0 + 0"
837     using assms by (rule add_mono)
838   then show ?thesis by simp
839 qed
846   assumes x: "0 \<le> x" and y: "0 \<le> y"
847   shows "x + y = 0 \<longleftrightarrow> x = 0 \<and> y = 0"
848 proof (intro iffI conjI)
849   have "x = x + 0" by simp
850   also have "x + 0 \<le> x + y" using y by (rule add_left_mono)
851   also assume "x + y = 0"
852   also have "0 \<le> x" using x .
853   finally show "x = 0" .
854 next
855   have "y = 0 + y" by simp
856   also have "0 + y \<le> x + y" using x by (rule add_right_mono)
857   also assume "x + y = 0"
858   also have "0 \<le> y" using y .
859   finally show "y = 0" .
860 next
861   assume "x = 0 \<and> y = 0"
862   then show "x + y = 0" by simp
863 qed
866   "0 \<le> a \<Longrightarrow> b \<le> c \<Longrightarrow> b \<le> a + c"
867   by (insert add_mono [of 0 a b c], simp)
870   "0 \<le> c \<Longrightarrow> b \<le> a \<Longrightarrow> b \<le> a + c"
874   "0 < a \<Longrightarrow> b \<le> c \<Longrightarrow> b < a + c"
875   by (insert add_less_le_mono [of 0 a b c], simp)
878   "0 \<le> a \<Longrightarrow> b < c \<Longrightarrow> b < a + c"
879   by (insert add_le_less_mono [of 0 a b c], simp)
881 end
885 begin
890 proof
891   fix a b c :: 'a
892   assume "c + a \<le> c + b"
893   hence "(-c) + (c + a) \<le> (-c) + (c + b)" by (rule add_left_mono)
894   hence "((-c) + c) + a \<le> ((-c) + c) + b" by (simp only: add.assoc)
895   thus "a \<le> b" by simp
896 qed
901   "b + a < b \<longleftrightarrow> a < 0"
902   using add_less_cancel_left [of _ _ 0] by simp
905   "a + b < b \<longleftrightarrow> a < 0"
906   using add_less_cancel_right [of _ _ 0] by simp
909   "a < a + b \<longleftrightarrow> 0 < b"
910   using add_less_cancel_left [of _ 0] by simp
913   "a < b + a \<longleftrightarrow> 0 < b"
914   using add_less_cancel_right [of 0] by simp
917   "b + a \<le> b \<longleftrightarrow> a \<le> 0"
918   using add_le_cancel_left [of _ _ 0] by simp
921   "a + b \<le> b \<longleftrightarrow> a \<le> 0"
922   using add_le_cancel_right [of _ _ 0] by simp
925   "a \<le> a + b \<longleftrightarrow> 0 \<le> b"
926   using add_le_cancel_left [of _ 0] by simp
929   "a \<le> b + a \<longleftrightarrow> 0 \<le> b"
930   using add_le_cancel_right [of 0] by simp
932 lemma max_diff_distrib_left:
933   shows "max x y - z = max (x - z) (y - z)"
934   using max_add_distrib_left [of x y "- z"] by simp
936 lemma min_diff_distrib_left:
937   shows "min x y - z = min (x - z) (y - z)"
938   using min_add_distrib_left [of x y "- z"] by simp
940 lemma le_imp_neg_le:
941   assumes "a \<le> b" shows "-b \<le> -a"
942 proof -
943   have "-a+a \<le> -a+b" using a \<le> b by (rule add_left_mono)
944   then have "0 \<le> -a+b" by simp
945   then have "0 + (-b) \<le> (-a + b) + (-b)" by (rule add_right_mono)
946   then show ?thesis by (simp add: algebra_simps)
947 qed
949 lemma neg_le_iff_le [simp]: "- b \<le> - a \<longleftrightarrow> a \<le> b"
950 proof
951   assume "- b \<le> - a"
952   hence "- (- a) \<le> - (- b)" by (rule le_imp_neg_le)
953   thus "a\<le>b" by simp
954 next
955   assume "a\<le>b"
956   thus "-b \<le> -a" by (rule le_imp_neg_le)
957 qed
959 lemma neg_le_0_iff_le [simp]: "- a \<le> 0 \<longleftrightarrow> 0 \<le> a"
960 by (subst neg_le_iff_le [symmetric], simp)
962 lemma neg_0_le_iff_le [simp]: "0 \<le> - a \<longleftrightarrow> a \<le> 0"
963 by (subst neg_le_iff_le [symmetric], simp)
965 lemma neg_less_iff_less [simp]: "- b < - a \<longleftrightarrow> a < b"
966 by (force simp add: less_le)
968 lemma neg_less_0_iff_less [simp]: "- a < 0 \<longleftrightarrow> 0 < a"
969 by (subst neg_less_iff_less [symmetric], simp)
971 lemma neg_0_less_iff_less [simp]: "0 < - a \<longleftrightarrow> a < 0"
972 by (subst neg_less_iff_less [symmetric], simp)
974 text{*The next several equations can make the simplifier loop!*}
976 lemma less_minus_iff: "a < - b \<longleftrightarrow> b < - a"
977 proof -
978   have "(- (-a) < - b) = (b < - a)" by (rule neg_less_iff_less)
979   thus ?thesis by simp
980 qed
982 lemma minus_less_iff: "- a < b \<longleftrightarrow> - b < a"
983 proof -
984   have "(- a < - (-b)) = (- b < a)" by (rule neg_less_iff_less)
985   thus ?thesis by simp
986 qed
988 lemma le_minus_iff: "a \<le> - b \<longleftrightarrow> b \<le> - a"
989 proof -
990   have mm: "!! a (b::'a). (-(-a)) < -b \<Longrightarrow> -(-b) < -a" by (simp only: minus_less_iff)
991   have "(- (- a) <= -b) = (b <= - a)"
992     apply (auto simp only: le_less)
993     apply (drule mm)
994     apply (simp_all)
995     apply (drule mm[simplified], assumption)
996     done
997   then show ?thesis by simp
998 qed
1000 lemma minus_le_iff: "- a \<le> b \<longleftrightarrow> - b \<le> a"
1001 by (auto simp add: le_less minus_less_iff)
1003 lemma diff_less_0_iff_less [simp]:
1004   "a - b < 0 \<longleftrightarrow> a < b"
1005 proof -
1006   have "a - b < 0 \<longleftrightarrow> a + (- b) < b + (- b)" by simp
1007   also have "... \<longleftrightarrow> a < b" by (simp only: add_less_cancel_right)
1008   finally show ?thesis .
1009 qed
1011 lemmas less_iff_diff_less_0 = diff_less_0_iff_less [symmetric]
1013 lemma diff_less_eq [algebra_simps, field_simps]:
1014   "a - b < c \<longleftrightarrow> a < c + b"
1015 apply (subst less_iff_diff_less_0 [of a])
1016 apply (rule less_iff_diff_less_0 [of _ c, THEN ssubst])
1018 done
1020 lemma less_diff_eq[algebra_simps, field_simps]:
1021   "a < c - b \<longleftrightarrow> a + b < c"
1022 apply (subst less_iff_diff_less_0 [of "a + b"])
1023 apply (subst less_iff_diff_less_0 [of a])
1025 done
1027 lemma diff_le_eq[algebra_simps, field_simps]: "a - b \<le> c \<longleftrightarrow> a \<le> c + b"
1028 by (auto simp add: le_less diff_less_eq )
1030 lemma le_diff_eq[algebra_simps, field_simps]: "a \<le> c - b \<longleftrightarrow> a + b \<le> c"
1031 by (auto simp add: le_less less_diff_eq)
1033 lemma diff_le_0_iff_le [simp]:
1034   "a - b \<le> 0 \<longleftrightarrow> a \<le> b"
1037 lemmas le_iff_diff_le_0 = diff_le_0_iff_le [symmetric]
1039 lemma diff_eq_diff_less:
1040   "a - b = c - d \<Longrightarrow> a < b \<longleftrightarrow> c < d"
1041   by (auto simp only: less_iff_diff_less_0 [of a b] less_iff_diff_less_0 [of c d])
1043 lemma diff_eq_diff_less_eq:
1044   "a - b = c - d \<Longrightarrow> a \<le> b \<longleftrightarrow> c \<le> d"
1045   by (auto simp only: le_iff_diff_le_0 [of a b] le_iff_diff_le_0 [of c d])
1047 lemma diff_mono: "a \<le> b \<Longrightarrow> d \<le> c \<Longrightarrow> a - c \<le> b - d"
1050 lemma diff_left_mono: "b \<le> a \<Longrightarrow> c - a \<le> c - b"
1053 lemma diff_right_mono: "a \<le> b \<Longrightarrow> a - c \<le> b - c"
1056 lemma diff_strict_mono: "a < b \<Longrightarrow> d < c \<Longrightarrow> a - c < b - d"
1059 lemma diff_strict_left_mono: "b < a \<Longrightarrow> c - a < c - b"
1062 lemma diff_strict_right_mono: "a < b \<Longrightarrow> a - c < b - c"
1065 end
1067 ML_file "Tools/group_cancel.ML"
1070   {* fn phi => fn ss => try Group_Cancel.cancel_add_conv *}
1072 simproc_setup group_cancel_diff ("a - b::'a::ab_group_add") =
1073   {* fn phi => fn ss => try Group_Cancel.cancel_diff_conv *}
1075 simproc_setup group_cancel_eq ("a = (b::'a::ab_group_add)") =
1076   {* fn phi => fn ss => try Group_Cancel.cancel_eq_conv *}
1078 simproc_setup group_cancel_le ("a \<le> (b::'a::ordered_ab_group_add)") =
1079   {* fn phi => fn ss => try Group_Cancel.cancel_le_conv *}
1081 simproc_setup group_cancel_less ("a < (b::'a::ordered_ab_group_add)") =
1082   {* fn phi => fn ss => try Group_Cancel.cancel_less_conv *}
1089 begin
1094 proof
1095   fix a b c :: 'a
1096   assume le: "c + a <= c + b"
1097   show "a <= b"
1098   proof (rule ccontr)
1099     assume w: "~ a \<le> b"
1100     hence "b <= a" by (simp add: linorder_not_le)
1101     hence le2: "c + b <= c + a" by (rule add_left_mono)
1102     have "a = b"
1103       apply (insert le)
1104       apply (insert le2)
1105       apply (drule antisym, simp_all)
1106       done
1107     with w show False
1108       by (simp add: linorder_not_le [symmetric])
1109   qed
1110 qed
1112 end
1115 begin
1119 lemma equal_neg_zero [simp]:
1120   "a = - a \<longleftrightarrow> a = 0"
1121 proof
1122   assume "a = 0" then show "a = - a" by simp
1123 next
1124   assume A: "a = - a" show "a = 0"
1125   proof (cases "0 \<le> a")
1126     case True with A have "0 \<le> - a" by auto
1127     with le_minus_iff have "a \<le> 0" by simp
1128     with True show ?thesis by (auto intro: order_trans)
1129   next
1130     case False then have B: "a \<le> 0" by auto
1131     with A have "- a \<le> 0" by auto
1132     with B show ?thesis by (auto intro: order_trans)
1133   qed
1134 qed
1136 lemma neg_equal_zero [simp]:
1137   "- a = a \<longleftrightarrow> a = 0"
1138   by (auto dest: sym)
1140 lemma neg_less_eq_nonneg [simp]:
1141   "- a \<le> a \<longleftrightarrow> 0 \<le> a"
1142 proof
1143   assume A: "- a \<le> a" show "0 \<le> a"
1144   proof (rule classical)
1145     assume "\<not> 0 \<le> a"
1146     then have "a < 0" by auto
1147     with A have "- a < 0" by (rule le_less_trans)
1148     then show ?thesis by auto
1149   qed
1150 next
1151   assume A: "0 \<le> a" show "- a \<le> a"
1152   proof (rule order_trans)
1153     show "- a \<le> 0" using A by (simp add: minus_le_iff)
1154   next
1155     show "0 \<le> a" using A .
1156   qed
1157 qed
1159 lemma neg_less_pos [simp]:
1160   "- a < a \<longleftrightarrow> 0 < a"
1161   by (auto simp add: less_le)
1163 lemma less_eq_neg_nonpos [simp]:
1164   "a \<le> - a \<longleftrightarrow> a \<le> 0"
1165   using neg_less_eq_nonneg [of "- a"] by simp
1167 lemma less_neg_neg [simp]:
1168   "a < - a \<longleftrightarrow> a < 0"
1169   using neg_less_pos [of "- a"] by simp
1171 lemma double_zero [simp]:
1172   "a + a = 0 \<longleftrightarrow> a = 0"
1173 proof
1174   assume assm: "a + a = 0"
1175   then have a: "- a = a" by (rule minus_unique)
1176   then show "a = 0" by (simp only: neg_equal_zero)
1177 qed simp
1179 lemma double_zero_sym [simp]:
1180   "0 = a + a \<longleftrightarrow> a = 0"
1181   by (rule, drule sym) simp_all
1184   "0 < a + a \<longleftrightarrow> 0 < a"
1185 proof
1186   assume "0 < a + a"
1187   then have "0 - a < a" by (simp only: diff_less_eq)
1188   then have "- a < a" by simp
1189   then show "0 < a" by simp
1190 next
1191   assume "0 < a"
1192   with this have "0 + 0 < a + a"
1194   then show "0 < a + a" by simp
1195 qed
1198   "0 \<le> a + a \<longleftrightarrow> 0 \<le> a"
1199   by (auto simp add: le_less)
1202   "a + a < 0 \<longleftrightarrow> a < 0"
1203 proof -
1204   have "\<not> a + a < 0 \<longleftrightarrow> \<not> a < 0"
1206   then show ?thesis by simp
1207 qed
1210   "a + a \<le> 0 \<longleftrightarrow> a \<le> 0"
1211 proof -
1212   have "\<not> a + a \<le> 0 \<longleftrightarrow> \<not> a \<le> 0"
1214   then show ?thesis by simp
1215 qed
1217 lemma minus_max_eq_min:
1218   "- max x y = min (-x) (-y)"
1219   by (auto simp add: max_def min_def)
1221 lemma minus_min_eq_max:
1222   "- min x y = max (-x) (-y)"
1223   by (auto simp add: max_def min_def)
1225 end
1227 class abs =
1228   fixes abs :: "'a \<Rightarrow> 'a"
1229 begin
1231 notation (xsymbols)
1232   abs  ("\<bar>_\<bar>")
1234 notation (HTML output)
1235   abs  ("\<bar>_\<bar>")
1237 end
1239 class sgn =
1240   fixes sgn :: "'a \<Rightarrow> 'a"
1242 class abs_if = minus + uminus + ord + zero + abs +
1243   assumes abs_if: "\<bar>a\<bar> = (if a < 0 then - a else a)"
1245 class sgn_if = minus + uminus + zero + one + ord + sgn +
1246   assumes sgn_if: "sgn x = (if x = 0 then 0 else if 0 < x then 1 else - 1)"
1247 begin
1249 lemma sgn0 [simp]: "sgn 0 = 0"
1252 end
1255   assumes abs_ge_zero [simp]: "\<bar>a\<bar> \<ge> 0"
1256     and abs_ge_self: "a \<le> \<bar>a\<bar>"
1257     and abs_leI: "a \<le> b \<Longrightarrow> - a \<le> b \<Longrightarrow> \<bar>a\<bar> \<le> b"
1258     and abs_minus_cancel [simp]: "\<bar>-a\<bar> = \<bar>a\<bar>"
1259     and abs_triangle_ineq: "\<bar>a + b\<bar> \<le> \<bar>a\<bar> + \<bar>b\<bar>"
1260 begin
1262 lemma abs_minus_le_zero: "- \<bar>a\<bar> \<le> 0"
1263   unfolding neg_le_0_iff_le by simp
1265 lemma abs_of_nonneg [simp]:
1266   assumes nonneg: "0 \<le> a" shows "\<bar>a\<bar> = a"
1267 proof (rule antisym)
1268   from nonneg le_imp_neg_le have "- a \<le> 0" by simp
1269   from this nonneg have "- a \<le> a" by (rule order_trans)
1270   then show "\<bar>a\<bar> \<le> a" by (auto intro: abs_leI)
1271 qed (rule abs_ge_self)
1273 lemma abs_idempotent [simp]: "\<bar>\<bar>a\<bar>\<bar> = \<bar>a\<bar>"
1274 by (rule antisym)
1275    (auto intro!: abs_ge_self abs_leI order_trans [of "- \<bar>a\<bar>" 0 "\<bar>a\<bar>"])
1277 lemma abs_eq_0 [simp]: "\<bar>a\<bar> = 0 \<longleftrightarrow> a = 0"
1278 proof -
1279   have "\<bar>a\<bar> = 0 \<Longrightarrow> a = 0"
1280   proof (rule antisym)
1281     assume zero: "\<bar>a\<bar> = 0"
1282     with abs_ge_self show "a \<le> 0" by auto
1283     from zero have "\<bar>-a\<bar> = 0" by simp
1284     with abs_ge_self [of "- a"] have "- a \<le> 0" by auto
1285     with neg_le_0_iff_le show "0 \<le> a" by auto
1286   qed
1287   then show ?thesis by auto
1288 qed
1290 lemma abs_zero [simp]: "\<bar>0\<bar> = 0"
1291 by simp
1293 lemma abs_0_eq [simp]: "0 = \<bar>a\<bar> \<longleftrightarrow> a = 0"
1294 proof -
1295   have "0 = \<bar>a\<bar> \<longleftrightarrow> \<bar>a\<bar> = 0" by (simp only: eq_ac)
1296   thus ?thesis by simp
1297 qed
1299 lemma abs_le_zero_iff [simp]: "\<bar>a\<bar> \<le> 0 \<longleftrightarrow> a = 0"
1300 proof
1301   assume "\<bar>a\<bar> \<le> 0"
1302   then have "\<bar>a\<bar> = 0" by (rule antisym) simp
1303   thus "a = 0" by simp
1304 next
1305   assume "a = 0"
1306   thus "\<bar>a\<bar> \<le> 0" by simp
1307 qed
1309 lemma zero_less_abs_iff [simp]: "0 < \<bar>a\<bar> \<longleftrightarrow> a \<noteq> 0"
1312 lemma abs_not_less_zero [simp]: "\<not> \<bar>a\<bar> < 0"
1313 proof -
1314   have a: "\<And>x y. x \<le> y \<Longrightarrow> \<not> y < x" by auto
1315   show ?thesis by (simp add: a)
1316 qed
1318 lemma abs_ge_minus_self: "- a \<le> \<bar>a\<bar>"
1319 proof -
1320   have "- a \<le> \<bar>-a\<bar>" by (rule abs_ge_self)
1321   then show ?thesis by simp
1322 qed
1324 lemma abs_minus_commute:
1325   "\<bar>a - b\<bar> = \<bar>b - a\<bar>"
1326 proof -
1327   have "\<bar>a - b\<bar> = \<bar>- (a - b)\<bar>" by (simp only: abs_minus_cancel)
1328   also have "... = \<bar>b - a\<bar>" by simp
1329   finally show ?thesis .
1330 qed
1332 lemma abs_of_pos: "0 < a \<Longrightarrow> \<bar>a\<bar> = a"
1333 by (rule abs_of_nonneg, rule less_imp_le)
1335 lemma abs_of_nonpos [simp]:
1336   assumes "a \<le> 0" shows "\<bar>a\<bar> = - a"
1337 proof -
1338   let ?b = "- a"
1339   have "- ?b \<le> 0 \<Longrightarrow> \<bar>- ?b\<bar> = - (- ?b)"
1340   unfolding abs_minus_cancel [of "?b"]
1341   unfolding neg_le_0_iff_le [of "?b"]
1342   unfolding minus_minus by (erule abs_of_nonneg)
1343   then show ?thesis using assms by auto
1344 qed
1346 lemma abs_of_neg: "a < 0 \<Longrightarrow> \<bar>a\<bar> = - a"
1347 by (rule abs_of_nonpos, rule less_imp_le)
1349 lemma abs_le_D1: "\<bar>a\<bar> \<le> b \<Longrightarrow> a \<le> b"
1350 by (insert abs_ge_self, blast intro: order_trans)
1352 lemma abs_le_D2: "\<bar>a\<bar> \<le> b \<Longrightarrow> - a \<le> b"
1353 by (insert abs_le_D1 [of "- a"], simp)
1355 lemma abs_le_iff: "\<bar>a\<bar> \<le> b \<longleftrightarrow> a \<le> b \<and> - a \<le> b"
1356 by (blast intro: abs_leI dest: abs_le_D1 abs_le_D2)
1358 lemma abs_triangle_ineq2: "\<bar>a\<bar> - \<bar>b\<bar> \<le> \<bar>a - b\<bar>"
1359 proof -
1360   have "\<bar>a\<bar> = \<bar>b + (a - b)\<bar>"
1362   then have "\<bar>a\<bar> \<le> \<bar>b\<bar> + \<bar>a - b\<bar>"
1364   then show ?thesis
1366 qed
1368 lemma abs_triangle_ineq2_sym: "\<bar>a\<bar> - \<bar>b\<bar> \<le> \<bar>b - a\<bar>"
1369   by (simp only: abs_minus_commute [of b] abs_triangle_ineq2)
1371 lemma abs_triangle_ineq3: "\<bar>\<bar>a\<bar> - \<bar>b\<bar>\<bar> \<le> \<bar>a - b\<bar>"
1372   by (simp add: abs_le_iff abs_triangle_ineq2 abs_triangle_ineq2_sym)
1374 lemma abs_triangle_ineq4: "\<bar>a - b\<bar> \<le> \<bar>a\<bar> + \<bar>b\<bar>"
1375 proof -
1376   have "\<bar>a - b\<bar> = \<bar>a + - b\<bar>" by (simp add: algebra_simps)
1377   also have "... \<le> \<bar>a\<bar> + \<bar>- b\<bar>" by (rule abs_triangle_ineq)
1378   finally show ?thesis by simp
1379 qed
1381 lemma abs_diff_triangle_ineq: "\<bar>a + b - (c + d)\<bar> \<le> \<bar>a - c\<bar> + \<bar>b - d\<bar>"
1382 proof -
1383   have "\<bar>a + b - (c+d)\<bar> = \<bar>(a-c) + (b-d)\<bar>" by (simp add: algebra_simps)
1384   also have "... \<le> \<bar>a-c\<bar> + \<bar>b-d\<bar>" by (rule abs_triangle_ineq)
1385   finally show ?thesis .
1386 qed
1389   "\<bar>\<bar>a\<bar> + \<bar>b\<bar>\<bar> = \<bar>a\<bar> + \<bar>b\<bar>" (is "?L = ?R")
1390 proof (rule antisym)
1391   show "?L \<ge> ?R" by(rule abs_ge_self)
1392 next
1393   have "?L \<le> \<bar>\<bar>a\<bar>\<bar> + \<bar>\<bar>b\<bar>\<bar>" by(rule abs_triangle_ineq)
1394   also have "\<dots> = ?R" by simp
1395   finally show "?L \<le> ?R" .
1396 qed
1398 end
1401 subsection {* Tools setup *}
1404   fixes i j k :: "'a\<Colon>ordered_ab_semigroup_add"
1405   shows "i \<le> j \<and> k \<le> l \<Longrightarrow> i + k \<le> j + l"
1406     and "i = j \<and> k \<le> l \<Longrightarrow> i + k \<le> j + l"
1407     and "i \<le> j \<and> k = l \<Longrightarrow> i + k \<le> j + l"
1408     and "i = j \<and> k = l \<Longrightarrow> i + k = j + l"