src/HOL/Algebra/Group.thy
 changeset 27611 2c01c0bdb385 parent 26805 27941d7d9a11 child 27698 197f0517f0bd
```     1.1 --- a/src/HOL/Algebra/Group.thy	Tue Jul 15 16:02:10 2008 +0200
1.2 +++ b/src/HOL/Algebra/Group.thy	Tue Jul 15 16:50:09 2008 +0200
1.3 @@ -396,9 +396,13 @@
1.4    by (rule subgroup.subset)
1.5
1.6  lemma (in subgroup) subgroup_is_group [intro]:
1.7 -  includes group G
1.8 -  shows "group (G\<lparr>carrier := H\<rparr>)"
1.9 -  by (rule groupI) (auto intro: m_assoc l_inv mem_carrier)
1.10 +  assumes "group G"
1.11 +  shows "group (G\<lparr>carrier := H\<rparr>)"
1.12 +proof -
1.13 +  interpret group [G] by fact
1.14 +  show ?thesis
1.15 +    by (rule groupI) (auto intro: m_assoc l_inv mem_carrier)
1.16 +qed
1.17
1.18  text {*
1.19    Since @{term H} is nonempty, it contains some element @{term x}.  Since
1.20 @@ -453,9 +457,11 @@
1.21                  one = (\<one>\<^bsub>G\<^esub>, \<one>\<^bsub>H\<^esub>)\<rparr>"
1.22
1.23  lemma DirProd_monoid:
1.24 -  includes monoid G + monoid H
1.25 +  assumes "monoid G" and "monoid H"
1.26    shows "monoid (G \<times>\<times> H)"
1.27  proof -
1.28 +  interpret G: monoid [G] by fact
1.29 +  interpret H: monoid [H] by fact
1.30    from prems
1.31    show ?thesis by (unfold monoid_def DirProd_def, auto)
1.32  qed
1.33 @@ -463,11 +469,15 @@
1.34
1.35  text{*Does not use the previous result because it's easier just to use auto.*}
1.36  lemma DirProd_group:
1.37 -  includes group G + group H
1.38 +  assumes "group G" and "group H"
1.39    shows "group (G \<times>\<times> H)"
1.40 -  by (rule groupI)
1.41 +proof -
1.42 +  interpret G: group [G] by fact
1.43 +  interpret H: group [H] by fact
1.44 +  show ?thesis by (rule groupI)
1.45       (auto intro: G.m_assoc H.m_assoc G.l_inv H.l_inv
1.47 +qed
1.48
1.49  lemma carrier_DirProd [simp]:
1.50       "carrier (G \<times>\<times> H) = carrier G \<times> carrier H"
1.51 @@ -482,23 +492,29 @@
1.53
1.54  lemma inv_DirProd [simp]:
1.55 -  includes group G + group H
1.56 +  assumes "group G" and "group H"
1.57    assumes g: "g \<in> carrier G"
1.58        and h: "h \<in> carrier H"
1.59    shows "m_inv (G \<times>\<times> H) (g, h) = (inv\<^bsub>G\<^esub> g, inv\<^bsub>H\<^esub> h)"
1.60 -  apply (rule group.inv_equality [OF DirProd_group])
1.61 +proof -
1.62 +  interpret G: group [G] by fact
1.63 +  interpret H: group [H] by fact
1.64 +  show ?thesis apply (rule group.inv_equality [OF DirProd_group])
1.65    apply (simp_all add: prems group.l_inv)
1.66    done
1.67 +qed
1.68
1.69  text{*This alternative proof of the previous result demonstrates interpret.
1.70     It uses @{text Prod.inv_equality} (available after @{text interpret})
1.71     instead of @{text "group.inv_equality [OF DirProd_group]"}. *}
1.72  lemma
1.73 -  includes group G + group H
1.74 +  assumes "group G" and "group H"
1.75    assumes g: "g \<in> carrier G"
1.76        and h: "h \<in> carrier H"
1.77    shows "m_inv (G \<times>\<times> H) (g, h) = (inv\<^bsub>G\<^esub> g, inv\<^bsub>H\<^esub> h)"
1.78  proof -
1.79 +  interpret G: group [G] by fact
1.80 +  interpret H: group [H] by fact
1.81    interpret Prod: group ["G \<times>\<times> H"]
1.82      by (auto intro: DirProd_group group.intro group.axioms prems)
1.83    show ?thesis by (simp add: Prod.inv_equality g h)
```