--- a/src/HOL/Groups.thy Fri Nov 05 09:07:14 2010 +0100
+++ b/src/HOL/Groups.thy Fri Nov 05 14:10:41 2010 +0100
@@ -284,6 +284,7 @@
finally show ?thesis .
qed
+
lemmas equals_zero_I = minus_unique (* legacy name *)
lemma minus_zero [simp]: "- 0 = 0"
@@ -305,6 +306,20 @@
finally show ?thesis .
qed
+subclass cancel_semigroup_add
+proof
+ fix a b c :: 'a
+ assume "a + b = a + c"
+ then have "- a + a + b = - a + a + c"
+ unfolding add_assoc by simp
+ then show "b = c" by simp
+next
+ fix a b c :: 'a
+ assume "b + a = c + a"
+ then have "b + a + - a = c + a + - a" by simp
+ then show "b = c" unfolding add_assoc by simp
+qed
+
lemma minus_add_cancel: "- a + (a + b) = b"
by (simp add: add_assoc [symmetric])