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: