src/HOL/Algebra/Group.thy
changeset 68399 0b71d08528f0
parent 68188 2af1f142f855
child 68443 43055b016688
     1.1 --- a/src/HOL/Algebra/Group.thy	Tue Jun 05 16:35:52 2018 +0200
     1.2 +++ b/src/HOL/Algebra/Group.thy	Wed Jun 06 14:25:53 2018 +0100
     1.3 @@ -324,39 +324,19 @@
     1.4  
     1.5  lemma (in group) l_inv [simp]:
     1.6    "x \<in> carrier G ==> inv x \<otimes> x = \<one>"
     1.7 -  using Units_l_inv by simp
     1.8 +  by simp
     1.9  
    1.10  
    1.11  subsection \<open>Cancellation Laws and Basic Properties\<close>
    1.12  
    1.13 -lemma (in group) l_cancel [simp]:
    1.14 -  "[| x \<in> carrier G; y \<in> carrier G; z \<in> carrier G |] ==>
    1.15 -   (x \<otimes> y = x \<otimes> z) = (y = z)"
    1.16 -  using Units_l_inv by simp
    1.17 -
    1.18  lemma (in group) r_inv [simp]:
    1.19    "x \<in> carrier G ==> x \<otimes> inv x = \<one>"
    1.20 -proof -
    1.21 -  assume x: "x \<in> carrier G"
    1.22 -  then have "inv x \<otimes> (x \<otimes> inv x) = inv x \<otimes> \<one>"
    1.23 -    by (simp add: m_assoc [symmetric])
    1.24 -  with x show ?thesis by (simp del: r_one)
    1.25 -qed
    1.26 +  by simp
    1.27  
    1.28 -lemma (in group) r_cancel [simp]:
    1.29 +lemma (in group) right_cancel [simp]:
    1.30    "[| x \<in> carrier G; y \<in> carrier G; z \<in> carrier G |] ==>
    1.31     (y \<otimes> x = z \<otimes> x) = (y = z)"
    1.32 -proof
    1.33 -  assume eq: "y \<otimes> x = z \<otimes> x"
    1.34 -    and G: "x \<in> carrier G"  "y \<in> carrier G"  "z \<in> carrier G"
    1.35 -  then have "y \<otimes> (x \<otimes> inv x) = z \<otimes> (x \<otimes> inv x)"
    1.36 -    by (simp add: m_assoc [symmetric] del: r_inv Units_r_inv)
    1.37 -  with G show "y = z" by simp
    1.38 -next
    1.39 -  assume eq: "y = z"
    1.40 -    and G: "x \<in> carrier G"  "y \<in> carrier G"  "z \<in> carrier G"
    1.41 -  then show "y \<otimes> x = z \<otimes> x" by simp
    1.42 -qed
    1.43 +  by (metis inv_closed m_assoc r_inv r_one)
    1.44  
    1.45  lemma (in group) inv_one [simp]:
    1.46    "inv \<one> = \<one>"
    1.47 @@ -389,11 +369,7 @@
    1.48  
    1.49  lemma (in group) inv_equality:
    1.50       "[|y \<otimes> x = \<one>; x \<in> carrier G; y \<in> carrier G|] ==> inv x = y"
    1.51 -apply (simp add: m_inv_def)
    1.52 -apply (rule the_equality)
    1.53 - apply (simp add: inv_comm [of y x])
    1.54 -apply (rule r_cancel [THEN iffD1], auto)
    1.55 -done
    1.56 +  using inv_unique r_inv by blast
    1.57  
    1.58  (* Contributed by Joachim Breitner *)
    1.59  lemma (in group) inv_solve_left: