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. *)