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"
```