src/HOL/Algebra/Group.thy
 changeset 13940 c67798653056 parent 13936 d3671b878828 child 13943 83d842ccd4aa
```     1.1 --- a/src/HOL/Algebra/Group.thy	Wed Apr 30 18:31:38 2003 +0200
1.2 +++ b/src/HOL/Algebra/Group.thy	Wed Apr 30 18:32:06 2003 +0200
1.3 @@ -93,6 +93,10 @@
1.4    finally show ?thesis .
1.5  qed
1.6
1.7 +lemma (in monoid) Units_one_closed [intro, simp]:
1.8 +  "\<one> \<in> Units G"
1.9 +  by (unfold Units_def) auto
1.10 +
1.11  lemma (in monoid) Units_inv_closed [intro, simp]:
1.12    "x \<in> Units G ==> inv x \<in> carrier G"
1.13    apply (unfold Units_def m_inv_def)
1.14 @@ -162,6 +166,15 @@
1.15    with G show "x = y" by simp
1.16  qed
1.17
1.18 +lemma (in monoid) Units_inv_comm:
1.19 +  assumes inv: "x \<otimes> y = \<one>"
1.20 +    and G: "x \<in> Units G" "y \<in> Units G"
1.21 +  shows "y \<otimes> x = \<one>"
1.22 +proof -
1.23 +  from G have "x \<otimes> y \<otimes> x = x \<otimes> \<one>" by (auto simp add: inv Units_closed)
1.24 +  with G show ?thesis by (simp del: r_one add: m_assoc Units_closed)
1.25 +qed
1.26 +
1.27  text {* Power *}
1.28
1.29  lemma (in monoid) nat_pow_closed [intro, simp]:
1.30 @@ -287,16 +300,7 @@
1.31    "[| x \<in> carrier G; y \<in> carrier G; z \<in> carrier G |] ==>
1.32     (x \<otimes> y = x \<otimes> z) = (y = z)"
1.33    using Units_l_inv by simp
1.34 -(*
1.35 -lemma (in group) r_one [simp]:
1.36 -  "x \<in> carrier G ==> x \<otimes> \<one> = x"
1.37 -proof -
1.38 -  assume x: "x \<in> carrier G"
1.39 -  then have "inv x \<otimes> (x \<otimes> \<one>) = inv x \<otimes> x"
1.40 -    by (simp add: m_assoc [symmetric] l_inv)
1.41 -  with x show ?thesis by simp
1.42 -qed
1.43 -*)
1.44 +
1.45  lemma (in group) r_inv:
1.46    "x \<in> carrier G ==> x \<otimes> inv x = \<one>"
1.47  proof -
1.48 @@ -346,6 +350,10 @@
1.49    with G show ?thesis by simp
1.50  qed
1.51
1.52 +lemma (in group) inv_comm:
1.53 +  "[| x \<otimes> y = \<one>; x \<in> carrier G; y \<in> carrier G |] ==> y \<otimes> x = \<one>"
1.54 +  by (rule Units_inv_comm) auto
1.55 +
1.56  text {* Power *}
1.57
1.58  lemma (in group) int_pow_def2:
```