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.7 -subsection "fundamental lemmas"
1.9 -
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.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.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.131 -text "Lemmas about intersection and normal subgroups"
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.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.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.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.224  lemma (in group) subgroup_in_normalizer:
1.225 @@ -267,39 +55,38 @@
1.226  qed
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.274  subsection \<open>Second Isomorphism Theorem\<close>
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.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.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.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.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.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.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.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.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.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.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"