--- a/src/HOL/Algebra/Coset.thy Fri Jun 15 13:02:12 2018 +0200
+++ b/src/HOL/Algebra/Coset.thy Fri Jun 15 13:52:05 2018 +0100
@@ -303,7 +303,7 @@
shows "subgroup (H <#> K) G"
proof (rule subgroup.intro)
show "H <#> K \<subseteq> carrier G"
- by (simp add: setmult_subset_G assms subgroup_imp_subset)
+ by (simp add: setmult_subset_G assms subgroup.subset)
next
have "\<one> \<otimes> \<one> \<in> H <#> K"
unfolding set_mult_def using assms subgroup.one_closed by blast
@@ -821,7 +821,7 @@
apply (rule card_partition)
apply (simp add: rcosets_subset_PowG [THEN finite_subset])
apply (simp add: rcosets_part_G)
- apply (simp add: card_rcosets_equal subgroup_imp_subset)
+ apply (simp add: card_rcosets_equal subgroup.subset)
apply (simp add: rcos_disjoint)
done
@@ -843,11 +843,11 @@
hence finite_rcos: "finite (rcosets H)" by simp
hence "card (\<Union>(rcosets H)) = (\<Sum>R\<in>(rcosets H). card R)"
using card_Union_disjoint[of "rcosets H"] finite_H rcos_disjoint[OF assms(1)]
- rcosets_finite[where ?H = H] by (simp add: assms subgroup_imp_subset)
+ rcosets_finite[where ?H = H] by (simp add: assms subgroup.subset)
hence "order G = (\<Sum>R\<in>(rcosets H). card R)"
by (simp add: assms order_def rcosets_part_G)
hence "order G = (\<Sum>R\<in>(rcosets H). card H)"
- using card_rcosets_equal by (simp add: assms subgroup_imp_subset)
+ using card_rcosets_equal by (simp add: assms subgroup.subset)
hence "order G = (card H) * (card (rcosets H))" by simp
hence "order G \<noteq> 0" using finite_rcos finite_H assms ex_in_conv
rcosets_part_G subgroup.one_closed by fastforce
@@ -1094,13 +1094,13 @@
show "\<And>x h. x \<in> carrier (G\<times>\<times>K) \<Longrightarrow> h \<in> H\<times>N \<Longrightarrow> x \<otimes>\<^bsub>G\<times>\<times>K\<^esub> h \<otimes>\<^bsub>G\<times>\<times>K\<^esub> inv\<^bsub>G\<times>\<times>K\<^esub> x \<in> H\<times>N"
proof-
fix x h assume xGK : "x \<in> carrier (G \<times>\<times> K)" and hHN : " h \<in> H \<times> N"
- hence hGK : "h \<in> carrier (G \<times>\<times> K)" using subgroup_imp_subset[OF sub] by auto
+ hence hGK : "h \<in> carrier (G \<times>\<times> K)" using subgroup.subset[OF sub] by auto
from xGK obtain x1 x2 where x1x2 :"x1 \<in> carrier G" "x2 \<in> carrier K" "x = (x1,x2)"
unfolding DirProd_def by fastforce
from hHN obtain h1 h2 where h1h2 : "h1 \<in> H" "h2 \<in> N" "h = (h1,h2)"
unfolding DirProd_def by fastforce
hence h1h2GK : "h1 \<in> carrier G" "h2 \<in> carrier K"
- using normal_imp_subgroup subgroup_imp_subset assms apply blast+.
+ using normal_imp_subgroup subgroup.subset assms apply blast+.
have "inv\<^bsub>G \<times>\<times> K\<^esub> x = (inv\<^bsub>G\<^esub> x1,inv\<^bsub>K\<^esub> x2)"
using inv_DirProd[OF group_axioms assms(1) x1x2(1)x1x2(2)] x1x2 by auto
hence "x \<otimes>\<^bsub>G \<times>\<times> K\<^esub> h \<otimes>\<^bsub>G \<times>\<times> K\<^esub> inv\<^bsub>G \<times>\<times> K\<^esub> x = (x1 \<otimes> h1 \<otimes> inv x1,x2 \<otimes>\<^bsub>K\<^esub> h2 \<otimes>\<^bsub>K\<^esub> inv\<^bsub>K\<^esub> x2)"
@@ -1160,7 +1160,7 @@
shows "(carrier G) <#> H = carrier G"
proof
show "(carrier G)<#>H \<subseteq> carrier G"
- unfolding set_mult_def using subgroup_imp_subset assms by blast
+ unfolding set_mult_def using subgroup.subset assms by blast
next
have " (carrier G) #> \<one> = carrier G" unfolding set_mult_def r_coset_def group_axioms by simp
moreover have "(carrier G) #> \<one> \<subseteq> (carrier G) <#> H" unfolding set_mult_def r_coset_def
@@ -1173,7 +1173,7 @@
assumes "subgroup H G"
and "subgroup N (G\<lparr>carrier:=H\<rparr>)"
shows "H<#>N = H"
- using group.set_mult_carrier_idem[OF subgroup_imp_group] subgroup_imp_subset assms
+ using group.set_mult_carrier_idem[OF subgroup_imp_group] subgroup.subset assms
by (metis monoid.cases_scheme order_refl partial_object.simps(1)
partial_object.update_convs(1) subgroup_set_mult_equality)
@@ -1196,9 +1196,9 @@
and "subgroup K (G\<lparr>carrier:=H\<rparr>)"
shows "K<#>N = N<#>K"
proof-
- have "N \<subseteq> carrier (G\<lparr>carrier := H\<rparr>)" using assms normal_imp_subgroup subgroup_imp_subset by blast
+ have "N \<subseteq> carrier (G\<lparr>carrier := H\<rparr>)" using assms normal_imp_subgroup subgroup.subset by blast
hence NH : "N \<subseteq> H" by simp
- have "K \<subseteq> carrier(G\<lparr>carrier := H\<rparr>)" using subgroup_imp_subset assms by blast
+ have "K \<subseteq> carrier(G\<lparr>carrier := H\<rparr>)" using subgroup.subset assms by blast
hence KH : "K \<subseteq> H" by simp
have Egal : "K <#>\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> N = N <#>\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> K"
using group.commut_normal[where ?G = "G\<lparr>carrier :=H\<rparr>", of K N,OF subgroup_imp_group[OF assms(1)]
@@ -1235,7 +1235,7 @@
show "subgroup (H\<inter>K) G" using HK_def subgroups_Inter_pair assms by auto
next
have "H1 \<subseteq> (carrier (G\<lparr>carrier:=H\<rparr>))"
- using assms(3) normal_imp_subgroup subgroup_imp_subset by blast
+ using assms(3) normal_imp_subgroup subgroup.subset by blast
also have "... \<subseteq> H" by simp
thus "H1K \<subseteq>H\<inter>K"
using H1K_def calculation by auto
@@ -1256,7 +1256,7 @@
hence invx:"inv\<^bsub>GHK\<^esub> x = inv\<^bsub>GH\<^esub> x"
using invHK assms GHK_def HK_def GH_def subgroup_inv_equality subgroups_Inter_pair by simp
have "H1\<subseteq>carrier(GH)"
- using assms GH_def normal_imp_subgroup subgroup_imp_subset by blast
+ using assms GH_def normal_imp_subgroup subgroup.subset by blast
hence hHK:"h\<in>HK"
using p2 H1K_def HK_def GH_def by auto
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"
@@ -1291,7 +1291,7 @@
moreover have "normal N (G \<lparr>carrier :=K\<rparr>)" using assms K_def by simp
ultimately have "N \<inter> H \<lhd> G\<lparr>carrier := K \<inter> H\<rparr>"
using normal_inter[of K H N] assms(1) by blast
- moreover have "K \<inter> H = H" using K_def assms subgroup_imp_subset by blast
+ moreover have "K \<inter> H = H" using K_def assms subgroup.subset by blast
ultimately show "normal (N\<inter>H) (G\<lparr>carrier := H\<rparr>)" by auto
qed
--- a/src/HOL/Algebra/Group.thy Fri Jun 15 13:02:12 2018 +0200
+++ b/src/HOL/Algebra/Group.thy Fri Jun 15 13:52:05 2018 +0100
@@ -1274,9 +1274,9 @@
and "subgroup I (G\<lparr>carrier:=J\<rparr>)"
shows "subgroup I G" unfolding subgroup_def
proof
- have H1: "I \<subseteq> carrier (G\<lparr>carrier:=J\<rparr>)" using assms(2) subgroup_imp_subset by blast
+ have H1: "I \<subseteq> carrier (G\<lparr>carrier:=J\<rparr>)" using assms(2) subgroup.subset by blast
also have H2: "...\<subseteq>J" by simp
- also have "...\<subseteq>(carrier G)" by (simp add: assms(1) subgroup_imp_subset)
+ also have "...\<subseteq>(carrier G)" by (simp add: assms(1) subgroup.subset)
finally have H: "I \<subseteq> carrier G" by simp
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)
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
--- a/src/HOL/Algebra/Zassenhaus.thy Fri Jun 15 13:02:12 2018 +0200
+++ b/src/HOL/Algebra/Zassenhaus.thy Fri Jun 15 13:52:05 2018 +0100
@@ -11,22 +11,22 @@
shows "normal H (G\<lparr>carrier:= (normalizer G H)\<rparr>)"
proof(intro group.normal_invI)
show "Group.group (G\<lparr>carrier := normalizer G H\<rparr>)"
- by (simp add: assms group.normalizer_imp_subgroup is_group subgroup_imp_group subgroup_imp_subset)
+ by (simp add: assms group.normalizer_imp_subgroup is_group subgroup_imp_group subgroup.subset)
have K:"H \<subseteq> (normalizer G H)" unfolding normalizer_def
proof
fix x assume xH: "x \<in> H"
- from xH have xG : "x \<in> carrier G" using subgroup_imp_subset assms by auto
+ from xH have xG : "x \<in> carrier G" using subgroup.subset assms by auto
have "x <# H = H"
by (metis \<open>x \<in> H\<close> assms group.lcos_mult_one is_group
- l_repr_independence one_closed subgroup_imp_subset)
+ l_repr_independence one_closed subgroup.subset)
moreover have "H #> inv x = H"
by (simp add: xH assms is_group subgroup.rcos_const subgroup.m_inv_closed)
ultimately have "x <# H #> (inv x) = H" by simp
thus " x \<in> stabilizer G (\<lambda>g. \<lambda>H\<in>{H. H \<subseteq> carrier G}. g <# H #> inv g) H"
- using assms xG subgroup_imp_subset unfolding stabilizer_def by auto
+ using assms xG subgroup.subset unfolding stabilizer_def by auto
qed
thus "subgroup H (G\<lparr>carrier:= (normalizer G H)\<rparr>)"
- using subgroup_incl normalizer_imp_subgroup assms by (simp add: subgroup_imp_subset)
+ using subgroup_incl normalizer_imp_subgroup assms by (simp add: subgroup.subset)
show " \<And>x h. x \<in> carrier (G\<lparr>carrier := normalizer G H\<rparr>) \<Longrightarrow> h \<in> H \<Longrightarrow>
x \<otimes>\<^bsub>G\<lparr>carrier := normalizer G H\<rparr>\<^esub> h
\<otimes>\<^bsub>G\<lparr>carrier := normalizer G H\<rparr>\<^esub> inv\<^bsub>G\<lparr>carrier := normalizer G H\<rparr>\<^esub> x \<in> H"
@@ -37,7 +37,7 @@
ultimately have "x \<otimes>\<^bsub>G\<lparr>carrier := normalizer G H\<rparr>\<^esub> h = x \<otimes> h" by simp
moreover have " inv\<^bsub>G\<lparr>carrier := normalizer G H\<rparr>\<^esub> x = inv x"
using xnormalizer
- by (simp add: assms normalizer_imp_subgroup subgroup_imp_subset subgroup_inv_equality)
+ by (simp add: assms normalizer_imp_subgroup subgroup.subset subgroup_inv_equality)
ultimately have xhxegal: "x \<otimes>\<^bsub>G\<lparr>carrier := normalizer G H\<rparr>\<^esub> h
\<otimes>\<^bsub>G\<lparr>carrier := normalizer G H\<rparr>\<^esub> inv\<^bsub>G\<lparr>carrier := normalizer G H\<rparr>\<^esub> x
= x \<otimes>h \<otimes> inv x"
@@ -45,7 +45,7 @@
have "x \<otimes>h \<otimes> inv x \<in> (x <# H #> inv x)"
unfolding l_coset_def r_coset_def using hH by auto
moreover have "x <# H #> inv x = H"
- using xnormalizer assms subgroup_imp_subset[OF assms]
+ using xnormalizer assms subgroup.subset[OF assms]
unfolding normalizer_def stabilizer_def by auto
ultimately have "x \<otimes>h \<otimes> inv x \<in> H" by simp
thus " x \<otimes>\<^bsub>G\<lparr>carrier := normalizer G H\<rparr>\<^esub> h
@@ -61,12 +61,12 @@
shows "subgroup H (G\<lparr>carrier := normalizer G N\<rparr>)"
proof-
have N_carrierG : "N \<subseteq> carrier(G)"
- using assms normal_imp_subgroup subgroup_imp_subset
+ using assms normal_imp_subgroup subgroup.subset
by (smt monoid.cases_scheme order_trans partial_object.simps(1) partial_object.update_convs(1))
{have "H \<subseteq> normalizer G N" unfolding normalizer_def stabilizer_def
proof
fix x assume xH : "x \<in> H"
- hence xcarrierG : "x \<in> carrier(G)" using assms subgroup_imp_subset by auto
+ hence xcarrierG : "x \<in> carrier(G)" using assms subgroup.subset by auto
have " N #> x = x <# N" using assms xH
unfolding r_coset_def l_coset_def normal_def normal_axioms_def subgroup_imp_group by auto
hence "x <# N #> inv x =(N #> x) #> inv x"
@@ -79,7 +79,7 @@
qed}
thus "subgroup H (G\<lparr>carrier := normalizer G N\<rparr>)"
using subgroup_incl[OF assms(1) normalizer_imp_subgroup]
- assms normal_imp_subgroup subgroup_imp_subset
+ assms normal_imp_subgroup subgroup.subset
by (metis group.incl_subgroup is_group)
qed
@@ -92,7 +92,7 @@
shows "subgroup (N<#>H) G" unfolding subgroup_def
proof-
have A :"N <#> H \<subseteq> carrier G"
- using assms setmult_subset_G by (simp add: normal_imp_subgroup subgroup_imp_subset)
+ using assms setmult_subset_G by (simp add: normal_imp_subgroup subgroup.subset)
have B :"\<And> x y. \<lbrakk>x \<in> (N <#> H); y \<in> (N <#> H)\<rbrakk> \<Longrightarrow> (x \<otimes> y) \<in> (N<#>H)"
proof-
@@ -102,7 +102,7 @@
obtain n2 h2 where B3:"n2 \<in> N \<and> h2 \<in> H \<and> n2\<otimes>h2 = y"
using set_mult_def B1b by (metis (no_types, lifting) UN_E singletonD)
have "N #> h1 = h1 <# N"
- using normalI B2 assms normal.coset_eq subgroup_imp_subset by blast
+ using normalI B2 assms normal.coset_eq subgroup.subset by blast
hence "h1\<otimes>n2 \<in> N #> h1"
using B2 B3 assms l_coset_def by fastforce
from this obtain y2 where y2_def:"y2 \<in> N" and y2_prop:"y2\<otimes>h1 = h1\<otimes>n2"
@@ -132,7 +132,7 @@
hence C4:"(inv h \<otimes> inv n \<otimes> h) \<otimes> inv h \<in> (N<#>H)"
using C2 assms subgroup.m_inv_closed[of H G h] unfolding set_mult_def by auto
have "inv h \<otimes> inv n \<otimes> h \<otimes> inv h = inv h \<otimes> inv n"
- using subgroup_imp_subset[OF assms(2)]
+ using subgroup.subset[OF assms(2)]
by (metis A C1 C2 C3 inv_closed inv_solve_right m_closed subsetCE)
thus "inv(x)\<in>N<#>H" using C4 C2 C3 by simp
qed
@@ -159,10 +159,10 @@
proof-
have Hyp:"subgroup (N <#>\<^bsub>G\<lparr>carrier := K\<rparr>\<^esub> H) (G\<lparr>carrier := K\<rparr>)"
using group.mult_norm_subgroup[where ?G = "G\<lparr>carrier := K\<rparr>"] assms subgroup_imp_group by auto
- have "H \<subseteq> carrier(G\<lparr>carrier := K\<rparr>)" using assms subgroup_imp_subset by blast
+ have "H \<subseteq> carrier(G\<lparr>carrier := K\<rparr>)" using assms subgroup.subset by blast
also have "... \<subseteq> K" by simp
finally have Incl1:"H \<subseteq> K" by simp
- have "N \<subseteq> carrier(G\<lparr>carrier := K\<rparr>)" using assms normal_imp_subgroup subgroup_imp_subset by blast
+ have "N \<subseteq> carrier(G\<lparr>carrier := K\<rparr>)" using assms normal_imp_subgroup subgroup.subset by blast
also have "... \<subseteq> K" by simp
finally have Incl2:"N \<subseteq> K" by simp
have "(N <#>\<^bsub>G\<lparr>carrier := K\<rparr>\<^esub> H) = (N <#> H)"
@@ -209,7 +209,7 @@
have GroupNH : "Group.group (G\<lparr>carrier := N<#>H\<rparr>)"
using subgroup_imp_group assms mult_norm_subgroup by simp
have HcarrierNH :"H \<subseteq> carrier(G\<lparr>carrier := N<#>H\<rparr>)"
- using assms subgroup_of_normal_set_mult subgroup_imp_subset by blast
+ using assms subgroup_of_normal_set_mult subgroup.subset by blast
hence HNH :"H \<subseteq> N<#>H" by simp
have op_hom : "f \<in> hom (G\<lparr>carrier := H\<rparr>) (G\<lparr>carrier := N <#> H\<rparr> Mod N)" unfolding hom_def
proof
@@ -277,7 +277,7 @@
have "x = (#>\<^bsub>G\<lparr>carrier := N <#> H\<rparr>\<^esub>) N (n \<otimes> h)" using K nhnh by simp
hence "x = (#>) N (n \<otimes> h)" using K nhnh unfolding r_coset_def by auto
also have "... = (N #> n) #>h"
- using coset_mult_assoc hH nN assms subgroup_imp_subset normal_imp_subgroup
+ using coset_mult_assoc hH nN assms subgroup.subset normal_imp_subgroup
by (metis subgroup.mem_carrier)
finally have "x = (#>) N h"
using coset_join2[of n N] nN assms by (simp add: normal_imp_subgroup subgroup.mem_carrier)
@@ -326,9 +326,9 @@
G\<lparr>carrier := normalizer G N, carrier := H\<rparr> Mod N \<inter> H =
(G\<lparr>carrier:= N<#>H\<rparr> Mod N) \<cong>
G\<lparr>carrier := normalizer G N, carrier := H\<rparr> Mod N \<inter> H"
- using subgroup_set_mult_equality[OF normalizer_imp_subgroup[OF subgroup_imp_subset[OF assms(2)]], of N H]
- subgroup_imp_subset[OF assms(3)]
- subgroup_imp_subset[OF normal_imp_subgroup[OF subgroup_in_normalizer[OF assms(2)]]]
+ using subgroup_set_mult_equality[OF normalizer_imp_subgroup[OF subgroup.subset[OF assms(2)]], of N H]
+ subgroup.subset[OF assms(3)]
+ subgroup.subset[OF normal_imp_subgroup[OF subgroup_in_normalizer[OF assms(2)]]]
by simp
ultimately have "G\<lparr>carrier := normalizer G N,
carrier := N <#>\<^bsub>G\<lparr>carrier := normalizer G N\<rparr>\<^esub> H\<rparr> Mod N \<cong>
@@ -338,7 +338,7 @@
carrier := N <#>\<^bsub>G\<lparr>carrier := normalizer G N\<rparr>\<^esub> H\<rparr> Mod N \<cong>
G\<lparr>carrier := normalizer G N, carrier := H\<rparr> Mod N \<inter> H"
using group.weak_snd_iso_thme[OF subgroup_imp_group[OF normalizer_imp_subgroup[OF
- subgroup_imp_subset[OF assms(2)]]] assms(3) subgroup_in_normalizer[OF assms(2)]]
+ subgroup.subset[OF assms(2)]]] assms(3) subgroup_in_normalizer[OF assms(2)]]
by simp
moreover have "H\<inter>N = N\<inter>H" using assms by auto
ultimately show "(G\<lparr>carrier:= N<#>H\<rparr> Mod N) \<cong> G\<lparr>carrier := H\<rparr> Mod H \<inter> N" by auto
@@ -350,7 +350,7 @@
and "subgroup N G"
and "subgroup H (G\<lparr>carrier:= (normalizer G N)\<rparr>)"
shows "(G\<lparr>carrier:= H<#>N\<rparr> Mod N) \<cong> (G\<lparr>carrier:= H\<rparr> Mod (H\<inter>N))"
- by (metis assms commut_normal_subgroup group.subgroup_in_normalizer is_group subgroup_imp_subset
+ by (metis assms commut_normal_subgroup group.subgroup_in_normalizer is_group subgroup.subset
normalizer_imp_subgroup snd_iso_thme)
@@ -365,29 +365,29 @@
shows "subgroup (H\<inter>K) (G\<lparr>carrier:=(normalizer G (H1<#>(H\<inter>K1))) \<rparr>)"
proof (intro subgroup_incl[OF subgroups_Inter_pair[OF assms(1) assms(3)]])
show "subgroup (normalizer G (H1 <#> H \<inter> K1)) G"
- using normalizer_imp_subgroup assms normal_imp_subgroup subgroup_imp_subset
+ using normalizer_imp_subgroup assms normal_imp_subgroup subgroup.subset
by (metis group.incl_subgroup is_group setmult_subset_G subgroups_Inter_pair)
next
show "H \<inter> K \<subseteq> normalizer G (H1 <#> H \<inter> K1)" unfolding normalizer_def stabilizer_def
proof
fix x assume xHK : "x \<in> H \<inter> K"
hence xG : "{x} \<subseteq> carrier G" "{inv x} \<subseteq> carrier G"
- using subgroup_imp_subset assms inv_closed xHK by auto
+ using subgroup.subset assms inv_closed xHK by auto
have allG : "H \<subseteq> carrier G" "K \<subseteq> carrier G" "H1 \<subseteq> carrier G" "K1 \<subseteq> carrier G"
- using assms subgroup_imp_subset normal_imp_subgroup incl_subgroup apply blast+ .
+ using assms subgroup.subset normal_imp_subgroup incl_subgroup apply blast+ .
have HK1_normal: "H\<inter>K1 \<lhd> (G\<lparr>carrier := H \<inter> K\<rparr>)" using normal_inter[OF assms(3)assms(1)assms(4)]
by (simp add : inf_commute)
have "H \<inter> K \<subseteq> normalizer G (H \<inter> K1)"
- using subgroup_imp_subset[OF normal_imp_subgroup_normalizer[OF subgroups_Inter_pair[OF
+ using subgroup.subset[OF normal_imp_subgroup_normalizer[OF subgroups_Inter_pair[OF
assms(1)assms(3)]HK1_normal]] by auto
hence "x <# (H \<inter> K1) #> inv x = (H \<inter> K1)"
- using xHK subgroup_imp_subset[OF subgroups_Inter_pair[OF assms(1) incl_subgroup[OF assms(3)
+ using xHK subgroup.subset[OF subgroups_Inter_pair[OF assms(1) incl_subgroup[OF assms(3)
normal_imp_subgroup[OF assms(4)]]]]
unfolding normalizer_def stabilizer_def by auto
moreover have "H \<subseteq> normalizer G H1"
- using subgroup_imp_subset[OF normal_imp_subgroup_normalizer[OF assms(1)assms(2)]] by auto
+ using subgroup.subset[OF normal_imp_subgroup_normalizer[OF assms(1)assms(2)]] by auto
hence "x <# H1 #> inv x = H1"
- using xHK subgroup_imp_subset[OF incl_subgroup[OF assms(1) normal_imp_subgroup[OF assms(2)]]]
+ using xHK subgroup.subset[OF incl_subgroup[OF assms(1) normal_imp_subgroup[OF assms(2)]]]
unfolding normalizer_def stabilizer_def by auto
ultimately have "H1 <#> H \<inter> K1 = (x <# H1 #> inv x) <#> (x <# H \<inter> K1 #> inv x)" by auto
also have "... = ({x} <#> H1) <#> {inv x} <#> ({x} <#> H \<inter> K1 <#> {inv x})"
@@ -418,31 +418,31 @@
shows " (H\<inter>K) \<inter> (H1<#>(H\<inter>K1)) = (H1\<inter>K)<#>(H\<inter>K1)"
proof
have all_inclG : "H \<subseteq> carrier G" "H1 \<subseteq> carrier G" "K \<subseteq> carrier G" "K1 \<subseteq> carrier G"
- using assms subgroup_imp_subset normal_imp_subgroup incl_subgroup apply blast+.
+ using assms subgroup.subset normal_imp_subgroup incl_subgroup apply blast+.
show "H \<inter> K \<inter> (H1 <#> H \<inter> K1) \<subseteq> H1 \<inter> K <#> H \<inter> K1"
proof
fix x assume x_def : "x \<in> (H \<inter> K) \<inter> (H1 <#> (H \<inter> K1))"
from x_def have x_incl : "x \<in> H" "x \<in> K" "x \<in> (H1 <#> (H \<inter> K1))" by auto
then obtain h1 hk1 where h1hk1_def : "h1 \<in> H1" "hk1 \<in> H \<inter> K1" "h1 \<otimes> hk1 = x"
using assms unfolding set_mult_def by blast
- hence "hk1 \<in> H \<inter> K" using subgroup_imp_subset[OF normal_imp_subgroup[OF assms(4)]] by auto
+ hence "hk1 \<in> H \<inter> K" using subgroup.subset[OF normal_imp_subgroup[OF assms(4)]] by auto
hence "inv hk1 \<in> H \<inter> K" using subgroup.m_inv_closed[OF subgroups_Inter_pair] assms by auto
moreover have "h1 \<otimes> hk1 \<in> H \<inter> K" using x_incl h1hk1_def by auto
ultimately have "h1 \<otimes> hk1 \<otimes> inv hk1 \<in> H \<inter> K"
using subgroup.m_closed[OF subgroups_Inter_pair] assms by auto
- hence "h1 \<in> H \<inter> K" using h1hk1_def assms subgroup_imp_subset incl_subgroup normal_imp_subgroup
+ hence "h1 \<in> H \<inter> K" using h1hk1_def assms subgroup.subset incl_subgroup normal_imp_subgroup
by (metis Int_iff contra_subsetD inv_solve_right m_closed)
hence "h1 \<in> H1 \<inter> H \<inter> K" using h1hk1_def by auto
- hence "h1 \<in> H1 \<inter> K" using subgroup_imp_subset[OF normal_imp_subgroup[OF assms(2)]] by auto
+ hence "h1 \<in> H1 \<inter> K" using subgroup.subset[OF normal_imp_subgroup[OF assms(2)]] by auto
hence "h1 \<otimes> hk1 \<in> (H1\<inter>K)<#>(H\<inter>K1)"
using h1hk1_def unfolding set_mult_def by auto
thus " x \<in> (H1\<inter>K)<#>(H\<inter>K1)" using h1hk1_def x_def by auto
qed
show "H1 \<inter> K <#> H \<inter> K1 \<subseteq> H \<inter> K \<inter> (H1 <#> H \<inter> K1)"
proof-
- have "H1 \<inter> K \<subseteq> H \<inter> K" using subgroup_imp_subset[OF normal_imp_subgroup[OF assms(2)]] by auto
+ have "H1 \<inter> K \<subseteq> H \<inter> K" using subgroup.subset[OF normal_imp_subgroup[OF assms(2)]] by auto
moreover have "H \<inter> K1 \<subseteq> H \<inter> K"
- using subgroup_imp_subset[OF normal_imp_subgroup[OF assms(4)]] by auto
+ using subgroup.subset[OF normal_imp_subgroup[OF assms(4)]] by auto
ultimately have "H1 \<inter> K <#> H \<inter> K1 \<subseteq> H \<inter> K" unfolding set_mult_def
using subgroup.m_closed[OF subgroups_Inter_pair [OF assms(1)assms(3)]] by blast
moreover have "H1 \<inter> K \<subseteq> H1" by auto
@@ -459,7 +459,7 @@
shows "(H1<#>(H\<inter>K1)) \<lhd> G\<lparr>carrier:=(H1<#>(H\<inter>K))\<rparr>"
proof-
have all_inclG : "H \<subseteq> carrier G" "H1 \<subseteq> carrier G" "K \<subseteq> carrier G" "K1 \<subseteq> carrier G"
- using assms subgroup_imp_subset normal_imp_subgroup incl_subgroup apply blast+.
+ using assms subgroup.subset normal_imp_subgroup incl_subgroup apply blast+.
have subH1:"subgroup (H1 <#> H \<inter> K) (G\<lparr>carrier := H\<rparr>)"
using mult_norm_sub_in_sub[OF assms(2)subgroup_incl[OF subgroups_Inter_pair[OF assms(1)assms(3)]
assms(1)]] assms by auto
@@ -469,13 +469,13 @@
using mult_norm_sub_in_sub[OF assms(2) subgroup_incl[OF subgroups_Inter_pair[OF
assms(1) incl_subgroup[OF assms(3)normal_imp_subgroup[OF assms(4)]]]]] assms by auto
hence "(H\<inter>K1) \<subseteq> (H\<inter>K)"
- using assms subgroup_imp_subset normal_imp_subgroup monoid.cases_scheme
+ using assms subgroup.subset normal_imp_subgroup monoid.cases_scheme
by (metis inf.mono partial_object.simps(1) partial_object.update_convs(1) subset_refl)
- hence incl:"(H1<#>(H\<inter>K1)) \<subseteq> H1<#>(H\<inter>K)" using assms subgroup_imp_subset normal_imp_subgroup
+ hence incl:"(H1<#>(H\<inter>K1)) \<subseteq> H1<#>(H\<inter>K)" using assms subgroup.subset normal_imp_subgroup
unfolding set_mult_def by blast
hence "subgroup (H1 <#> H \<inter> K1) (G\<lparr>carrier := (H1<#>(H\<inter>K))\<rparr>)"
using assms subgroup_incl[OF incl_subgroup[OF assms(1)subH2]incl_subgroup[OF assms(1)
- subH1]] normal_imp_subgroup subgroup_imp_subset unfolding set_mult_def by blast
+ subH1]] normal_imp_subgroup subgroup.subset unfolding set_mult_def by blast
moreover have " (\<And> x. x\<in>carrier (G\<lparr>carrier := H1 <#> H \<inter> K\<rparr>) \<Longrightarrow>
H1 <#> H\<inter>K1 #>\<^bsub>G\<lparr>carrier := H1 <#> H\<inter>K\<rparr>\<^esub> x = x <#\<^bsub>G\<lparr>carrier := H1 <#> H\<inter>K\<rparr>\<^esub> (H1 <#> H\<inter>K1))"
proof-
@@ -483,14 +483,14 @@
hence x_def : "x \<in> H1 <#> H \<inter> K" by simp
from this obtain h1 hk where h1hk_def :"h1 \<in> H1" "hk \<in> H \<inter> K" "h1 \<otimes> hk = x"
unfolding set_mult_def by blast
- have xH : "x \<in> H" using subgroup_imp_subset[OF subH1] using x_def by auto
+ have xH : "x \<in> H" using subgroup.subset[OF subH1] using x_def by auto
hence allG : "h1 \<in> carrier G" "hk \<in> carrier G" "x \<in> carrier G"
- using assms subgroup_imp_subset h1hk_def normal_imp_subgroup incl_subgroup apply blast+.
+ using assms subgroup.subset h1hk_def normal_imp_subgroup incl_subgroup apply blast+.
hence "x <#\<^bsub>G\<lparr>carrier := H1 <#> H\<inter>K\<rparr>\<^esub> (H1 <#> H\<inter>K1) =h1 \<otimes> hk <# (H1 <#> H\<inter>K1)"
- using subgroup_set_mult_equality subgroup_imp_subset xH h1hk_def by (simp add: l_coset_def)
+ using subgroup_set_mult_equality subgroup.subset xH h1hk_def by (simp add: l_coset_def)
also have "... = h1 <# (hk <# (H1 <#> H\<inter>K1))"
- using lcos_m_assoc[OF subgroup_imp_subset[OF incl_subgroup[OF assms(1) subH1]]allG(1)allG(2)]
- by (metis allG(1) allG(2) assms(1) incl_subgroup lcos_m_assoc subH2 subgroup_imp_subset)
+ using lcos_m_assoc[OF subgroup.subset[OF incl_subgroup[OF assms(1) subH1]]allG(1)allG(2)]
+ by (metis allG(1) allG(2) assms(1) incl_subgroup lcos_m_assoc subH2 subgroup.subset)
also have "... = h1 <# (hk <# H1 <#> H\<inter>K1)"
using set_mult_assoc all_inclG allG by (simp add: l_coset_eq_set_mult inf.coboundedI1)
also have "... = h1 <# (hk <# H1 #> \<one> <#> H\<inter>K1 #> \<one>)"
@@ -504,18 +504,18 @@
using rcos_assoc_lcos allG all_inclG
by (smt inf_le1 inv_closed l_coset_subset_G r_coset_subset_G setmult_rcos_assoc subset_trans)
moreover have "H \<subseteq> normalizer G H1"
- using assms h1hk_def subgroup_imp_subset[OF normal_imp_subgroup_normalizer] by simp
+ using assms h1hk_def subgroup.subset[OF normal_imp_subgroup_normalizer] by simp
hence "\<And>g. g \<in> H \<Longrightarrow> g \<in> {g \<in> carrier G. (\<lambda>H\<in>{H. H \<subseteq> carrier G}. g <# H #> inv g) H1 = H1}"
using all_inclG assms unfolding normalizer_def stabilizer_def by auto
hence "\<And>g. g \<in> H \<Longrightarrow> g <# H1 #> inv g = H1" using all_inclG by simp
hence "(hk <# H1 #> inv hk) = H1" using h1hk_def all_inclG by simp
moreover have "H\<inter>K \<subseteq> normalizer G (H\<inter>K1)"
using normal_inter[OF assms(3)assms(1)assms(4)] assms subgroups_Inter_pair
- subgroup_imp_subset[OF normal_imp_subgroup_normalizer] by (simp add: inf_commute)
+ subgroup.subset[OF normal_imp_subgroup_normalizer] by (simp add: inf_commute)
hence "\<And>g. g\<in>H\<inter>K \<Longrightarrow> g\<in>{g\<in>carrier G. (\<lambda>H\<in>{H. H \<subseteq> carrier G}. g <# H #> inv g) (H\<inter>K1) = H\<inter>K1}"
using all_inclG assms unfolding normalizer_def stabilizer_def by auto
hence "\<And>g. g \<in> H\<inter>K \<Longrightarrow> g <# (H\<inter>K1) #> inv g = H\<inter>K1"
- using subgroup_imp_subset[OF subgroups_Inter_pair[OF assms(1) incl_subgroup[OF
+ using subgroup.subset[OF subgroups_Inter_pair[OF assms(1) incl_subgroup[OF
assms(3)normal_imp_subgroup[OF assms(4)]]]] by auto
hence "(hk <# H\<inter>K1 #> inv hk) = H\<inter>K1" using h1hk_def by simp
ultimately have "x <#\<^bsub>G\<lparr>carrier := H1 <#> H \<inter> K\<rparr>\<^esub> (H1 <#> H \<inter> K1) = h1 <#(H1 <#> (H \<inter> K1)#> hk)"
@@ -529,7 +529,7 @@
finally have eq1 : "x <#\<^bsub>G\<lparr>carrier := H1 <#> H \<inter> K\<rparr>\<^esub> (H1 <#> H \<inter> K1) = H1 <#> (H \<inter> K1) #> hk"
by (simp add: allG(2) all_inclG inf.coboundedI2 setmult_rcos_assoc)
have "H1 <#> H \<inter> K1 #>\<^bsub>G\<lparr>carrier := H1 <#> H \<inter> K\<rparr>\<^esub> x = H1 <#> H \<inter> K1 #> (h1 \<otimes> hk)"
- using subgroup_set_mult_equality subgroup_imp_subset xH h1hk_def by (simp add: r_coset_def)
+ using subgroup_set_mult_equality subgroup.subset xH h1hk_def by (simp add: r_coset_def)
also have "... = H1 <#> H \<inter> K1 #> h1 #> hk"
using coset_mult_assoc by (simp add: allG all_inclG inf.coboundedI2 setmult_subset_G)
also have"... = H \<inter> K1 <#> H1 #> h1 #> hk"
@@ -565,18 +565,18 @@
have H_simp: "N<#>N1 = H1<#> (H\<inter>K)"
proof-
have H1_incl_G : "H1 \<subseteq> carrier G"
- using assms normal_imp_subgroup incl_subgroup subgroup_imp_subset by blast
+ using assms normal_imp_subgroup incl_subgroup subgroup.subset by blast
have K1_incl_G :"K1 \<subseteq> carrier G"
- using assms normal_imp_subgroup incl_subgroup subgroup_imp_subset by blast
+ using assms normal_imp_subgroup incl_subgroup subgroup.subset by blast
have "N<#>N1= (H\<inter>K)<#> (H1<#>(H\<inter>K1))" by (auto simp add: N_def N1_def)
also have "... = ((H\<inter>K)<#>H1) <#>(H\<inter>K1)"
using set_mult_assoc[where ?M = "H\<inter>K"] K1_incl_G H1_incl_G assms
- by (simp add: inf.coboundedI2 subgroup_imp_subset)
+ by (simp add: inf.coboundedI2 subgroup.subset)
also have "... = (H1<#>(H\<inter>K))<#>(H\<inter>K1)"
using commut_normal_subgroup assms subgroup_incl subgroups_Inter_pair by auto
also have "... = H1 <#> ((H\<inter>K)<#>(H\<inter>K1))"
using set_mult_assoc K1_incl_G H1_incl_G assms
- by (simp add: inf.coboundedI2 subgroup_imp_subset)
+ by (simp add: inf.coboundedI2 subgroup.subset)
also have " ((H\<inter>K)<#>(H\<inter>K1)) = (H\<inter>K)"
proof (intro set_mult_subgroup_idem[where ?H = "H\<inter>K" and ?N="H\<inter>K1",
OF subgroups_Inter_pair[OF assms(1) assms(3)]])
--- a/src/HOL/Analysis/Infinite_Products.thy Fri Jun 15 13:02:12 2018 +0200
+++ b/src/HOL/Analysis/Infinite_Products.thy Fri Jun 15 13:52:05 2018 +0100
@@ -98,6 +98,10 @@
using LIMSEQ_unique by blast
qed
+lemma raw_has_prod_Suc:
+ "raw_has_prod f (Suc M) a \<longleftrightarrow> raw_has_prod (\<lambda>n. f (Suc n)) M a"
+ unfolding raw_has_prod_def by auto
+
lemma has_prod_0_iff: "f has_prod 0 \<longleftrightarrow> (\<exists>i. f i = 0 \<and> (\<exists>p. raw_has_prod f (Suc i) p))"
by (simp add: has_prod_def)
@@ -1203,21 +1207,37 @@
qed
lemma convergent_prod_Suc_iff:
- assumes "\<And>k. f k \<noteq> 0" shows "convergent_prod (\<lambda>n. f (Suc n)) = convergent_prod f"
+ shows "convergent_prod (\<lambda>n. f (Suc n)) = convergent_prod f"
proof
assume "convergent_prod f"
- then have "f has_prod prodinf f"
- by (rule convergent_prod_has_prod)
- moreover have "prodinf f \<noteq> 0"
- by (simp add: \<open>convergent_prod f\<close> assms prodinf_nonzero)
- ultimately have "(\<lambda>n. f (Suc n)) has_prod (prodinf f * inverse (f 0))"
- by (simp add: has_prod_Suc_iff inverse_eq_divide assms)
- then show "convergent_prod (\<lambda>n. f (Suc n))"
- using has_prod_iff by blast
+ then obtain M L where M_nz:"\<forall>n\<ge>M. f n \<noteq> 0" and
+ M_L:"(\<lambda>n. \<Prod>i\<le>n. f (i + M)) \<longlonglongrightarrow> L" and "L \<noteq> 0"
+ unfolding convergent_prod_altdef by auto
+ have "(\<lambda>n. \<Prod>i\<le>n. f (Suc (i + M))) \<longlonglongrightarrow> L / f M"
+ proof -
+ have "(\<lambda>n. \<Prod>i\<in>{0..Suc n}. f (i + M)) \<longlonglongrightarrow> L"
+ using M_L
+ apply (subst (asm) LIMSEQ_Suc_iff[symmetric])
+ using atLeast0AtMost by auto
+ then have "(\<lambda>n. f M * (\<Prod>i\<in>{0..n}. f (Suc (i + M)))) \<longlonglongrightarrow> L"
+ apply (subst (asm) prod.atLeast0_atMost_Suc_shift)
+ by simp
+ then have "(\<lambda>n. (\<Prod>i\<in>{0..n}. f (Suc (i + M)))) \<longlonglongrightarrow> L/f M"
+ apply (drule_tac tendsto_divide)
+ using M_nz[rule_format,of M,simplified] by auto
+ then show ?thesis unfolding atLeast0AtMost .
+ qed
+ then show "convergent_prod (\<lambda>n. f (Suc n))" unfolding convergent_prod_altdef
+ apply (rule_tac exI[where x=M])
+ apply (rule_tac exI[where x="L/f M"])
+ using M_nz \<open>L\<noteq>0\<close> by auto
next
assume "convergent_prod (\<lambda>n. f (Suc n))"
- then show "convergent_prod f"
- using assms convergent_prod_def raw_has_prod_Suc_iff by blast
+ then obtain M where "\<exists>L. (\<forall>n\<ge>M. f (Suc n) \<noteq> 0) \<and> (\<lambda>n. \<Prod>i\<le>n. f (Suc (i + M))) \<longlonglongrightarrow> L \<and> L \<noteq> 0"
+ unfolding convergent_prod_altdef by auto
+ then show "convergent_prod f" unfolding convergent_prod_altdef
+ apply (rule_tac exI[where x="Suc M"])
+ using Suc_le_D by auto
qed
lemma raw_has_prod_inverse:
@@ -1256,6 +1276,26 @@
lemma prodinf_inverse: "convergent_prod f \<Longrightarrow> (\<Prod>n. inverse (f n)) = inverse (\<Prod>n. f n)"
by (intro has_prod_unique [symmetric] has_prod_inverse convergent_prod_has_prod)
+lemma has_prod_Suc_imp:
+ assumes "(\<lambda>n. f (Suc n)) has_prod a"
+ shows "f has_prod (a * f 0)"
+proof -
+ have "f has_prod (a * f 0)" when "raw_has_prod (\<lambda>n. f (Suc n)) 0 a"
+ apply (cases "f 0=0")
+ using that unfolding has_prod_def raw_has_prod_Suc
+ by (auto simp add: raw_has_prod_Suc_iff)
+ moreover have "f has_prod (a * f 0)" when
+ "(\<exists>i q. a = 0 \<and> f (Suc i) = 0 \<and> raw_has_prod (\<lambda>n. f (Suc n)) (Suc i) q)"
+ proof -
+ from that
+ obtain i q where "a = 0" "f (Suc i) = 0" "raw_has_prod (\<lambda>n. f (Suc n)) (Suc i) q"
+ by auto
+ then show ?thesis unfolding has_prod_def
+ by (auto intro!:exI[where x="Suc i"] simp:raw_has_prod_Suc)
+ qed
+ ultimately show "f has_prod (a * f 0)" using assms unfolding has_prod_def by auto
+qed
+
lemma has_prod_iff_shift:
assumes "\<And>i. i < n \<Longrightarrow> f i \<noteq> 0"
shows "(\<lambda>i. f (i + n)) has_prod a \<longleftrightarrow> f has_prod (a * (\<Prod>i<n. f i))"
@@ -1373,6 +1413,24 @@
end
+lemma exp_suminf_prodinf_real:
+ fixes f :: "nat \<Rightarrow> real"
+ assumes ge0:"\<And>n. f n \<ge> 0" and ac: "abs_convergent_prod (\<lambda>n. exp (f n))"
+ shows "prodinf (\<lambda>i. exp (f i)) = exp (suminf f)"
+proof -
+ have "summable f"
+ using ac unfolding abs_convergent_prod_conv_summable
+ proof (elim summable_comparison_test')
+ fix n
+ show "norm (f n) \<le> norm (exp (f n) - 1)"
+ using ge0[of n]
+ by (metis abs_of_nonneg add.commute diff_add_cancel diff_ge_0_iff_ge exp_ge_add_one_self
+ exp_le_cancel_iff one_le_exp_iff real_norm_def)
+ qed
+ then show ?thesis
+ by (simp add: prodinf_exp)
+qed
+
lemma has_prod_imp_sums_ln_real:
fixes f :: "nat \<Rightarrow> real"
assumes "raw_has_prod f 0 p" and 0: "\<And>x. f x > 0"