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.46             simp add: DirProd_def)
    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.52    by (simp add: DirProd_def)
    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)