src/HOL/Algebra/Zassenhaus.thy
changeset 68555 22d51874f37d
parent 68466 3d8241f4198b
child 68604 57721285d4ef
     1.1 --- a/src/HOL/Algebra/Zassenhaus.thy	Sat Jun 30 18:58:13 2018 +0100
     1.2 +++ b/src/HOL/Algebra/Zassenhaus.thy	Sun Jul 01 16:13:25 2018 +0100
     1.3 @@ -43,7 +43,7 @@
     1.4      ultimately have "x \<otimes>\<^bsub>G\<lparr>carrier := normalizer G H\<rparr>\<^esub> h = x \<otimes> h" by simp
     1.5      moreover have " inv\<^bsub>G\<lparr>carrier := normalizer G H\<rparr>\<^esub> x =  inv x"
     1.6        using xnormalizer
     1.7 -      by (simp add: assms normalizer_imp_subgroup subgroup.subset subgroup_inv_equality)
     1.8 +      by (simp add: assms normalizer_imp_subgroup subgroup.subset m_inv_consistent)
     1.9      ultimately  have xhxegal: "x \<otimes>\<^bsub>G\<lparr>carrier := normalizer G H\<rparr>\<^esub> h
    1.10                  \<otimes>\<^bsub>G\<lparr>carrier := normalizer G H\<rparr>\<^esub> inv\<^bsub>G\<lparr>carrier := normalizer G H\<rparr>\<^esub> x
    1.11                    = x \<otimes>h \<otimes> inv x"
    1.12 @@ -172,7 +172,7 @@
    1.13    also have "... \<subseteq> K" by simp
    1.14    finally have Incl2:"N \<subseteq> K" by simp
    1.15    have "(N <#>\<^bsub>G\<lparr>carrier := K\<rparr>\<^esub> H) = (N <#> H)"
    1.16 -    using subgroup_set_mult_equality[of K] assms Incl1 Incl2 by simp
    1.17 +    using set_mult_consistent by simp
    1.18    thus "subgroup (N<#>H) (G\<lparr>carrier:=K\<rparr>)" using Hyp by auto
    1.19  qed
    1.20  
    1.21 @@ -332,8 +332,7 @@
    1.22           G\<lparr>carrier := normalizer G N, carrier := H\<rparr> Mod N \<inter> H =
    1.23            (G\<lparr>carrier:= N<#>H\<rparr> Mod N)  \<cong>
    1.24           G\<lparr>carrier := normalizer G N, carrier := H\<rparr> Mod N \<inter> H"
    1.25 -    using subgroup_set_mult_equality[OF  normalizer_imp_subgroup[OF subgroup.subset[OF assms(2)]], of N H]
    1.26 -          subgroup.subset[OF assms(3)]
    1.27 +    using subgroup.subset[OF assms(3)]
    1.28            subgroup.subset[OF normal_imp_subgroup[OF subgroup_in_normalizer[OF assms(2)]]]
    1.29      by simp
    1.30    ultimately have "G\<lparr>carrier := normalizer G N,
    1.31 @@ -493,7 +492,7 @@
    1.32      hence allG : "h1 \<in> carrier G" "hk \<in> carrier G" "x \<in> carrier G"
    1.33        using assms subgroup.subset h1hk_def normal_imp_subgroup incl_subgroup apply blast+.
    1.34      hence "x <#\<^bsub>G\<lparr>carrier := H1 <#> H\<inter>K\<rparr>\<^esub> (H1 <#> H\<inter>K1) =h1 \<otimes> hk <# (H1 <#> H\<inter>K1)"
    1.35 -      using subgroup_set_mult_equality subgroup.subset xH h1hk_def by (simp add: l_coset_def)
    1.36 +      using subgroup.subset xH h1hk_def by (simp add: l_coset_def)
    1.37      also have "... = h1 <# (hk <# (H1 <#> H\<inter>K1))"
    1.38        using lcos_m_assoc[OF subgroup.subset[OF incl_subgroup[OF assms(1) subH1]]allG(1)allG(2)]
    1.39        by (metis allG(1) allG(2) assms(1) incl_subgroup lcos_m_assoc subH2 subgroup.subset)
    1.40 @@ -535,7 +534,7 @@
    1.41      finally have eq1 : "x <#\<^bsub>G\<lparr>carrier := H1 <#> H \<inter> K\<rparr>\<^esub> (H1 <#> H \<inter> K1) = H1 <#> (H \<inter> K1) #> hk"
    1.42        by (simp add: allG(2) all_inclG inf.coboundedI2 setmult_rcos_assoc)
    1.43      have "H1 <#> H \<inter> K1 #>\<^bsub>G\<lparr>carrier := H1 <#> H \<inter> K\<rparr>\<^esub> x = H1 <#> H \<inter> K1 #> (h1 \<otimes> hk)"
    1.44 -      using subgroup_set_mult_equality subgroup.subset xH h1hk_def by (simp add: r_coset_def)
    1.45 +      using subgroup.subset xH h1hk_def by (simp add: r_coset_def)
    1.46      also have "... = H1 <#> H \<inter> K1 #> h1 #> hk"
    1.47        using coset_mult_assoc by (simp add: allG all_inclG inf.coboundedI2 setmult_subset_G)
    1.48      also have"... =  H \<inter> K1 <#> H1 #> h1 #> hk"