src/HOL/OrderedGroup.thy
 changeset 23085 fd30d75a6614 parent 22997 d4f3b015b50b child 23181 f52b555f8141
--- a/src/HOL/OrderedGroup.thy	Wed May 23 19:23:22 2007 +0200
+++ b/src/HOL/OrderedGroup.thy	Thu May 24 07:27:44 2007 +0200
@@ -24,7 +24,7 @@
\end{itemize}
*}

-subsection {* Semigroups, Groups *}
+subsection {* Semigroups and Monoids *}

assumes add_assoc: "(a \<^loc>+ b) \<^loc>+ c = a \<^loc>+ (b \<^loc>+ c)"
@@ -48,8 +48,14 @@

theorems mult_ac = mult_assoc mult_commute mult_left_commute

+  assumes add_0_left [simp]: "\<^loc>0 \<^loc>+ a = a" and add_0_right [simp]: "a \<^loc>+ \<^loc>0 = a"
+
-  assumes add_0 [simp]: "\<^loc>0 \<^loc>+ a = a"
+  assumes add_0: "\<^loc>0 \<^loc>+ a = a"
+

class monoid_mult = one + semigroup_mult +
assumes mult_1_left [simp]: "\<^loc>1 \<^loc>* a  = a"
@@ -80,80 +86,89 @@
then show "b = c" by (rule add_imp_eq)
qed

+  "a + b = a + c \<longleftrightarrow> b = (c \<Colon> 'a\<Colon>cancel_semigroup_add)"
+
+  "b + a = c + a \<longleftrightarrow> b = (c \<Colon> 'a\<Colon>cancel_semigroup_add)"
+
+subsection {* Groups *}
+
+  assumes ab_left_minus: "uminus a \<^loc>+ a = \<^loc>0"
+  assumes ab_diff_minus: "a \<^loc>- b = a \<^loc>+ (uminus b)"
+
assumes left_minus [simp]: "uminus a \<^loc>+ a = \<^loc>0"
assumes diff_minus: "a \<^loc>- b = a \<^loc>+ (uminus b)"

+by intro_classes (simp_all add: ab_left_minus ab_diff_minus)
+
proof intro_classes
fix a b c :: 'a
assume "a + b = a + c"
then have "uminus a + a + b = uminus a + a + c" unfolding add_assoc by simp
-  then show "b = c" by simp
+  then show "b = c" by simp
qed

+
proof -
-  have "a + 0 = 0 + a" by (simp only: add_commute)
-  also have "... = a" by simp
+  also have "\<dots> = 0" by(rule minus_add_cancel)
finally show ?thesis .
qed

-
-  "a + b = a + c \<longleftrightarrow> b = (c \<Colon> 'a\<Colon>cancel_semigroup_add)"
+lemma minus_minus[simp]: "- (-(a::'a::group_add)) = a"
+proof -
+  have "-(-a) = -(-a) + (-a + a)" by simp
+  also have "\<dots> = a" by(rule minus_add_cancel)
+  finally show ?thesis .
+qed

-  "b + a = c + a \<longleftrightarrow> b = (c \<Colon> 'a\<Colon>cancel_semigroup_add)"
-
-lemma right_minus [simp]: "a + -(a::'a::ab_group_add) = 0"
+lemma right_minus[simp]: "a + - a = (0::'a::group_add)"
proof -
-  have "a + -a = -a + a" by (simp add: add_ac)
-  also have "... = 0" by simp
+  have "a + -a = -(-a) + -a" by simp
+  also have "\<dots> = 0" thm group_add.left_minus by(rule left_minus)
finally show ?thesis .
qed

-lemma right_minus_eq: "(a - b = 0) = (a = (b::'a::ab_group_add))"
+lemma right_minus_eq: "(a - b = 0) = (a = (b::'a::group_add))"
proof
-  have "a = a - b + b" by (simp add: diff_minus add_ac)
-  also assume "a - b = 0"
-  finally show "a = b" by simp
+  assume "a - b = 0"
+  have "a = (a - b) + b" by (simp add:diff_minus add_assoc)
+  also have "\<dots> = b" using a - b = 0 by simp
+  finally show "a = b" .
next
-  assume "a = b"
-  thus "a - b = 0" by (simp add: diff_minus)
-qed
-
-lemma minus_minus [simp]: "- (- (a::'a::ab_group_add)) = a"
-proof (rule add_left_cancel [of "-a", THEN iffD1])
-  show "(-a + -(-a) = -a + a)"
-  by simp
+  assume "a = b" thus "a - b = 0" by (simp add: diff_minus)
qed

-lemma equals_zero_I: "a+b = 0 ==> -a = (b::'a::ab_group_add)"
-apply (rule right_minus_eq [THEN iffD1, symmetric])
-done
+lemma equals_zero_I: assumes "a+b = 0" shows "-a = (b::'a::group_add)"
+proof -
+  have "- a = -a + (a+b)" using assms by simp
+  finally show ?thesis .
+qed

-lemma minus_zero [simp]: "- 0 = (0::'a::ab_group_add)"
+lemma diff_self[simp]: "(a::'a::group_add) - a = 0"

-lemma diff_self [simp]: "a - (a::'a::ab_group_add) = 0"
-
-lemma diff_0 [simp]: "(0::'a::ab_group_add) - a = -a"
+lemma diff_0 [simp]: "(0::'a::group_add) - a = -a"

-lemma diff_0_right [simp]: "a - (0::'a::ab_group_add) = a"
+lemma diff_0_right [simp]: "a - (0::'a::group_add) = a"

-lemma neg_equal_iff_equal [simp]: "(-a = -b) = (a = (b::'a::ab_group_add))"
+lemma neg_equal_iff_equal [simp]: "(-a = -b) = (a = (b::'a::group_add))"
proof
assume "- a = - b"
hence "- (- a) = - (- b)"
@@ -164,21 +179,21 @@
thus "-a = -b" by simp
qed

-lemma neg_equal_0_iff_equal [simp]: "(-a = 0) = (a = (0::'a::ab_group_add))"
+lemma neg_equal_0_iff_equal [simp]: "(-a = 0) = (a = (0::'a::group_add))"
by (subst neg_equal_iff_equal [symmetric], simp)

-lemma neg_0_equal_iff_equal [simp]: "(0 = -a) = (0 = (a::'a::ab_group_add))"
+lemma neg_0_equal_iff_equal [simp]: "(0 = -a) = (0 = (a::'a::group_add))"
by (subst neg_equal_iff_equal [symmetric], simp)

text{*The next two equations can make the simplifier loop!*}

-lemma equation_minus_iff: "(a = - b) = (b = - (a::'a::ab_group_add))"
+lemma equation_minus_iff: "(a = - b) = (b = - (a::'a::group_add))"
proof -
have "(- (-a) = - b) = (- a = b)" by (rule neg_equal_iff_equal)
thus ?thesis by (simp add: eq_commute)
qed

-lemma minus_equation_iff: "(- a = b) = (- (b::'a::ab_group_add) = a)"
+lemma minus_equation_iff: "(- a = b) = (- (b::'a::group_add) = a)"
proof -
have "(- a = - (-b)) = (a = -b)" by (rule neg_equal_iff_equal)
thus ?thesis by (simp add: eq_commute)
@@ -186,7 +201,7 @@

apply (rule equals_zero_I)
done

lemma minus_diff_eq [simp]: "- (a - b) = b - (a::'a::ab_group_add)"
@@ -1009,9 +1024,6 @@

-
assumes
@@ -1082,7 +1094,7 @@

val cancel_ss = HOL_basic_ss settermless termless_agrp
@{thm minus_add_cancel}];