more on infinite products. Also subgroup_imp_subset -> subgroup.subset
authorpaulson <lp15@cam.ac.uk>
Fri Jun 15 12:18:06 2018 +0100 (10 months ago)
changeset 68452c027dfbfad30
parent 68449 6d0f1a5a16ea
child 68453 febbf8f2881d
more on infinite products. Also subgroup_imp_subset -> subgroup.subset
src/HOL/Algebra/Coset.thy
src/HOL/Algebra/Group.thy
src/HOL/Algebra/Zassenhaus.thy
src/HOL/Analysis/Infinite_Products.thy
     1.1 --- a/src/HOL/Algebra/Coset.thy	Thu Jun 14 17:50:23 2018 +0200
     1.2 +++ b/src/HOL/Algebra/Coset.thy	Fri Jun 15 12:18:06 2018 +0100
     1.3 @@ -303,7 +303,7 @@
     1.4    shows "subgroup (H <#> K) G"
     1.5  proof (rule subgroup.intro)
     1.6    show "H <#> K \<subseteq> carrier G"
     1.7 -    by (simp add: setmult_subset_G assms subgroup_imp_subset)
     1.8 +    by (simp add: setmult_subset_G assms subgroup.subset)
     1.9  next
    1.10    have "\<one> \<otimes> \<one> \<in> H <#> K"
    1.11      unfolding set_mult_def using assms subgroup.one_closed by blast
    1.12 @@ -821,7 +821,7 @@
    1.13  apply (rule card_partition)
    1.14     apply (simp add: rcosets_subset_PowG [THEN finite_subset])
    1.15    apply (simp add: rcosets_part_G)
    1.16 -  apply (simp add: card_rcosets_equal subgroup_imp_subset)
    1.17 +  apply (simp add: card_rcosets_equal subgroup.subset)
    1.18  apply (simp add: rcos_disjoint)
    1.19  done
    1.20  
    1.21 @@ -843,11 +843,11 @@
    1.22        hence finite_rcos: "finite (rcosets H)" by simp
    1.23        hence "card (\<Union>(rcosets H)) = (\<Sum>R\<in>(rcosets H). card R)"
    1.24          using card_Union_disjoint[of "rcosets H"] finite_H rcos_disjoint[OF assms(1)]
    1.25 -              rcosets_finite[where ?H = H] by (simp add: assms subgroup_imp_subset)
    1.26 +              rcosets_finite[where ?H = H] by (simp add: assms subgroup.subset)
    1.27        hence "order G = (\<Sum>R\<in>(rcosets H). card R)"
    1.28          by (simp add: assms order_def rcosets_part_G)
    1.29        hence "order G = (\<Sum>R\<in>(rcosets H). card H)"
    1.30 -        using card_rcosets_equal by (simp add: assms subgroup_imp_subset)
    1.31 +        using card_rcosets_equal by (simp add: assms subgroup.subset)
    1.32        hence "order G = (card H) * (card (rcosets H))" by simp
    1.33        hence "order G \<noteq> 0" using finite_rcos finite_H assms ex_in_conv
    1.34                                  rcosets_part_G subgroup.one_closed by fastforce
    1.35 @@ -1094,13 +1094,13 @@
    1.36    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"
    1.37    proof-
    1.38      fix x h assume xGK : "x \<in> carrier (G \<times>\<times> K)" and hHN : " h \<in> H \<times> N"
    1.39 -    hence hGK : "h \<in> carrier (G \<times>\<times> K)" using subgroup_imp_subset[OF sub] by auto
    1.40 +    hence hGK : "h \<in> carrier (G \<times>\<times> K)" using subgroup.subset[OF sub] by auto
    1.41      from xGK obtain x1 x2 where x1x2 :"x1 \<in> carrier G" "x2 \<in> carrier K" "x = (x1,x2)"
    1.42        unfolding DirProd_def by fastforce
    1.43      from hHN obtain h1 h2 where h1h2 : "h1 \<in> H" "h2 \<in> N" "h = (h1,h2)"
    1.44        unfolding DirProd_def by fastforce
    1.45      hence h1h2GK : "h1 \<in> carrier G" "h2 \<in> carrier K"
    1.46 -      using normal_imp_subgroup subgroup_imp_subset assms apply blast+.
    1.47 +      using normal_imp_subgroup subgroup.subset assms apply blast+.
    1.48      have "inv\<^bsub>G \<times>\<times> K\<^esub> x = (inv\<^bsub>G\<^esub> x1,inv\<^bsub>K\<^esub> x2)"
    1.49        using inv_DirProd[OF group_axioms assms(1) x1x2(1)x1x2(2)] x1x2 by auto
    1.50      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)"
    1.51 @@ -1160,7 +1160,7 @@
    1.52    shows "(carrier G) <#> H = carrier G"
    1.53  proof
    1.54    show "(carrier G)<#>H \<subseteq> carrier G" 
    1.55 -    unfolding set_mult_def using subgroup_imp_subset assms by blast
    1.56 +    unfolding set_mult_def using subgroup.subset assms by blast
    1.57  next
    1.58    have " (carrier G) #>  \<one> = carrier G" unfolding set_mult_def r_coset_def group_axioms by simp
    1.59    moreover have "(carrier G) #>  \<one> \<subseteq> (carrier G) <#> H" unfolding set_mult_def r_coset_def
    1.60 @@ -1173,7 +1173,7 @@
    1.61    assumes "subgroup H G"
    1.62      and "subgroup N (G\<lparr>carrier:=H\<rparr>)"
    1.63    shows "H<#>N = H"
    1.64 -  using group.set_mult_carrier_idem[OF subgroup_imp_group] subgroup_imp_subset assms
    1.65 +  using group.set_mult_carrier_idem[OF subgroup_imp_group] subgroup.subset assms
    1.66    by (metis monoid.cases_scheme order_refl partial_object.simps(1)
    1.67        partial_object.update_convs(1) subgroup_set_mult_equality)
    1.68  
    1.69 @@ -1196,9 +1196,9 @@
    1.70      and "subgroup K (G\<lparr>carrier:=H\<rparr>)"
    1.71    shows "K<#>N = N<#>K"
    1.72  proof-
    1.73 -  have "N \<subseteq> carrier (G\<lparr>carrier := H\<rparr>)" using assms normal_imp_subgroup subgroup_imp_subset by blast
    1.74 +  have "N \<subseteq> carrier (G\<lparr>carrier := H\<rparr>)" using assms normal_imp_subgroup subgroup.subset by blast
    1.75    hence NH : "N \<subseteq> H" by simp
    1.76 -  have "K \<subseteq> carrier(G\<lparr>carrier := H\<rparr>)" using subgroup_imp_subset assms by blast
    1.77 +  have "K \<subseteq> carrier(G\<lparr>carrier := H\<rparr>)" using subgroup.subset assms by blast
    1.78    hence KH : "K \<subseteq> H" by simp
    1.79    have Egal : "K <#>\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> N = N <#>\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> K"
    1.80    using group.commut_normal[where ?G = "G\<lparr>carrier :=H\<rparr>", of K N,OF subgroup_imp_group[OF assms(1)]
    1.81 @@ -1235,7 +1235,7 @@
    1.82        show "subgroup (H\<inter>K) G" using HK_def subgroups_Inter_pair assms by auto
    1.83      next
    1.84        have "H1 \<subseteq> (carrier (G\<lparr>carrier:=H\<rparr>))" 
    1.85 -        using  assms(3) normal_imp_subgroup subgroup_imp_subset by blast
    1.86 +        using  assms(3) normal_imp_subgroup subgroup.subset by blast
    1.87        also have "... \<subseteq> H" by simp
    1.88        thus "H1K \<subseteq>H\<inter>K" 
    1.89          using H1K_def calculation by auto
    1.90 @@ -1256,7 +1256,7 @@
    1.91        hence invx:"inv\<^bsub>GHK\<^esub> x = inv\<^bsub>GH\<^esub> x"
    1.92          using invHK assms GHK_def HK_def GH_def subgroup_inv_equality subgroups_Inter_pair by simp
    1.93        have "H1\<subseteq>carrier(GH)"
    1.94 -        using assms GH_def normal_imp_subgroup subgroup_imp_subset by blast
    1.95 +        using assms GH_def normal_imp_subgroup subgroup.subset by blast
    1.96        hence hHK:"h\<in>HK" 
    1.97          using p2 H1K_def HK_def GH_def by auto
    1.98        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.99 @@ -1291,7 +1291,7 @@
   1.100    moreover have "normal N (G \<lparr>carrier :=K\<rparr>)" using assms K_def by simp
   1.101    ultimately have "N \<inter> H \<lhd> G\<lparr>carrier := K \<inter> H\<rparr>"
   1.102      using normal_inter[of K H N] assms(1) by blast
   1.103 -  moreover have "K \<inter> H = H" using K_def assms subgroup_imp_subset by blast
   1.104 +  moreover have "K \<inter> H = H" using K_def assms subgroup.subset by blast
   1.105    ultimately show "normal (N\<inter>H) (G\<lparr>carrier := H\<rparr>)" by auto
   1.106  qed
   1.107  
     2.1 --- a/src/HOL/Algebra/Group.thy	Thu Jun 14 17:50:23 2018 +0200
     2.2 +++ b/src/HOL/Algebra/Group.thy	Fri Jun 15 12:18:06 2018 +0100
     2.3 @@ -1274,9 +1274,9 @@
     2.4      and "subgroup I (G\<lparr>carrier:=J\<rparr>)"
     2.5    shows "subgroup I G" unfolding subgroup_def
     2.6  proof
     2.7 -  have H1: "I \<subseteq> carrier (G\<lparr>carrier:=J\<rparr>)" using assms(2) subgroup_imp_subset by blast
     2.8 +  have H1: "I \<subseteq> carrier (G\<lparr>carrier:=J\<rparr>)" using assms(2) subgroup.subset by blast
     2.9    also have H2: "...\<subseteq>J" by simp
    2.10 -  also  have "...\<subseteq>(carrier G)"  by (simp add: assms(1) subgroup_imp_subset)
    2.11 +  also  have "...\<subseteq>(carrier G)"  by (simp add: assms(1) subgroup.subset)
    2.12    finally have H: "I \<subseteq> carrier G" by simp
    2.13    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)
    2.14    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
     3.1 --- a/src/HOL/Algebra/Zassenhaus.thy	Thu Jun 14 17:50:23 2018 +0200
     3.2 +++ b/src/HOL/Algebra/Zassenhaus.thy	Fri Jun 15 12:18:06 2018 +0100
     3.3 @@ -11,22 +11,22 @@
     3.4    shows "normal H (G\<lparr>carrier:= (normalizer G H)\<rparr>)"
     3.5  proof(intro group.normal_invI)
     3.6    show "Group.group (G\<lparr>carrier := normalizer G H\<rparr>)"
     3.7 -    by (simp add: assms group.normalizer_imp_subgroup is_group subgroup_imp_group subgroup_imp_subset)
     3.8 +    by (simp add: assms group.normalizer_imp_subgroup is_group subgroup_imp_group subgroup.subset)
     3.9    have K:"H \<subseteq> (normalizer G H)" unfolding normalizer_def
    3.10    proof
    3.11      fix x assume xH: "x \<in> H"
    3.12 -    from xH have xG : "x \<in> carrier G" using subgroup_imp_subset assms by auto
    3.13 +    from xH have xG : "x \<in> carrier G" using subgroup.subset assms by auto
    3.14      have "x <# H = H"
    3.15        by (metis \<open>x \<in> H\<close> assms group.lcos_mult_one is_group
    3.16 -         l_repr_independence one_closed subgroup_imp_subset)
    3.17 +         l_repr_independence one_closed subgroup.subset)
    3.18      moreover have "H #> inv x = H" 
    3.19        by (simp add: xH assms is_group subgroup.rcos_const subgroup.m_inv_closed)
    3.20      ultimately have "x <# H #> (inv x) = H" by simp
    3.21      thus " x \<in> stabilizer G (\<lambda>g. \<lambda>H\<in>{H. H \<subseteq> carrier G}. g <# H #> inv g) H"
    3.22 -      using assms xG subgroup_imp_subset unfolding stabilizer_def by auto
    3.23 +      using assms xG subgroup.subset unfolding stabilizer_def by auto
    3.24    qed
    3.25    thus "subgroup H (G\<lparr>carrier:= (normalizer G H)\<rparr>)"
    3.26 -    using subgroup_incl normalizer_imp_subgroup assms by (simp add: subgroup_imp_subset)
    3.27 +    using subgroup_incl normalizer_imp_subgroup assms by (simp add: subgroup.subset)
    3.28    show  " \<And>x h. x \<in> carrier (G\<lparr>carrier := normalizer G H\<rparr>) \<Longrightarrow> h \<in> H \<Longrightarrow>
    3.29               x \<otimes>\<^bsub>G\<lparr>carrier := normalizer G H\<rparr>\<^esub> h
    3.30                 \<otimes>\<^bsub>G\<lparr>carrier := normalizer G H\<rparr>\<^esub> inv\<^bsub>G\<lparr>carrier := normalizer G H\<rparr>\<^esub> x \<in> H"
    3.31 @@ -37,7 +37,7 @@
    3.32      ultimately have "x \<otimes>\<^bsub>G\<lparr>carrier := normalizer G H\<rparr>\<^esub> h = x \<otimes> h" by simp
    3.33      moreover have " inv\<^bsub>G\<lparr>carrier := normalizer G H\<rparr>\<^esub> x =  inv x"
    3.34        using xnormalizer
    3.35 -      by (simp add: assms normalizer_imp_subgroup subgroup_imp_subset subgroup_inv_equality)
    3.36 +      by (simp add: assms normalizer_imp_subgroup subgroup.subset subgroup_inv_equality)
    3.37      ultimately  have xhxegal: "x \<otimes>\<^bsub>G\<lparr>carrier := normalizer G H\<rparr>\<^esub> h
    3.38                  \<otimes>\<^bsub>G\<lparr>carrier := normalizer G H\<rparr>\<^esub> inv\<^bsub>G\<lparr>carrier := normalizer G H\<rparr>\<^esub> x
    3.39                    = x \<otimes>h \<otimes> inv x"
    3.40 @@ -45,7 +45,7 @@
    3.41      have  "x \<otimes>h \<otimes> inv x \<in> (x <# H #> inv x)"
    3.42        unfolding l_coset_def r_coset_def using hH  by auto
    3.43      moreover have "x <# H #> inv x = H"
    3.44 -      using xnormalizer assms subgroup_imp_subset[OF assms]
    3.45 +      using xnormalizer assms subgroup.subset[OF assms]
    3.46        unfolding normalizer_def stabilizer_def by auto
    3.47      ultimately have "x \<otimes>h \<otimes> inv x \<in> H" by simp
    3.48      thus  " x \<otimes>\<^bsub>G\<lparr>carrier := normalizer G H\<rparr>\<^esub> h
    3.49 @@ -61,12 +61,12 @@
    3.50    shows "subgroup H (G\<lparr>carrier := normalizer G N\<rparr>)" 
    3.51  proof-
    3.52    have N_carrierG : "N \<subseteq> carrier(G)"
    3.53 -    using assms normal_imp_subgroup subgroup_imp_subset
    3.54 +    using assms normal_imp_subgroup subgroup.subset
    3.55      by (smt monoid.cases_scheme order_trans partial_object.simps(1) partial_object.update_convs(1))
    3.56    {have "H \<subseteq> normalizer G N" unfolding normalizer_def stabilizer_def
    3.57      proof
    3.58        fix x assume xH : "x \<in> H"
    3.59 -      hence xcarrierG : "x \<in> carrier(G)" using assms subgroup_imp_subset  by auto
    3.60 +      hence xcarrierG : "x \<in> carrier(G)" using assms subgroup.subset  by auto
    3.61        have "   N #> x = x <# N" using assms xH
    3.62          unfolding r_coset_def l_coset_def normal_def normal_axioms_def subgroup_imp_group by auto
    3.63        hence "x <# N #> inv x =(N #> x) #> inv x"
    3.64 @@ -79,7 +79,7 @@
    3.65      qed}
    3.66    thus "subgroup H (G\<lparr>carrier := normalizer G N\<rparr>)"
    3.67      using subgroup_incl[OF assms(1) normalizer_imp_subgroup]
    3.68 -      assms normal_imp_subgroup subgroup_imp_subset
    3.69 +      assms normal_imp_subgroup subgroup.subset
    3.70      by (metis  group.incl_subgroup is_group)
    3.71  qed
    3.72  
    3.73 @@ -92,7 +92,7 @@
    3.74    shows "subgroup (N<#>H) G" unfolding subgroup_def
    3.75  proof-
    3.76    have  A :"N <#> H \<subseteq> carrier G"
    3.77 -    using assms  setmult_subset_G by (simp add: normal_imp_subgroup subgroup_imp_subset)
    3.78 +    using assms  setmult_subset_G by (simp add: normal_imp_subgroup subgroup.subset)
    3.79  
    3.80    have B :"\<And> x y. \<lbrakk>x \<in> (N <#> H); y \<in> (N <#> H)\<rbrakk> \<Longrightarrow> (x \<otimes> y) \<in> (N<#>H)"
    3.81    proof-
    3.82 @@ -102,7 +102,7 @@
    3.83      obtain n2 h2 where B3:"n2 \<in> N \<and> h2 \<in> H \<and> n2\<otimes>h2 = y"
    3.84        using set_mult_def B1b by (metis (no_types, lifting) UN_E singletonD)
    3.85      have "N #> h1 = h1 <# N"
    3.86 -      using normalI B2 assms normal.coset_eq subgroup_imp_subset by blast
    3.87 +      using normalI B2 assms normal.coset_eq subgroup.subset by blast
    3.88      hence "h1\<otimes>n2 \<in> N #> h1" 
    3.89        using B2 B3 assms l_coset_def by fastforce
    3.90      from this obtain y2 where y2_def:"y2 \<in> N" and y2_prop:"y2\<otimes>h1 = h1\<otimes>n2" 
    3.91 @@ -132,7 +132,7 @@
    3.92      hence  C4:"(inv h \<otimes> inv n \<otimes> h) \<otimes> inv h \<in> (N<#>H)" 
    3.93        using   C2 assms subgroup.m_inv_closed[of H G h] unfolding set_mult_def by auto
    3.94      have "inv h \<otimes> inv n \<otimes> h \<otimes> inv h = inv h \<otimes> inv n"
    3.95 -      using  subgroup_imp_subset[OF assms(2)] 
    3.96 +      using  subgroup.subset[OF assms(2)] 
    3.97        by (metis A C1 C2 C3 inv_closed inv_solve_right m_closed subsetCE)
    3.98      thus "inv(x)\<in>N<#>H" using C4 C2 C3 by simp
    3.99    qed
   3.100 @@ -159,10 +159,10 @@
   3.101  proof-
   3.102    have Hyp:"subgroup (N <#>\<^bsub>G\<lparr>carrier := K\<rparr>\<^esub> H) (G\<lparr>carrier := K\<rparr>)"
   3.103      using group.mult_norm_subgroup[where ?G = "G\<lparr>carrier := K\<rparr>"] assms subgroup_imp_group by auto
   3.104 -  have "H \<subseteq> carrier(G\<lparr>carrier := K\<rparr>)" using assms subgroup_imp_subset by blast
   3.105 +  have "H \<subseteq> carrier(G\<lparr>carrier := K\<rparr>)" using assms subgroup.subset by blast
   3.106    also have "... \<subseteq> K" by simp
   3.107    finally have Incl1:"H \<subseteq> K" by simp
   3.108 -  have "N \<subseteq> carrier(G\<lparr>carrier := K\<rparr>)" using assms normal_imp_subgroup subgroup_imp_subset by blast
   3.109 +  have "N \<subseteq> carrier(G\<lparr>carrier := K\<rparr>)" using assms normal_imp_subgroup subgroup.subset by blast
   3.110    also have "... \<subseteq> K" by simp
   3.111    finally have Incl2:"N \<subseteq> K" by simp
   3.112    have "(N <#>\<^bsub>G\<lparr>carrier := K\<rparr>\<^esub> H) = (N <#> H)"
   3.113 @@ -209,7 +209,7 @@
   3.114    have GroupNH : "Group.group (G\<lparr>carrier := N<#>H\<rparr>)"
   3.115      using subgroup_imp_group assms mult_norm_subgroup by simp
   3.116    have  HcarrierNH :"H \<subseteq> carrier(G\<lparr>carrier := N<#>H\<rparr>)"
   3.117 -    using assms subgroup_of_normal_set_mult subgroup_imp_subset by blast
   3.118 +    using assms subgroup_of_normal_set_mult subgroup.subset by blast
   3.119    hence HNH :"H \<subseteq> N<#>H" by simp
   3.120    have op_hom : "f \<in> hom (G\<lparr>carrier := H\<rparr>) (G\<lparr>carrier := N <#> H\<rparr> Mod N)" unfolding hom_def
   3.121    proof
   3.122 @@ -277,7 +277,7 @@
   3.123        have  "x = (#>\<^bsub>G\<lparr>carrier := N <#> H\<rparr>\<^esub>) N (n \<otimes> h)" using K nhnh by simp
   3.124        hence  "x = (#>) N (n \<otimes> h)" using K nhnh unfolding r_coset_def by auto
   3.125        also have "... = (N #> n) #>h"
   3.126 -        using coset_mult_assoc hH nN assms subgroup_imp_subset normal_imp_subgroup
   3.127 +        using coset_mult_assoc hH nN assms subgroup.subset normal_imp_subgroup
   3.128          by (metis subgroup.mem_carrier)
   3.129        finally have "x = (#>) N h"
   3.130          using coset_join2[of n N] nN assms by (simp add: normal_imp_subgroup subgroup.mem_carrier)
   3.131 @@ -326,9 +326,9 @@
   3.132           G\<lparr>carrier := normalizer G N, carrier := H\<rparr> Mod N \<inter> H =
   3.133            (G\<lparr>carrier:= N<#>H\<rparr> Mod N)  \<cong>
   3.134           G\<lparr>carrier := normalizer G N, carrier := H\<rparr> Mod N \<inter> H" 
   3.135 -    using subgroup_set_mult_equality[OF  normalizer_imp_subgroup[OF subgroup_imp_subset[OF assms(2)]], of N H] 
   3.136 -          subgroup_imp_subset[OF assms(3)]
   3.137 -          subgroup_imp_subset[OF normal_imp_subgroup[OF subgroup_in_normalizer[OF assms(2)]]]
   3.138 +    using subgroup_set_mult_equality[OF  normalizer_imp_subgroup[OF subgroup.subset[OF assms(2)]], of N H] 
   3.139 +          subgroup.subset[OF assms(3)]
   3.140 +          subgroup.subset[OF normal_imp_subgroup[OF subgroup_in_normalizer[OF assms(2)]]]
   3.141      by simp
   3.142    ultimately have "G\<lparr>carrier := normalizer G N,
   3.143                      carrier := N <#>\<^bsub>G\<lparr>carrier := normalizer G N\<rparr>\<^esub> H\<rparr> Mod N  \<cong>
   3.144 @@ -338,7 +338,7 @@
   3.145                      carrier := N <#>\<^bsub>G\<lparr>carrier := normalizer G N\<rparr>\<^esub> H\<rparr> Mod N  \<cong>
   3.146                    G\<lparr>carrier := normalizer G N, carrier := H\<rparr> Mod N \<inter> H"
   3.147      using group.weak_snd_iso_thme[OF subgroup_imp_group[OF normalizer_imp_subgroup[OF
   3.148 -          subgroup_imp_subset[OF assms(2)]]] assms(3) subgroup_in_normalizer[OF assms(2)]]
   3.149 +          subgroup.subset[OF assms(2)]]] assms(3) subgroup_in_normalizer[OF assms(2)]]
   3.150      by simp
   3.151    moreover have "H\<inter>N = N\<inter>H" using assms  by auto
   3.152    ultimately show "(G\<lparr>carrier:= N<#>H\<rparr> Mod N)  \<cong>  G\<lparr>carrier := H\<rparr> Mod H \<inter> N" by auto
   3.153 @@ -350,7 +350,7 @@
   3.154      and "subgroup N G"
   3.155      and "subgroup H (G\<lparr>carrier:= (normalizer G N)\<rparr>)"
   3.156    shows "(G\<lparr>carrier:= H<#>N\<rparr> Mod N)  \<cong> (G\<lparr>carrier:= H\<rparr> Mod (H\<inter>N))"
   3.157 -  by (metis assms commut_normal_subgroup group.subgroup_in_normalizer is_group subgroup_imp_subset
   3.158 +  by (metis assms commut_normal_subgroup group.subgroup_in_normalizer is_group subgroup.subset
   3.159        normalizer_imp_subgroup snd_iso_thme)
   3.160  
   3.161  
   3.162 @@ -365,29 +365,29 @@
   3.163    shows "subgroup (H\<inter>K) (G\<lparr>carrier:=(normalizer G (H1<#>(H\<inter>K1))) \<rparr>)"
   3.164  proof (intro subgroup_incl[OF subgroups_Inter_pair[OF assms(1) assms(3)]])
   3.165    show "subgroup (normalizer G (H1 <#> H \<inter> K1)) G"
   3.166 -    using normalizer_imp_subgroup assms normal_imp_subgroup subgroup_imp_subset
   3.167 +    using normalizer_imp_subgroup assms normal_imp_subgroup subgroup.subset
   3.168      by (metis group.incl_subgroup is_group setmult_subset_G subgroups_Inter_pair)
   3.169  next
   3.170    show "H \<inter> K \<subseteq> normalizer G (H1 <#> H \<inter> K1)" unfolding normalizer_def stabilizer_def
   3.171    proof
   3.172      fix x assume xHK : "x \<in> H \<inter> K"
   3.173      hence xG : "{x} \<subseteq> carrier G" "{inv x} \<subseteq> carrier G"
   3.174 -      using subgroup_imp_subset assms inv_closed xHK by auto
   3.175 +      using subgroup.subset assms inv_closed xHK by auto
   3.176      have allG : "H \<subseteq> carrier G" "K \<subseteq> carrier G" "H1 \<subseteq> carrier G"  "K1 \<subseteq> carrier G"
   3.177 -      using assms subgroup_imp_subset normal_imp_subgroup incl_subgroup apply blast+ .
   3.178 +      using assms subgroup.subset normal_imp_subgroup incl_subgroup apply blast+ .
   3.179      have HK1_normal: "H\<inter>K1 \<lhd> (G\<lparr>carrier :=  H \<inter> K\<rparr>)" using normal_inter[OF assms(3)assms(1)assms(4)]
   3.180        by (simp add : inf_commute)
   3.181      have "H \<inter> K \<subseteq> normalizer G (H \<inter> K1)"
   3.182 -      using subgroup_imp_subset[OF normal_imp_subgroup_normalizer[OF subgroups_Inter_pair[OF
   3.183 +      using subgroup.subset[OF normal_imp_subgroup_normalizer[OF subgroups_Inter_pair[OF
   3.184              assms(1)assms(3)]HK1_normal]] by auto
   3.185      hence "x <# (H \<inter> K1) #> inv x = (H \<inter> K1)"
   3.186 -      using xHK subgroup_imp_subset[OF subgroups_Inter_pair[OF assms(1) incl_subgroup[OF assms(3)
   3.187 +      using xHK subgroup.subset[OF subgroups_Inter_pair[OF assms(1) incl_subgroup[OF assms(3)
   3.188                                                              normal_imp_subgroup[OF assms(4)]]]]
   3.189        unfolding normalizer_def stabilizer_def by auto
   3.190      moreover have "H \<subseteq>  normalizer G H1"
   3.191 -      using subgroup_imp_subset[OF normal_imp_subgroup_normalizer[OF assms(1)assms(2)]] by auto
   3.192 +      using subgroup.subset[OF normal_imp_subgroup_normalizer[OF assms(1)assms(2)]] by auto
   3.193      hence "x <# H1 #> inv x = H1"
   3.194 -      using xHK subgroup_imp_subset[OF  incl_subgroup[OF assms(1) normal_imp_subgroup[OF assms(2)]]]
   3.195 +      using xHK subgroup.subset[OF  incl_subgroup[OF assms(1) normal_imp_subgroup[OF assms(2)]]]
   3.196        unfolding normalizer_def stabilizer_def by auto
   3.197      ultimately have "H1 <#> H \<inter> K1 = (x <# H1 #> inv x) <#> (x <#  H \<inter> K1 #> inv x)" by auto
   3.198      also have "... = ({x} <#> H1) <#> {inv x} <#> ({x} <#>  H \<inter> K1 <#> {inv x})"
   3.199 @@ -418,31 +418,31 @@
   3.200    shows " (H\<inter>K) \<inter> (H1<#>(H\<inter>K1)) = (H1\<inter>K)<#>(H\<inter>K1)"
   3.201  proof
   3.202    have all_inclG : "H \<subseteq> carrier G" "H1 \<subseteq> carrier G" "K \<subseteq> carrier G" "K1 \<subseteq> carrier G"
   3.203 -    using assms subgroup_imp_subset normal_imp_subgroup incl_subgroup apply blast+.
   3.204 +    using assms subgroup.subset normal_imp_subgroup incl_subgroup apply blast+.
   3.205    show "H \<inter> K \<inter> (H1 <#> H \<inter> K1) \<subseteq> H1 \<inter> K <#> H \<inter> K1"
   3.206    proof
   3.207      fix x assume x_def : "x \<in> (H \<inter> K) \<inter> (H1 <#> (H \<inter> K1))"
   3.208      from x_def have x_incl : "x \<in> H" "x \<in> K" "x \<in> (H1 <#> (H \<inter> K1))" by auto
   3.209      then obtain h1 hk1 where h1hk1_def : "h1 \<in> H1" "hk1 \<in> H \<inter> K1" "h1 \<otimes> hk1 = x"
   3.210        using assms unfolding set_mult_def by blast
   3.211 -    hence "hk1 \<in> H \<inter> K" using subgroup_imp_subset[OF normal_imp_subgroup[OF assms(4)]] by auto
   3.212 +    hence "hk1 \<in> H \<inter> K" using subgroup.subset[OF normal_imp_subgroup[OF assms(4)]] by auto
   3.213      hence "inv hk1 \<in> H \<inter> K" using subgroup.m_inv_closed[OF subgroups_Inter_pair] assms by auto
   3.214      moreover have "h1 \<otimes> hk1 \<in> H \<inter> K" using x_incl h1hk1_def by auto
   3.215      ultimately have "h1 \<otimes> hk1 \<otimes> inv hk1 \<in> H \<inter> K"
   3.216        using subgroup.m_closed[OF subgroups_Inter_pair] assms by auto
   3.217 -    hence "h1 \<in> H \<inter> K" using  h1hk1_def assms subgroup_imp_subset incl_subgroup normal_imp_subgroup
   3.218 +    hence "h1 \<in> H \<inter> K" using  h1hk1_def assms subgroup.subset incl_subgroup normal_imp_subgroup
   3.219        by (metis Int_iff contra_subsetD inv_solve_right m_closed)
   3.220      hence "h1 \<in> H1 \<inter> H \<inter> K" using h1hk1_def by auto
   3.221 -    hence "h1 \<in> H1 \<inter> K" using subgroup_imp_subset[OF normal_imp_subgroup[OF assms(2)]] by auto
   3.222 +    hence "h1 \<in> H1 \<inter> K" using subgroup.subset[OF normal_imp_subgroup[OF assms(2)]] by auto
   3.223      hence "h1 \<otimes> hk1 \<in> (H1\<inter>K)<#>(H\<inter>K1)"
   3.224        using h1hk1_def unfolding set_mult_def by auto
   3.225      thus " x \<in> (H1\<inter>K)<#>(H\<inter>K1)" using h1hk1_def x_def by auto
   3.226    qed
   3.227    show "H1 \<inter> K <#> H \<inter> K1 \<subseteq> H \<inter> K \<inter> (H1 <#> H \<inter> K1)"
   3.228    proof-
   3.229 -    have "H1 \<inter> K \<subseteq> H \<inter> K" using subgroup_imp_subset[OF normal_imp_subgroup[OF assms(2)]] by auto
   3.230 +    have "H1 \<inter> K \<subseteq> H \<inter> K" using subgroup.subset[OF normal_imp_subgroup[OF assms(2)]] by auto
   3.231      moreover have "H \<inter> K1 \<subseteq> H \<inter> K"
   3.232 -      using subgroup_imp_subset[OF normal_imp_subgroup[OF assms(4)]] by auto
   3.233 +      using subgroup.subset[OF normal_imp_subgroup[OF assms(4)]] by auto
   3.234      ultimately have "H1 \<inter> K <#> H \<inter> K1 \<subseteq> H \<inter> K" unfolding set_mult_def
   3.235        using subgroup.m_closed[OF subgroups_Inter_pair [OF assms(1)assms(3)]] by blast
   3.236      moreover have "H1 \<inter> K \<subseteq> H1" by auto
   3.237 @@ -459,7 +459,7 @@
   3.238    shows "(H1<#>(H\<inter>K1)) \<lhd> G\<lparr>carrier:=(H1<#>(H\<inter>K))\<rparr>"
   3.239  proof-
   3.240    have all_inclG : "H \<subseteq> carrier G" "H1 \<subseteq> carrier G" "K \<subseteq> carrier G" "K1 \<subseteq> carrier G"
   3.241 -    using assms subgroup_imp_subset normal_imp_subgroup incl_subgroup apply blast+.
   3.242 +    using assms subgroup.subset normal_imp_subgroup incl_subgroup apply blast+.
   3.243    have subH1:"subgroup (H1 <#> H \<inter> K) (G\<lparr>carrier := H\<rparr>)" 
   3.244      using mult_norm_sub_in_sub[OF assms(2)subgroup_incl[OF subgroups_Inter_pair[OF assms(1)assms(3)]
   3.245            assms(1)]] assms by auto
   3.246 @@ -469,13 +469,13 @@
   3.247      using mult_norm_sub_in_sub[OF assms(2) subgroup_incl[OF subgroups_Inter_pair[OF
   3.248             assms(1) incl_subgroup[OF assms(3)normal_imp_subgroup[OF assms(4)]]]]] assms by auto
   3.249    hence "(H\<inter>K1) \<subseteq> (H\<inter>K)"
   3.250 -    using assms subgroup_imp_subset normal_imp_subgroup monoid.cases_scheme
   3.251 +    using assms subgroup.subset normal_imp_subgroup monoid.cases_scheme
   3.252      by (metis inf.mono  partial_object.simps(1) partial_object.update_convs(1) subset_refl)
   3.253 -  hence incl:"(H1<#>(H\<inter>K1)) \<subseteq> H1<#>(H\<inter>K)" using assms subgroup_imp_subset normal_imp_subgroup
   3.254 +  hence incl:"(H1<#>(H\<inter>K1)) \<subseteq> H1<#>(H\<inter>K)" using assms subgroup.subset normal_imp_subgroup
   3.255      unfolding set_mult_def by blast
   3.256    hence "subgroup (H1 <#> H \<inter> K1) (G\<lparr>carrier := (H1<#>(H\<inter>K))\<rparr>)"
   3.257      using assms subgroup_incl[OF incl_subgroup[OF assms(1)subH2]incl_subgroup[OF assms(1)
   3.258 -          subH1]] normal_imp_subgroup subgroup_imp_subset unfolding set_mult_def by blast
   3.259 +          subH1]] normal_imp_subgroup subgroup.subset unfolding set_mult_def by blast
   3.260    moreover have " (\<And> x. x\<in>carrier (G\<lparr>carrier := H1 <#> H \<inter> K\<rparr>) \<Longrightarrow>
   3.261          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))"
   3.262    proof-
   3.263 @@ -483,14 +483,14 @@
   3.264      hence x_def : "x \<in> H1 <#> H \<inter> K" by simp
   3.265      from this obtain h1 hk where h1hk_def :"h1 \<in> H1" "hk \<in> H \<inter> K" "h1 \<otimes> hk = x"
   3.266        unfolding set_mult_def by blast
   3.267 -    have xH : "x \<in> H" using subgroup_imp_subset[OF subH1] using x_def by auto
   3.268 +    have xH : "x \<in> H" using subgroup.subset[OF subH1] using x_def by auto
   3.269      hence allG : "h1 \<in> carrier G" "hk \<in> carrier G" "x \<in> carrier G"
   3.270 -      using assms subgroup_imp_subset h1hk_def normal_imp_subgroup incl_subgroup apply blast+.
   3.271 +      using assms subgroup.subset h1hk_def normal_imp_subgroup incl_subgroup apply blast+.
   3.272      hence "x <#\<^bsub>G\<lparr>carrier := H1 <#> H\<inter>K\<rparr>\<^esub> (H1 <#> H\<inter>K1) =h1 \<otimes> hk <# (H1 <#> H\<inter>K1)"
   3.273 -      using subgroup_set_mult_equality subgroup_imp_subset xH h1hk_def by (simp add: l_coset_def)
   3.274 +      using subgroup_set_mult_equality subgroup.subset xH h1hk_def by (simp add: l_coset_def)
   3.275      also have "... = h1 <# (hk <# (H1 <#> H\<inter>K1))"
   3.276 -      using lcos_m_assoc[OF subgroup_imp_subset[OF incl_subgroup[OF assms(1) subH1]]allG(1)allG(2)]
   3.277 -      by (metis allG(1) allG(2) assms(1) incl_subgroup lcos_m_assoc subH2 subgroup_imp_subset)
   3.278 +      using lcos_m_assoc[OF subgroup.subset[OF incl_subgroup[OF assms(1) subH1]]allG(1)allG(2)]
   3.279 +      by (metis allG(1) allG(2) assms(1) incl_subgroup lcos_m_assoc subH2 subgroup.subset)
   3.280      also have "... = h1 <# (hk <# H1 <#> H\<inter>K1)"
   3.281        using set_mult_assoc all_inclG allG by (simp add: l_coset_eq_set_mult inf.coboundedI1)
   3.282      also have "... = h1 <# (hk <# H1 #> \<one> <#> H\<inter>K1 #> \<one>)"
   3.283 @@ -504,18 +504,18 @@
   3.284        using rcos_assoc_lcos allG all_inclG
   3.285        by (smt inf_le1 inv_closed l_coset_subset_G r_coset_subset_G setmult_rcos_assoc subset_trans)
   3.286      moreover have "H \<subseteq>  normalizer G H1"
   3.287 -      using assms h1hk_def subgroup_imp_subset[OF normal_imp_subgroup_normalizer] by simp
   3.288 +      using assms h1hk_def subgroup.subset[OF normal_imp_subgroup_normalizer] by simp
   3.289      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}"
   3.290        using all_inclG assms unfolding normalizer_def stabilizer_def by auto
   3.291      hence "\<And>g. g \<in> H \<Longrightarrow>  g <# H1 #> inv g = H1" using all_inclG by simp
   3.292      hence "(hk <# H1 #> inv hk) = H1" using h1hk_def all_inclG by simp
   3.293      moreover have "H\<inter>K \<subseteq> normalizer G (H\<inter>K1)"
   3.294        using normal_inter[OF assms(3)assms(1)assms(4)] assms subgroups_Inter_pair
   3.295 -            subgroup_imp_subset[OF normal_imp_subgroup_normalizer] by (simp add: inf_commute)
   3.296 +            subgroup.subset[OF normal_imp_subgroup_normalizer] by (simp add: inf_commute)
   3.297      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}"
   3.298        using all_inclG assms unfolding normalizer_def stabilizer_def by auto
   3.299      hence "\<And>g. g \<in> H\<inter>K \<Longrightarrow>  g <# (H\<inter>K1) #> inv g = H\<inter>K1"
   3.300 -      using subgroup_imp_subset[OF subgroups_Inter_pair[OF assms(1) incl_subgroup[OF
   3.301 +      using subgroup.subset[OF subgroups_Inter_pair[OF assms(1) incl_subgroup[OF
   3.302              assms(3)normal_imp_subgroup[OF assms(4)]]]] by auto
   3.303      hence "(hk <# H\<inter>K1 #> inv hk) = H\<inter>K1" using h1hk_def by simp
   3.304      ultimately have "x <#\<^bsub>G\<lparr>carrier := H1 <#> H \<inter> K\<rparr>\<^esub> (H1 <#> H \<inter> K1) = h1 <#(H1 <#> (H \<inter> K1)#> hk)"
   3.305 @@ -529,7 +529,7 @@
   3.306      finally have eq1 : "x <#\<^bsub>G\<lparr>carrier := H1 <#> H \<inter> K\<rparr>\<^esub> (H1 <#> H \<inter> K1) = H1 <#> (H \<inter> K1) #> hk"
   3.307        by (simp add: allG(2) all_inclG inf.coboundedI2 setmult_rcos_assoc)
   3.308      have "H1 <#> H \<inter> K1 #>\<^bsub>G\<lparr>carrier := H1 <#> H \<inter> K\<rparr>\<^esub> x = H1 <#> H \<inter> K1 #> (h1 \<otimes> hk)"
   3.309 -      using subgroup_set_mult_equality subgroup_imp_subset xH h1hk_def by (simp add: r_coset_def)
   3.310 +      using subgroup_set_mult_equality subgroup.subset xH h1hk_def by (simp add: r_coset_def)
   3.311      also have "... = H1 <#> H \<inter> K1 #> h1 #> hk"
   3.312        using coset_mult_assoc by (simp add: allG all_inclG inf.coboundedI2 setmult_subset_G)
   3.313      also have"... =  H \<inter> K1 <#> H1 #> h1 #> hk"
   3.314 @@ -565,18 +565,18 @@
   3.315    have H_simp: "N<#>N1 = H1<#> (H\<inter>K)"
   3.316    proof-
   3.317      have H1_incl_G : "H1 \<subseteq> carrier G"
   3.318 -      using assms normal_imp_subgroup incl_subgroup subgroup_imp_subset by blast
   3.319 +      using assms normal_imp_subgroup incl_subgroup subgroup.subset by blast
   3.320      have K1_incl_G :"K1 \<subseteq> carrier G"
   3.321 -      using assms normal_imp_subgroup incl_subgroup subgroup_imp_subset by blast
   3.322 +      using assms normal_imp_subgroup incl_subgroup subgroup.subset by blast
   3.323      have "N<#>N1=  (H\<inter>K)<#> (H1<#>(H\<inter>K1))" by (auto simp add: N_def N1_def)
   3.324      also have "... = ((H\<inter>K)<#>H1) <#>(H\<inter>K1)"
   3.325        using set_mult_assoc[where ?M = "H\<inter>K"] K1_incl_G H1_incl_G assms
   3.326 -      by (simp add: inf.coboundedI2 subgroup_imp_subset)
   3.327 +      by (simp add: inf.coboundedI2 subgroup.subset)
   3.328      also have "... = (H1<#>(H\<inter>K))<#>(H\<inter>K1)" 
   3.329        using commut_normal_subgroup assms subgroup_incl subgroups_Inter_pair by auto
   3.330      also have "... =  H1 <#> ((H\<inter>K)<#>(H\<inter>K1))"
   3.331        using set_mult_assoc K1_incl_G H1_incl_G assms
   3.332 -      by (simp add: inf.coboundedI2 subgroup_imp_subset)
   3.333 +      by (simp add: inf.coboundedI2 subgroup.subset)
   3.334      also have " ((H\<inter>K)<#>(H\<inter>K1)) = (H\<inter>K)"
   3.335      proof (intro set_mult_subgroup_idem[where ?H = "H\<inter>K" and ?N="H\<inter>K1",
   3.336               OF subgroups_Inter_pair[OF assms(1) assms(3)]])
     4.1 --- a/src/HOL/Analysis/Infinite_Products.thy	Thu Jun 14 17:50:23 2018 +0200
     4.2 +++ b/src/HOL/Analysis/Infinite_Products.thy	Fri Jun 15 12:18:06 2018 +0100
     4.3 @@ -98,6 +98,10 @@
     4.4      using LIMSEQ_unique by blast
     4.5  qed
     4.6  
     4.7 +lemma raw_has_prod_Suc: 
     4.8 +  "raw_has_prod f (Suc M) a \<longleftrightarrow> raw_has_prod (\<lambda>n. f (Suc n)) M a"
     4.9 +  unfolding raw_has_prod_def by auto
    4.10 +
    4.11  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))"
    4.12    by (simp add: has_prod_def)
    4.13        
    4.14 @@ -1203,21 +1207,37 @@
    4.15  qed
    4.16  
    4.17  lemma convergent_prod_Suc_iff:
    4.18 -  assumes "\<And>k. f k \<noteq> 0" shows "convergent_prod (\<lambda>n. f (Suc n)) = convergent_prod f"
    4.19 +  shows "convergent_prod (\<lambda>n. f (Suc n)) = convergent_prod f"
    4.20  proof
    4.21    assume "convergent_prod f"
    4.22 -  then have "f has_prod prodinf f"
    4.23 -    by (rule convergent_prod_has_prod)
    4.24 -  moreover have "prodinf f \<noteq> 0"
    4.25 -    by (simp add: \<open>convergent_prod f\<close> assms prodinf_nonzero)
    4.26 -  ultimately have "(\<lambda>n. f (Suc n)) has_prod (prodinf f * inverse (f 0))"
    4.27 -    by (simp add: has_prod_Suc_iff inverse_eq_divide assms)
    4.28 -  then show "convergent_prod (\<lambda>n. f (Suc n))"
    4.29 -    using has_prod_iff by blast
    4.30 +  then obtain M L where M_nz:"\<forall>n\<ge>M. f n \<noteq> 0" and 
    4.31 +        M_L:"(\<lambda>n. \<Prod>i\<le>n. f (i + M)) \<longlonglongrightarrow> L" and "L \<noteq> 0" 
    4.32 +    unfolding convergent_prod_altdef by auto
    4.33 +  have "(\<lambda>n. \<Prod>i\<le>n. f (Suc (i + M))) \<longlonglongrightarrow> L / f M"
    4.34 +  proof -
    4.35 +    have "(\<lambda>n. \<Prod>i\<in>{0..Suc n}. f (i + M)) \<longlonglongrightarrow> L"
    4.36 +      using M_L 
    4.37 +      apply (subst (asm) LIMSEQ_Suc_iff[symmetric]) 
    4.38 +      using atLeast0AtMost by auto
    4.39 +    then have "(\<lambda>n. f M * (\<Prod>i\<in>{0..n}. f (Suc (i + M)))) \<longlonglongrightarrow> L"
    4.40 +      apply (subst (asm) prod.atLeast0_atMost_Suc_shift)
    4.41 +      by simp
    4.42 +    then have "(\<lambda>n. (\<Prod>i\<in>{0..n}. f (Suc (i + M)))) \<longlonglongrightarrow> L/f M"
    4.43 +      apply (drule_tac tendsto_divide)
    4.44 +      using M_nz[rule_format,of M,simplified] by auto
    4.45 +    then show ?thesis unfolding atLeast0AtMost .
    4.46 +  qed
    4.47 +  then show "convergent_prod (\<lambda>n. f (Suc n))" unfolding convergent_prod_altdef
    4.48 +    apply (rule_tac exI[where x=M])
    4.49 +    apply (rule_tac exI[where x="L/f M"])
    4.50 +    using M_nz \<open>L\<noteq>0\<close> by auto
    4.51  next
    4.52    assume "convergent_prod (\<lambda>n. f (Suc n))"
    4.53 -  then show "convergent_prod f"
    4.54 -    using assms convergent_prod_def raw_has_prod_Suc_iff by blast
    4.55 +  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"
    4.56 +    unfolding convergent_prod_altdef by auto
    4.57 +  then show "convergent_prod f" unfolding convergent_prod_altdef
    4.58 +    apply (rule_tac exI[where x="Suc M"])
    4.59 +    using Suc_le_D by auto
    4.60  qed
    4.61  
    4.62  lemma raw_has_prod_inverse: 
    4.63 @@ -1256,6 +1276,26 @@
    4.64  lemma prodinf_inverse: "convergent_prod f \<Longrightarrow> (\<Prod>n. inverse (f n)) = inverse (\<Prod>n. f n)"
    4.65    by (intro has_prod_unique [symmetric] has_prod_inverse convergent_prod_has_prod)
    4.66  
    4.67 +lemma has_prod_Suc_imp: 
    4.68 +  assumes "(\<lambda>n. f (Suc n)) has_prod a"
    4.69 +  shows "f has_prod (a * f 0)"
    4.70 +proof -
    4.71 +  have "f has_prod (a * f 0)" when "raw_has_prod (\<lambda>n. f (Suc n)) 0 a" 
    4.72 +    apply (cases "f 0=0")
    4.73 +    using that unfolding has_prod_def raw_has_prod_Suc 
    4.74 +    by (auto simp add: raw_has_prod_Suc_iff)
    4.75 +  moreover have "f has_prod (a * f 0)" when 
    4.76 +    "(\<exists>i q. a = 0 \<and> f (Suc i) = 0 \<and> raw_has_prod (\<lambda>n. f (Suc n)) (Suc i) q)" 
    4.77 +  proof -
    4.78 +    from that 
    4.79 +    obtain i q where "a = 0" "f (Suc i) = 0" "raw_has_prod (\<lambda>n. f (Suc n)) (Suc i) q"
    4.80 +      by auto
    4.81 +    then show ?thesis unfolding has_prod_def 
    4.82 +      by (auto intro!:exI[where x="Suc i"] simp:raw_has_prod_Suc)
    4.83 +  qed
    4.84 +  ultimately show "f has_prod (a * f 0)" using assms unfolding has_prod_def by auto
    4.85 +qed
    4.86 +
    4.87  lemma has_prod_iff_shift: 
    4.88    assumes "\<And>i. i < n \<Longrightarrow> f i \<noteq> 0"
    4.89    shows "(\<lambda>i. f (i + n)) has_prod a \<longleftrightarrow> f has_prod (a * (\<Prod>i<n. f i))"
    4.90 @@ -1373,6 +1413,24 @@
    4.91  
    4.92  end
    4.93  
    4.94 +lemma exp_suminf_prodinf_real:
    4.95 +  fixes f :: "nat \<Rightarrow> real"
    4.96 +  assumes ge0:"\<And>n. f n \<ge> 0" and ac: "abs_convergent_prod (\<lambda>n. exp (f n))"
    4.97 +  shows "prodinf (\<lambda>i. exp (f i)) = exp (suminf f)"
    4.98 +proof -
    4.99 +  have "summable f" 
   4.100 +    using ac unfolding abs_convergent_prod_conv_summable
   4.101 +  proof (elim summable_comparison_test')
   4.102 +    fix n
   4.103 +    show "norm (f n) \<le> norm (exp (f n) - 1)" 
   4.104 +      using ge0[of n] 
   4.105 +      by (metis abs_of_nonneg add.commute diff_add_cancel diff_ge_0_iff_ge exp_ge_add_one_self 
   4.106 +          exp_le_cancel_iff one_le_exp_iff real_norm_def)
   4.107 +  qed
   4.108 +  then show ?thesis
   4.109 +    by (simp add: prodinf_exp)
   4.110 +qed
   4.111 +
   4.112  lemma has_prod_imp_sums_ln_real: 
   4.113    fixes f :: "nat \<Rightarrow> real"
   4.114    assumes "raw_has_prod f 0 p" and 0: "\<And>x. f x > 0"