src/HOL/Groups.thy
changeset 40368 47c186c8577d
parent 39134 917b4b6ba3d2
child 42245 29e3967550d5
     1.1 --- a/src/HOL/Groups.thy	Fri Nov 05 09:07:14 2010 +0100
     1.2 +++ b/src/HOL/Groups.thy	Fri Nov 05 14:10:41 2010 +0100
     1.3 @@ -284,6 +284,7 @@
     1.4    finally show ?thesis .
     1.5  qed
     1.6  
     1.7 +
     1.8  lemmas equals_zero_I = minus_unique (* legacy name *)
     1.9  
    1.10  lemma minus_zero [simp]: "- 0 = 0"
    1.11 @@ -305,6 +306,20 @@
    1.12    finally show ?thesis .
    1.13  qed
    1.14  
    1.15 +subclass cancel_semigroup_add
    1.16 +proof
    1.17 +  fix a b c :: 'a
    1.18 +  assume "a + b = a + c"
    1.19 +  then have "- a + a + b = - a + a + c"
    1.20 +    unfolding add_assoc by simp
    1.21 +  then show "b = c" by simp
    1.22 +next
    1.23 +  fix a b c :: 'a
    1.24 +  assume "b + a = c + a"
    1.25 +  then have "b + a + - a = c + a  + - a" by simp
    1.26 +  then show "b = c" unfolding add_assoc by simp
    1.27 +qed
    1.28 +
    1.29  lemma minus_add_cancel: "- a + (a + b) = b"
    1.30  by (simp add: add_assoc [symmetric])
    1.31