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"