# HG changeset patch
# User paulson
# Date 1033115701 -7200
# Node ID e14d963e3bc05e8c3417d839c458359109b588dd
# Parent  d8e98ef3ad1333a364780f1bde48c143e219efd5
Isar proof

diff -r d8e98ef3ad13 -r e14d963e3bc0 src/HOL/GroupTheory/Group.thy
--- a/src/HOL/GroupTheory/Group.thy	Fri Sep 27 10:34:05 2002 +0200
+++ b/src/HOL/GroupTheory/Group.thy	Fri Sep 27 10:35:01 2002 +0200
@@ -74,6 +74,11 @@
 locale abelian_group = group +
   assumes sum_commute: "[|x \<in> carrier G; y \<in> carrier G|] ==> x \<oplus> y = y \<oplus> x"
 
+lemma abelian_group_iff:
+     "abelian_group G = 
+      (group G & (\<forall>x \<in> carrier G. \<forall>y \<in> carrier G. sum G x y = sum G y x))"
+by (force simp add: abelian_group_axioms_def abelian_group_def group_def) 
+
 
 subsection{*Basic Group Theory Theorems*}
 
@@ -90,23 +95,14 @@
 done
 
 lemma (in group) left_cancellation:
-     "[| x \<oplus> y  =  x \<oplus> z;
-         x  \<in> carrier G ; y \<in> carrier G; z \<in> carrier G |]  
-      ==> y = z"
-apply (drule arg_cong [of concl: "%z. (\<ominus>x) \<oplus> z"])
-apply (simp add: sum_assoc [symmetric])
-done
-
-(*Isar version??
-lemma (in group) left_cancellation:
   assumes eq: "x \<oplus> y  =  x \<oplus> z"
-  shows   "[| x \<in> carrier G ; y \<in> carrier G; z \<in> carrier G |]  
-      ==> y = z"
+      and inG: "x \<in> carrier G" "y \<in> carrier G" "z \<in> carrier G" 
+  shows "y = z"
 proof -
-  have "(\<ominus>x) \<oplus> (x \<oplus> y) = (\<ominus>x) \<oplus> (x \<oplus> z)" by (simp only: eq)
-  assume ?this 
-  have "((\<ominus>x) \<oplus> x) \<oplus> y = ((\<ominus>x) \<oplus> x) \<oplus> z" by (simp only: sum_assoc) 
-*)
+  have "((\<ominus>x) \<oplus> x) \<oplus> y = ((\<ominus>x) \<oplus> x) \<oplus> z" 
+        by (simp only: eq inG minus_closed sum_assoc) 
+  then show ?thesis by (simp only: inG left_minus left_zero) 
+qed
 
 lemma (in group) left_cancellation_iff [simp]:
      "[| x \<in> carrier G; y \<in> carrier G; z \<in> carrier G |]