# HG changeset patch
# User haftmann
# Date 1288962641 -3600
# Node ID 47c186c8577d7bbe453c48b748b62197d2b41c61
# Parent  6fb991dc074b974abce1e6b482707f740a902b03
added class relation group_add < cancel_semigroup_add

diff -r 6fb991dc074b -r 47c186c8577d src/HOL/Groups.thy
--- 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])