src/HOL/Algebra/Group.thy
 changeset 13944 9b34607cd83e parent 13943 83d842ccd4aa child 13949 0ce528cd6f19
```     1.1 --- a/src/HOL/Algebra/Group.thy	Thu May 01 10:29:44 2003 +0200
1.2 +++ b/src/HOL/Algebra/Group.thy	Thu May 01 11:54:18 2003 +0200
1.3 @@ -348,7 +348,7 @@
1.4    "[| x \<otimes> y = \<one>; x \<in> carrier G; y \<in> carrier G |] ==> y \<otimes> x = \<one>"
1.5    by (rule Units_inv_comm) auto
1.6
1.7 -lemma (in group) m_inv_equality:
1.8 +lemma (in group) inv_equality:
1.9       "[|y \<otimes> x = \<one>; x \<in> carrier G; y \<in> carrier G|] ==> inv x = y"
1.11  apply (rule the_equality)
1.12 @@ -567,6 +567,27 @@
1.13      (auto intro: G.m_assoc H.m_assoc G.l_inv H.l_inv
1.15
1.16 +lemma carrier_DirProdGroup [simp]:
1.17 +     "carrier (G \<times>\<^sub>g H) = carrier G \<times> carrier H"
1.18 +  by (simp add: DirProdGroup_def DirProdSemigroup_def)
1.19 +
1.20 +lemma one_DirProdGroup [simp]:
1.21 +     "one (G \<times>\<^sub>g H) = (one G, one H)"
1.22 +  by (simp add: DirProdGroup_def DirProdSemigroup_def);
1.23 +
1.24 +lemma mult_DirProdGroup [simp]:
1.25 +     "mult (G \<times>\<^sub>g H) (g, h) (g', h') = (mult G g g', mult H h h')"
1.26 +  by (simp add: DirProdGroup_def DirProdSemigroup_def)
1.27 +
1.28 +lemma inv_DirProdGroup [simp]:
1.29 +  includes group G + group H
1.30 +  assumes g: "g \<in> carrier G"
1.31 +      and h: "h \<in> carrier H"
1.32 +  shows "m_inv (G \<times>\<^sub>g H) (g, h) = (m_inv G g, m_inv H h)"
1.33 +  apply (rule group.inv_equality [OF DirProdGroup_group])
1.34 +  apply (simp_all add: prems group_def group.l_inv)
1.35 +  done
1.36 +
1.37  subsection {* Homomorphisms *}
1.38
1.39  constdefs
```