src/HOL/Algebra/More_Group.thy
 changeset 68399 0b71d08528f0 parent 67341 df79ef3b3a41
```     1.1 --- a/src/HOL/Algebra/More_Group.thy	Tue Jun 05 16:35:52 2018 +0200
1.2 +++ b/src/HOL/Algebra/More_Group.thy	Wed Jun 06 14:25:53 2018 +0100
1.3 @@ -81,31 +81,16 @@
1.4    done
1.5
1.6  lemma (in group) l_cancel_one [simp]: "x \<in> carrier G \<Longrightarrow> a \<in> carrier G \<Longrightarrow> x \<otimes> a = x \<longleftrightarrow> a = one G"
1.7 -  apply auto
1.8 -  apply (subst l_cancel [symmetric])
1.9 -     prefer 4
1.10 -     apply (erule ssubst)
1.11 -     apply auto
1.12 -  done
1.13 +  by (metis Units_eq Units_l_cancel monoid.r_one monoid_axioms one_closed)
1.14
1.15  lemma (in group) r_cancel_one [simp]: "x \<in> carrier G \<Longrightarrow> a \<in> carrier G \<Longrightarrow> a \<otimes> x = x \<longleftrightarrow> a = one G"
1.16 -  apply auto
1.17 -  apply (subst r_cancel [symmetric])
1.18 -     prefer 4
1.19 -     apply (erule ssubst)
1.20 -     apply auto
1.21 -  done
1.22 +  by (metis monoid.l_one monoid_axioms one_closed right_cancel)
1.23
1.24 -(* Is there a better way to do this? *)
1.25  lemma (in group) l_cancel_one' [simp]: "x \<in> carrier G \<Longrightarrow> a \<in> carrier G \<Longrightarrow> x = x \<otimes> a \<longleftrightarrow> a = one G"
1.26 -  apply (subst eq_commute)
1.27 -  apply simp
1.28 -  done
1.29 +  using l_cancel_one by fastforce
1.30
1.31  lemma (in group) r_cancel_one' [simp]: "x \<in> carrier G \<Longrightarrow> a \<in> carrier G \<Longrightarrow> x = a \<otimes> x \<longleftrightarrow> a = one G"
1.32 -  apply (subst eq_commute)
1.33 -  apply simp
1.34 -  done
1.35 +  using r_cancel_one by fastforce
1.36
1.37  (* This should be generalized to arbitrary groups, not just commutative
1.38     ones, using Lagrange's theorem. *)
```