src/HOL/Algebra/Zassenhaus.thy
changeset 68445 c183a6a69f2d
parent 68443 43055b016688
child 68452 c027dfbfad30
     1.1 --- a/src/HOL/Algebra/Zassenhaus.thy	Tue Jun 12 16:09:12 2018 +0100
     1.2 +++ b/src/HOL/Algebra/Zassenhaus.thy	Thu Jun 14 14:23:38 2018 +0100
     1.3 @@ -2,220 +2,8 @@
     1.4    imports Coset Group_Action
     1.5  begin
     1.6  
     1.7 -subsection "fundamental lemmas"
     1.8  
     1.9 -
    1.10 -text "Lemmas about subgroups"
    1.11 -
    1.12 -
    1.13 -(*A subgroup included in another subgroup is a subgroup of the subgroup*)
    1.14 -lemma (in group) subgroup_incl :
    1.15 -  assumes "subgroup I G"
    1.16 -    and "subgroup J G"
    1.17 -    and "I\<subseteq>J"
    1.18 -  shows "subgroup I (G\<lparr>carrier:=J\<rparr>)"using assms subgroup_inv_equality
    1.19 -  by (auto simp add: subgroup_def)
    1.20 -
    1.21 -(*A subgroup of a subgroup is a subgroup of the group*)
    1.22 -lemma (in group) incl_subgroup :
    1.23 -  assumes "subgroup J G"
    1.24 -    and "subgroup I (G\<lparr>carrier:=J\<rparr>)"
    1.25 -  shows "subgroup I G" unfolding subgroup_def
    1.26 -proof
    1.27 -  have H1: "I \<subseteq> carrier (G\<lparr>carrier:=J\<rparr>)" using assms(2) subgroup_imp_subset by blast
    1.28 -  also have H2: "...\<subseteq>J" by simp
    1.29 -  also  have "...\<subseteq>(carrier G)"  by (simp add: assms(1) subgroup_imp_subset)
    1.30 -  finally have H: "I \<subseteq> carrier G" by simp
    1.31 -  have "(\<And>x y. \<lbrakk>x \<in> I ; y \<in> I\<rbrakk> \<Longrightarrow> x \<otimes> y \<in> I)" using assms(2) by (auto simp add: subgroup_def)
    1.32 -  thus  "I \<subseteq> carrier G \<and> (\<forall>x y. x \<in> I \<longrightarrow> y \<in> I \<longrightarrow> x \<otimes> y \<in> I)"  using H by blast
    1.33 -  have K: "\<one> \<in> I" using assms(2) by (auto simp add: subgroup_def)
    1.34 -  have "(\<And>x. x \<in> I \<Longrightarrow> inv x \<in> I)" using assms  subgroup.m_inv_closed H
    1.35 -    by (metis H1 H2  subgroup_inv_equality subsetCE)
    1.36 -  thus "\<one> \<in> I \<and> (\<forall>x. x \<in> I \<longrightarrow> inv x \<in> I)" using K by blast
    1.37 -qed
    1.38 -
    1.39 -
    1.40 -text "Lemmas about set_mult"
    1.41 -
    1.42 -
    1.43 -lemma (in group) set_mult_same_law :
    1.44 -  assumes "subgroup H G"
    1.45 -and "K1 \<subseteq> H"
    1.46 -and "K2 \<subseteq> H"
    1.47 -shows "K1<#>\<^bsub>(G\<lparr>carrier:=H\<rparr>)\<^esub>K2 = K1<#>K2"
    1.48 -proof 
    1.49 -  show "K1 <#>\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> K2 \<subseteq> K1 <#> K2"
    1.50 -  proof
    1.51 -    fix h assume Hyph : "h\<in>K1<#>\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub>K2"
    1.52 -    then obtain k1 k2 where Hyp : "k1\<in>K1 \<and> k2\<in>K2 \<and> k1\<otimes>\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub>k2 = h"
    1.53 -      unfolding set_mult_def by blast
    1.54 -    hence "k1\<in>H" using assms by blast
    1.55 -    moreover have  "k2\<in>H" using Hyp assms by blast
    1.56 -    ultimately have EGAL : "k1 \<otimes>\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> k2 = k1 \<otimes>\<^bsub>G\<^esub> k2" by simp
    1.57 -    have "k1 \<otimes>\<^bsub>G\<^esub> k2 \<in> K1<#>K2" unfolding  set_mult_def using Hyp by blast
    1.58 -    hence "k1 \<otimes>\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> k2 \<in> K1<#>K2" using EGAL by auto
    1.59 -    thus "h \<in> K1<#>K2 " using Hyp by blast
    1.60 -  qed
    1.61 -  show "K1 <#> K2 \<subseteq> K1 <#>\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> K2"
    1.62 -  proof
    1.63 -    fix h assume Hyph : "h\<in>K1<#>K2"
    1.64 -    then obtain k1 k2 where Hyp : "k1\<in>K1 \<and> k2\<in>K2 \<and> k1\<otimes>k2 = h" unfolding set_mult_def by blast
    1.65 -    hence k1H: "k1\<in>H" using assms by blast
    1.66 -    have  k2H: "k2\<in>H" using Hyp assms by blast
    1.67 -    have EGAL : "k1 \<otimes>\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> k2 = k1 \<otimes>\<^bsub>G\<^esub> k2" using k1H k2H by simp
    1.68 -    have "k1 \<otimes>\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> k2 \<in> K1<#>\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub>K2" unfolding  set_mult_def using Hyp by blast
    1.69 -    hence "k1 \<otimes> k2 \<in> K1<#>\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub>K2" using EGAL by auto
    1.70 -    thus "h \<in> K1<#>\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub>K2 " using Hyp by blast
    1.71 -  qed
    1.72 -qed
    1.73 -
    1.74 -
    1.75 -(*A group multiplied by a subgroup stays the same*)
    1.76 -lemma (in group) set_mult_carrier_idem :
    1.77 -  assumes "subgroup H G"
    1.78 -  shows "(carrier G)<#>H = carrier G"
    1.79 -proof
    1.80 -  show "(carrier G)<#>H \<subseteq> carrier G" unfolding set_mult_def using subgroup_imp_subset assms by blast
    1.81 -next
    1.82 -  have " (carrier G) #>  \<one> = carrier G" unfolding set_mult_def r_coset_def group_axioms by simp
    1.83 -  moreover have "(carrier G) #>  \<one> \<subseteq> (carrier G) <#> H" unfolding set_mult_def r_coset_def
    1.84 -    using assms subgroup.one_closed[OF assms] by blast
    1.85 -  ultimately show "carrier G \<subseteq> (carrier G) <#> H" by simp
    1.86 -qed
    1.87 -
    1.88 -(*Same lemma as above, but everything is included in a subgroup*)
    1.89 -lemma (in group) set_mult_subgroup_idem :
    1.90 -  assumes "subgroup H G"
    1.91 -    and "subgroup N (G\<lparr>carrier:=H\<rparr>)"
    1.92 -  shows "H<#>N = H"
    1.93 -  using group.set_mult_carrier_idem[OF subgroup_imp_group] subgroup_imp_subset assms
    1.94 -  by (metis monoid.cases_scheme order_refl partial_object.simps(1)
    1.95 -      partial_object.update_convs(1) set_mult_same_law)
    1.96 -
    1.97 -(*A normal subgroup is commutative with set_mult*)
    1.98 -lemma (in group) commut_normal :
    1.99 -  assumes "subgroup H G"
   1.100 -    and "N\<lhd>G"
   1.101 -  shows "H<#>N = N<#>H" 
   1.102 -proof-
   1.103 -  have aux1 : "{H <#> N} = {\<Union>h\<in>H. h <# N }" unfolding set_mult_def l_coset_def by auto
   1.104 -  also have "... = {\<Union>h\<in>H. N #> h }" using assms normal.coset_eq subgroup.mem_carrier by fastforce
   1.105 -  moreover have aux2 : "{N <#> H} = {\<Union>h\<in>H. N #> h }"unfolding set_mult_def r_coset_def by auto
   1.106 -  ultimately show "H<#>N = N<#>H" by simp
   1.107 -qed
   1.108 -
   1.109 -(*Same lemma as above, but everything is included in a subgroup*)
   1.110 -lemma (in group) commut_normal_subgroup :
   1.111 -  assumes "subgroup H G"
   1.112 -    and "N\<lhd>(G\<lparr>carrier:=H\<rparr>)"
   1.113 -    and "subgroup K (G\<lparr>carrier:=H\<rparr>)"
   1.114 -  shows "K<#>N = N<#>K"
   1.115 -proof-
   1.116 -  have "N \<subseteq> carrier (G\<lparr>carrier := H\<rparr>)" using assms normal_imp_subgroup subgroup_imp_subset by blast
   1.117 -  hence NH : "N \<subseteq> H" by simp
   1.118 -  have "K \<subseteq> carrier(G\<lparr>carrier := H\<rparr>)" using subgroup_imp_subset assms by blast
   1.119 -  hence KH : "K \<subseteq> H" by simp
   1.120 -  have Egal : "K <#>\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> N = N <#>\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> K"
   1.121 -  using group.commut_normal[where ?G = "G\<lparr>carrier :=H\<rparr>", of K N,OF subgroup_imp_group[OF assms(1)]
   1.122 -               assms(3) assms(2)] by auto
   1.123 -  also have "... = N <#> K" using set_mult_same_law[of H N K, OF assms(1) NH KH] by auto
   1.124 -  moreover have "K <#>\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> N = K <#> N"
   1.125 -    using set_mult_same_law[of H K N, OF assms(1) KH NH] by auto
   1.126 -  ultimately show "K<#>N = N<#>K" by auto
   1.127 -qed
   1.128 -
   1.129 -
   1.130 -
   1.131 -text "Lemmas about intersection and normal subgroups"
   1.132 -
   1.133 -
   1.134 -
   1.135 -lemma (in group) normal_inter:
   1.136 -  assumes "subgroup H G"
   1.137 -    and "subgroup K G"
   1.138 -    and "H1\<lhd>G\<lparr>carrier := H\<rparr>"
   1.139 -  shows " (H1\<inter>K)\<lhd>(G\<lparr>carrier:= (H\<inter>K)\<rparr>)" 
   1.140 -proof-
   1.141 -  define HK and H1K and GH and GHK
   1.142 -    where "HK = H\<inter>K" and "H1K=H1\<inter>K" and "GH =G\<lparr>carrier := H\<rparr>" and "GHK = (G\<lparr>carrier:= (H\<inter>K)\<rparr>)"
   1.143 -  show "H1K\<lhd>GHK"
   1.144 -  proof (intro group.normal_invI[of GHK H1K])
   1.145 -    show "Group.group GHK"
   1.146 -      using GHK_def subgroups_Inter_pair subgroup_imp_group assms by blast
   1.147 -
   1.148 -  next
   1.149 -    have  H1K_incl:"subgroup H1K (G\<lparr>carrier:= (H\<inter>K)\<rparr>)"
   1.150 -    proof(intro subgroup_incl)
   1.151 -          show "subgroup H1K G"
   1.152 -            using assms normal_imp_subgroup subgroups_Inter_pair incl_subgroup H1K_def by blast
   1.153 -        next
   1.154 -          show "subgroup (H\<inter>K) G" using HK_def subgroups_Inter_pair assms by auto
   1.155 -        next
   1.156 -          have "H1 \<subseteq> (carrier (G\<lparr>carrier:=H\<rparr>))" 
   1.157 -            using  assms(3) normal_imp_subgroup subgroup_imp_subset by blast
   1.158 -          also have "... \<subseteq> H" by simp
   1.159 -          thus "H1K \<subseteq>H\<inter>K" 
   1.160 -            using H1K_def calculation by auto
   1.161 -        qed
   1.162 -        thus "subgroup H1K GHK" using GHK_def by simp
   1.163 -
   1.164 -  next
   1.165 -    show "\<And> x h. x\<in>carrier GHK \<Longrightarrow> h\<in>H1K \<Longrightarrow> x \<otimes>\<^bsub>GHK\<^esub> h \<otimes>\<^bsub>GHK\<^esub> inv\<^bsub>GHK\<^esub> x\<in> H1K"
   1.166 -        proof-
   1.167 -          have invHK: "\<lbrakk>y\<in>HK\<rbrakk> \<Longrightarrow> inv\<^bsub>GHK\<^esub> y = inv\<^bsub>GH\<^esub> y"
   1.168 -            using subgroup_inv_equality assms HK_def GH_def GHK_def subgroups_Inter_pair by simp
   1.169 -          have multHK : "\<lbrakk>x\<in>HK;y\<in>HK\<rbrakk> \<Longrightarrow>  x \<otimes>\<^bsub>(G\<lparr>carrier:=HK\<rparr>)\<^esub> y =  x \<otimes> y"
   1.170 -            using HK_def by simp
   1.171 -          fix x assume p: "x\<in>carrier GHK"
   1.172 -            fix h assume p2 : "h:H1K"
   1.173 -            have "carrier(GHK)\<subseteq>HK"
   1.174 -              using GHK_def HK_def by simp
   1.175 -            hence xHK:"x\<in>HK" using p by auto
   1.176 -            hence invx:"inv\<^bsub>GHK\<^esub> x = inv\<^bsub>GH\<^esub> x"
   1.177 -              using invHK assms GHK_def HK_def GH_def subgroup_inv_equality subgroups_Inter_pair by simp
   1.178 -            have "H1\<subseteq>carrier(GH)"
   1.179 -              using assms GH_def normal_imp_subgroup subgroup_imp_subset by blast
   1.180 -            hence hHK:"h\<in>HK" 
   1.181 -              using p2 H1K_def HK_def GH_def by auto
   1.182 -            hence xhx_egal : "x \<otimes>\<^bsub>GHK\<^esub> h \<otimes>\<^bsub>GHK\<^esub> inv\<^bsub>GHK\<^esub>x =  x \<otimes>\<^bsub>GH\<^esub> h \<otimes>\<^bsub>GH\<^esub> inv\<^bsub>GH\<^esub> x"
   1.183 -              using invx invHK multHK GHK_def GH_def by auto
   1.184 -            have xH:"x\<in>carrier(GH)" 
   1.185 -              using xHK HK_def GH_def by auto 
   1.186 -            have hH:"h\<in>carrier(GH)"
   1.187 -              using hHK HK_def GH_def by auto 
   1.188 -            have  "(\<forall>x\<in>carrier (GH). \<forall>h\<in>H1.  x \<otimes>\<^bsub>GH\<^esub> h \<otimes>\<^bsub>GH\<^esub> inv\<^bsub>GH\<^esub> x \<in> H1)"
   1.189 -              using assms normal_invE GH_def normal.inv_op_closed2 by fastforce
   1.190 -            hence INCL_1 : "x \<otimes>\<^bsub>GH\<^esub> h \<otimes>\<^bsub>GH\<^esub> inv\<^bsub>GH\<^esub> x \<in> H1"
   1.191 -              using  xH H1K_def p2 by blast
   1.192 -            have " x \<otimes>\<^bsub>GH\<^esub> h \<otimes>\<^bsub>GH\<^esub> inv\<^bsub>GH\<^esub> x \<in> HK"
   1.193 -              using assms HK_def subgroups_Inter_pair hHK xHK
   1.194 -              by (metis GH_def inf.cobounded1 subgroup_def subgroup_incl)
   1.195 -            hence " x \<otimes>\<^bsub>GH\<^esub> h \<otimes>\<^bsub>GH\<^esub> inv\<^bsub>GH\<^esub> x \<in> K" using HK_def by simp
   1.196 -            hence " x \<otimes>\<^bsub>GH\<^esub> h \<otimes>\<^bsub>GH\<^esub> inv\<^bsub>GH\<^esub> x \<in> H1K" using INCL_1 H1K_def by auto
   1.197 -            thus  "x \<otimes>\<^bsub>GHK\<^esub> h \<otimes>\<^bsub>GHK\<^esub> inv\<^bsub>GHK\<^esub> x \<in> H1K" using xhx_egal by simp
   1.198 -          qed
   1.199 -    qed
   1.200 -qed
   1.201 -
   1.202 -
   1.203 -lemma (in group) normal_inter_subgroup :
   1.204 -  assumes "subgroup H G"
   1.205 -    and "N \<lhd> G"
   1.206 -  shows "(N\<inter>H) \<lhd> (G\<lparr>carrier := H\<rparr>)"
   1.207 -proof -
   1.208 -  define K where "K = carrier G"
   1.209 -  have "G\<lparr>carrier := K\<rparr> =  G" using K_def by auto
   1.210 -  moreover have "subgroup K G" using K_def subgroup_self by blast
   1.211 -  moreover have "normal N (G \<lparr>carrier :=K\<rparr>)" using assms K_def by simp
   1.212 -  ultimately have "N \<inter> H \<lhd> G\<lparr>carrier := K \<inter> H\<rparr>"
   1.213 -    using normal_inter[of K H N] assms(1) by blast
   1.214 -  moreover have "K \<inter> H = H" using K_def assms subgroup_imp_subset by blast
   1.215 -  ultimately show "normal (N\<inter>H) (G\<lparr>carrier := H\<rparr>)" by auto
   1.216 -qed
   1.217 -
   1.218 -
   1.219 -
   1.220 -text \<open>Lemmas about normalizer\<close>
   1.221 +subsubsection \<open>Lemmas about normalizer\<close>
   1.222  
   1.223  
   1.224  lemma (in group) subgroup_in_normalizer: 
   1.225 @@ -267,39 +55,38 @@
   1.226  qed
   1.227  
   1.228  
   1.229 -lemma (in group) normal_imp_subgroup_normalizer :
   1.230 +lemma (in group) normal_imp_subgroup_normalizer:
   1.231    assumes "subgroup H G"
   1.232 -and "N \<lhd> (G\<lparr>carrier := H\<rparr>)"
   1.233 -shows "subgroup H (G\<lparr>carrier := normalizer G N\<rparr>)" 
   1.234 +    and "N \<lhd> (G\<lparr>carrier := H\<rparr>)"
   1.235 +  shows "subgroup H (G\<lparr>carrier := normalizer G N\<rparr>)" 
   1.236  proof-
   1.237    have N_carrierG : "N \<subseteq> carrier(G)"
   1.238      using assms normal_imp_subgroup subgroup_imp_subset
   1.239      by (smt monoid.cases_scheme order_trans partial_object.simps(1) partial_object.update_convs(1))
   1.240    {have "H \<subseteq> normalizer G N" unfolding normalizer_def stabilizer_def
   1.241      proof
   1.242 -    fix x assume xH : "x \<in> H"
   1.243 -    hence xcarrierG : "x \<in> carrier(G)" using assms subgroup_imp_subset  by auto
   1.244 -    have "   N #> x = x <# N" using assms xH
   1.245 -      unfolding r_coset_def l_coset_def normal_def normal_axioms_def subgroup_imp_group by auto
   1.246 -    hence "x <# N #> inv x =(N #> x) #> inv x"
   1.247 -      by simp
   1.248 -    also have "... = N #> \<one>"
   1.249 -      using  assms r_inv xcarrierG coset_mult_assoc[OF N_carrierG] by simp  
   1.250 -    finally have "x <# N #> inv x = N" by (simp add: N_carrierG)
   1.251 -    thus "x \<in> {g \<in> carrier G. (\<lambda>H\<in>{H. H \<subseteq> carrier G}. g <# H #> inv g) N = N}"
   1.252 -      using xcarrierG by (simp add : N_carrierG)
   1.253 -  qed}
   1.254 +      fix x assume xH : "x \<in> H"
   1.255 +      hence xcarrierG : "x \<in> carrier(G)" using assms subgroup_imp_subset  by auto
   1.256 +      have "   N #> x = x <# N" using assms xH
   1.257 +        unfolding r_coset_def l_coset_def normal_def normal_axioms_def subgroup_imp_group by auto
   1.258 +      hence "x <# N #> inv x =(N #> x) #> inv x"
   1.259 +        by simp
   1.260 +      also have "... = N #> \<one>"
   1.261 +        using  assms r_inv xcarrierG coset_mult_assoc[OF N_carrierG] by simp  
   1.262 +      finally have "x <# N #> inv x = N" by (simp add: N_carrierG)
   1.263 +      thus "x \<in> {g \<in> carrier G. (\<lambda>H\<in>{H. H \<subseteq> carrier G}. g <# H #> inv g) N = N}"
   1.264 +        using xcarrierG by (simp add : N_carrierG)
   1.265 +    qed}
   1.266    thus "subgroup H (G\<lparr>carrier := normalizer G N\<rparr>)"
   1.267      using subgroup_incl[OF assms(1) normalizer_imp_subgroup]
   1.268 -         assms normal_imp_subgroup subgroup_imp_subset
   1.269 +      assms normal_imp_subgroup subgroup_imp_subset
   1.270      by (metis  group.incl_subgroup is_group)
   1.271  qed
   1.272  
   1.273  
   1.274  subsection \<open>Second Isomorphism Theorem\<close>
   1.275  
   1.276 -
   1.277 -lemma (in group) mult_norm_subgroup :
   1.278 +lemma (in group) mult_norm_subgroup:
   1.279    assumes "normal N G"
   1.280      and "subgroup H G"
   1.281    shows "subgroup (N<#>H) G" unfolding subgroup_def
   1.282 @@ -364,7 +151,7 @@
   1.283  qed
   1.284      
   1.285  
   1.286 -lemma (in group) mult_norm_sub_in_sub :
   1.287 +lemma (in group) mult_norm_sub_in_sub:
   1.288    assumes "normal N (G\<lparr>carrier:=K\<rparr>)"
   1.289    assumes "subgroup H (G\<lparr>carrier:=K\<rparr>)"
   1.290    assumes "subgroup K G"
   1.291 @@ -379,12 +166,12 @@
   1.292    also have "... \<subseteq> K" by simp
   1.293    finally have Incl2:"N \<subseteq> K" by simp
   1.294    have "(N <#>\<^bsub>G\<lparr>carrier := K\<rparr>\<^esub> H) = (N <#> H)"
   1.295 -    using set_mult_same_law[of K] assms Incl1 Incl2 by simp
   1.296 +    using subgroup_set_mult_equality[of K] assms Incl1 Incl2 by simp
   1.297    thus "subgroup (N<#>H) (G\<lparr>carrier:=K\<rparr>)" using Hyp by auto
   1.298  qed
   1.299  
   1.300  
   1.301 -lemma (in group) subgroup_of_normal_set_mult :
   1.302 +lemma (in group) subgroup_of_normal_set_mult:
   1.303    assumes "normal N G"
   1.304  and "subgroup H G"
   1.305  shows "subgroup H (G\<lparr>carrier := N <#> H\<rparr>)"
   1.306 @@ -398,7 +185,7 @@
   1.307  qed
   1.308  
   1.309  
   1.310 -lemma (in group) normal_in_normal_set_mult :
   1.311 +lemma (in group) normal_in_normal_set_mult:
   1.312    assumes "normal N G"
   1.313  and "subgroup H G"
   1.314  shows "normal N (G\<lparr>carrier := N <#> H\<rparr>)"
   1.315 @@ -413,7 +200,7 @@
   1.316  qed
   1.317  
   1.318  
   1.319 -proposition (in group) weak_snd_iso_thme :
   1.320 +proposition (in group) weak_snd_iso_thme:
   1.321    assumes "subgroup  H G" 
   1.322      and "N\<lhd>G"
   1.323    shows "(G\<lparr>carrier := N<#>H\<rparr> Mod N \<cong> G\<lparr>carrier:=H\<rparr> Mod (N\<inter>H))"
   1.324 @@ -518,7 +305,7 @@
   1.325  qed
   1.326  
   1.327  
   1.328 -theorem (in group) snd_iso_thme :
   1.329 +theorem (in group) snd_iso_thme:
   1.330    assumes "subgroup H G"
   1.331      and "subgroup N G"
   1.332      and "subgroup H (G\<lparr>carrier:= (normalizer G N)\<rparr>)"
   1.333 @@ -539,7 +326,7 @@
   1.334           G\<lparr>carrier := normalizer G N, carrier := H\<rparr> Mod N \<inter> H =
   1.335            (G\<lparr>carrier:= N<#>H\<rparr> Mod N)  \<cong>
   1.336           G\<lparr>carrier := normalizer G N, carrier := H\<rparr> Mod N \<inter> H" 
   1.337 -    using set_mult_same_law[OF  normalizer_imp_subgroup[OF subgroup_imp_subset[OF assms(2)]], of N H] 
   1.338 +    using subgroup_set_mult_equality[OF  normalizer_imp_subgroup[OF subgroup_imp_subset[OF assms(2)]], of N H] 
   1.339            subgroup_imp_subset[OF assms(3)]
   1.340            subgroup_imp_subset[OF normal_imp_subgroup[OF subgroup_in_normalizer[OF assms(2)]]]
   1.341      by simp
   1.342 @@ -570,7 +357,7 @@
   1.343  subsection\<open>The Zassenhaus Lemma\<close>
   1.344  
   1.345  
   1.346 -lemma (in group) distinc :
   1.347 +lemma (in group) distinc:
   1.348    assumes "subgroup  H G" 
   1.349      and "H1\<lhd>G\<lparr>carrier := H\<rparr>" 
   1.350      and  "subgroup K G" 
   1.351 @@ -623,7 +410,7 @@
   1.352    qed
   1.353  qed
   1.354  
   1.355 -lemma (in group) preliminary1 :
   1.356 +lemma (in group) preliminary1:
   1.357    assumes "subgroup  H G" 
   1.358      and "H1\<lhd>G\<lparr>carrier := H\<rparr>" 
   1.359      and  "subgroup K G" 
   1.360 @@ -664,7 +451,7 @@
   1.361    qed
   1.362  qed
   1.363  
   1.364 -lemma (in group) preliminary2 :
   1.365 +lemma (in group) preliminary2:
   1.366    assumes "subgroup  H G" 
   1.367      and "H1\<lhd>G\<lparr>carrier := H\<rparr>"
   1.368      and  "subgroup K G" 
   1.369 @@ -700,7 +487,7 @@
   1.370      hence allG : "h1 \<in> carrier G" "hk \<in> carrier G" "x \<in> carrier G"
   1.371        using assms subgroup_imp_subset h1hk_def normal_imp_subgroup incl_subgroup apply blast+.
   1.372      hence "x <#\<^bsub>G\<lparr>carrier := H1 <#> H\<inter>K\<rparr>\<^esub> (H1 <#> H\<inter>K1) =h1 \<otimes> hk <# (H1 <#> H\<inter>K1)"
   1.373 -      using set_mult_same_law subgroup_imp_subset xH h1hk_def by (simp add: l_coset_def)
   1.374 +      using subgroup_set_mult_equality subgroup_imp_subset xH h1hk_def by (simp add: l_coset_def)
   1.375      also have "... = h1 <# (hk <# (H1 <#> H\<inter>K1))"
   1.376        using lcos_m_assoc[OF subgroup_imp_subset[OF incl_subgroup[OF assms(1) subH1]]allG(1)allG(2)]
   1.377        by (metis allG(1) allG(2) assms(1) incl_subgroup lcos_m_assoc subH2 subgroup_imp_subset)
   1.378 @@ -742,7 +529,7 @@
   1.379      finally have eq1 : "x <#\<^bsub>G\<lparr>carrier := H1 <#> H \<inter> K\<rparr>\<^esub> (H1 <#> H \<inter> K1) = H1 <#> (H \<inter> K1) #> hk"
   1.380        by (simp add: allG(2) all_inclG inf.coboundedI2 setmult_rcos_assoc)
   1.381      have "H1 <#> H \<inter> K1 #>\<^bsub>G\<lparr>carrier := H1 <#> H \<inter> K\<rparr>\<^esub> x = H1 <#> H \<inter> K1 #> (h1 \<otimes> hk)"
   1.382 -      using set_mult_same_law subgroup_imp_subset xH h1hk_def by (simp add: r_coset_def)
   1.383 +      using subgroup_set_mult_equality subgroup_imp_subset xH h1hk_def by (simp add: r_coset_def)
   1.384      also have "... = H1 <#> H \<inter> K1 #> h1 #> hk"
   1.385        using coset_mult_assoc by (simp add: allG all_inclG inf.coboundedI2 setmult_subset_G)
   1.386      also have"... =  H \<inter> K1 <#> H1 #> h1 #> hk"
   1.387 @@ -762,7 +549,7 @@
   1.388  qed
   1.389  
   1.390  
   1.391 -proposition (in group)  Zassenhaus_1 :
   1.392 +proposition (in group)  Zassenhaus_1:
   1.393    assumes "subgroup  H G" 
   1.394      and "H1\<lhd>G\<lparr>carrier := H\<rparr>" 
   1.395      and  "subgroup K G" 
   1.396 @@ -811,7 +598,7 @@
   1.397  qed
   1.398  
   1.399  
   1.400 -theorem (in group) Zassenhaus :
   1.401 +theorem (in group) Zassenhaus:
   1.402    assumes "subgroup  H G" 
   1.403      and "H1\<lhd>G\<lparr>carrier := H\<rparr>" 
   1.404      and  "subgroup K G"