author paulson Fri, 15 Jun 2018 13:52:05 +0100 changeset 68453 febbf8f2881d parent 68451 c34aa23a1fb6 (current diff) parent 68452 c027dfbfad30 (diff) child 68454 f35aa0e7255d
merged
```--- 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: card_rcosets_equal subgroup_imp_subset)
+  apply (simp add: card_rcosets_equal subgroup.subset)
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)]
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))"

@@ -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]