type class generalisations; some work on infinite products
authorpaulson <lp15@cam.ac.uk>
Wed May 02 12:47:56 2018 +0100 (14 months ago)
changeset 68064b249fab48c76
parent 68051 68def9274939
child 68065 d2daeef3ce47
type class generalisations; some work on infinite products
src/HOL/Analysis/Infinite_Products.thy
src/HOL/Limits.thy
src/HOL/Series.thy
src/HOL/Set_Interval.thy
src/HOL/Topological_Spaces.thy
     1.1 --- a/src/HOL/Analysis/Infinite_Products.thy	Fri Apr 27 12:43:05 2018 +0100
     1.2 +++ b/src/HOL/Analysis/Infinite_Products.thy	Wed May 02 12:47:56 2018 +0100
     1.3 @@ -1,6 +1,5 @@
     1.4 -(*
     1.5 -  File:      HOL/Analysis/Infinite_Product.thy
     1.6 -  Author:    Manuel Eberl
     1.7 +(*File:      HOL/Analysis/Infinite_Product.thy
     1.8 +  Author:    Manuel Eberl & LC Paulson
     1.9  
    1.10    Basic results about convergence and absolute convergence of infinite products
    1.11    and their connection to summability.
    1.12 @@ -9,7 +8,7 @@
    1.13  theory Infinite_Products
    1.14    imports Complex_Main
    1.15  begin
    1.16 -
    1.17 +    
    1.18  lemma sum_le_prod:
    1.19    fixes f :: "'a \<Rightarrow> 'b :: linordered_semidom"
    1.20    assumes "\<And>x. x \<in> A \<Longrightarrow> f x \<ge> 0"
    1.21 @@ -51,8 +50,27 @@
    1.22      by (rule tendsto_eq_intros refl | simp)+
    1.23  qed auto
    1.24  
    1.25 +definition gen_has_prod :: "[nat \<Rightarrow> 'a::{t2_space, comm_semiring_1}, nat, 'a] \<Rightarrow> bool" 
    1.26 +  where "gen_has_prod f M p \<equiv> (\<lambda>n. \<Prod>i\<le>n. f (i+M)) \<longlonglongrightarrow> p \<and> p \<noteq> 0"
    1.27 +
    1.28 +text\<open>The nonzero and zero cases, as in \emph{Complex Analysis} by Joseph Bak and Donald J.Newman, page 241\<close>
    1.29 +definition has_prod :: "(nat \<Rightarrow> 'a::{t2_space, comm_semiring_1}) \<Rightarrow> 'a \<Rightarrow> bool" (infixr "has'_prod" 80)
    1.30 +  where "f has_prod p \<equiv> gen_has_prod f 0 p \<or> (\<exists>i q. p = 0 \<and> f i = 0 \<and> gen_has_prod f (Suc i) q)"
    1.31 +
    1.32  definition convergent_prod :: "(nat \<Rightarrow> 'a :: {t2_space,comm_semiring_1}) \<Rightarrow> bool" where
    1.33 -  "convergent_prod f \<longleftrightarrow> (\<exists>M L. (\<lambda>n. \<Prod>i\<le>n. f (i+M)) \<longlonglongrightarrow> L \<and> L \<noteq> 0)"
    1.34 +  "convergent_prod f \<equiv> \<exists>M p. gen_has_prod f M p"
    1.35 +
    1.36 +definition prodinf :: "(nat \<Rightarrow> 'a::{t2_space, comm_semiring_1}) \<Rightarrow> 'a"
    1.37 +    (binder "\<Prod>" 10)
    1.38 +  where "prodinf f = (THE p. f has_prod p)"
    1.39 +
    1.40 +lemmas prod_defs = gen_has_prod_def has_prod_def convergent_prod_def prodinf_def
    1.41 +
    1.42 +lemma has_prod_subst[trans]: "f = g \<Longrightarrow> g has_prod z \<Longrightarrow> f has_prod z"
    1.43 +  by simp
    1.44 +
    1.45 +lemma has_prod_cong: "(\<And>n. f n = g n) \<Longrightarrow> f has_prod c \<longleftrightarrow> g has_prod c"
    1.46 +  by presburger
    1.47  
    1.48  lemma convergent_prod_altdef:
    1.49    fixes f :: "nat \<Rightarrow> 'a :: {t2_space,comm_semiring_1}"
    1.50 @@ -60,7 +78,7 @@
    1.51  proof
    1.52    assume "convergent_prod f"
    1.53    then obtain M L where *: "(\<lambda>n. \<Prod>i\<le>n. f (i+M)) \<longlonglongrightarrow> L" "L \<noteq> 0"
    1.54 -    by (auto simp: convergent_prod_def)
    1.55 +    by (auto simp: prod_defs)
    1.56    have "f i \<noteq> 0" if "i \<ge> M" for i
    1.57    proof
    1.58      assume "f i = 0"
    1.59 @@ -79,7 +97,7 @@
    1.60    qed
    1.61    with * show "(\<exists>M L. (\<forall>n\<ge>M. f n \<noteq> 0) \<and> (\<lambda>n. \<Prod>i\<le>n. f (i+M)) \<longlonglongrightarrow> L \<and> L \<noteq> 0)" 
    1.62      by blast
    1.63 -qed (auto simp: convergent_prod_def)
    1.64 +qed (auto simp: prod_defs)
    1.65  
    1.66  definition abs_convergent_prod :: "(nat \<Rightarrow> _) \<Rightarrow> bool" where
    1.67    "abs_convergent_prod f \<longleftrightarrow> convergent_prod (\<lambda>i. 1 + norm (f i - 1))"
    1.68 @@ -101,12 +119,12 @@
    1.69      qed
    1.70    qed (use L in simp_all)
    1.71    hence "L \<noteq> 0" by auto
    1.72 -  with L show ?thesis unfolding abs_convergent_prod_def convergent_prod_def
    1.73 +  with L show ?thesis unfolding abs_convergent_prod_def prod_defs
    1.74      by (intro exI[of _ "0::nat"] exI[of _ L]) auto
    1.75  qed
    1.76  
    1.77  lemma
    1.78 -  fixes f :: "nat \<Rightarrow> 'a :: {real_normed_div_algebra,idom}"
    1.79 +  fixes f :: "nat \<Rightarrow> 'a :: {topological_semigroup_mult,t2_space,idom}"
    1.80    assumes "convergent_prod f"
    1.81    shows   convergent_prod_imp_convergent: "convergent (\<lambda>n. \<Prod>i\<le>n. f i)"
    1.82      and   convergent_prod_to_zero_iff:    "(\<lambda>n. \<Prod>i\<le>n. f i) \<longlonglongrightarrow> 0 \<longleftrightarrow> (\<exists>i. f i = 0)"
    1.83 @@ -141,8 +159,30 @@
    1.84    qed
    1.85  qed
    1.86  
    1.87 +lemma convergent_prod_iff_nz_lim:
    1.88 +  fixes f :: "nat \<Rightarrow> 'a :: {topological_semigroup_mult,t2_space,idom}"
    1.89 +  assumes "\<And>i. f i \<noteq> 0"
    1.90 +  shows "convergent_prod f \<longleftrightarrow> (\<exists>L. (\<lambda>n. \<Prod>i\<le>n. f i) \<longlonglongrightarrow> L \<and> L \<noteq> 0)"
    1.91 +    (is "?lhs \<longleftrightarrow> ?rhs")
    1.92 +proof
    1.93 +  assume ?lhs then show ?rhs
    1.94 +    using assms convergentD convergent_prod_imp_convergent convergent_prod_to_zero_iff by blast
    1.95 +next
    1.96 +  assume ?rhs then show ?lhs
    1.97 +    unfolding prod_defs
    1.98 +    by (rule_tac x="0" in exI) (auto simp: )
    1.99 +qed
   1.100 +
   1.101 +lemma convergent_prod_iff_convergent: 
   1.102 +  fixes f :: "nat \<Rightarrow> 'a :: {topological_semigroup_mult,t2_space,idom}"
   1.103 +  assumes "\<And>i. f i \<noteq> 0"
   1.104 +  shows "convergent_prod f \<longleftrightarrow> convergent (\<lambda>n. \<Prod>i\<le>n. f i) \<and> lim (\<lambda>n. \<Prod>i\<le>n. f i) \<noteq> 0"
   1.105 +  by (force simp add: convergent_prod_iff_nz_lim assms convergent_def limI)
   1.106 +
   1.107 +
   1.108  lemma abs_convergent_prod_altdef:
   1.109 -  "abs_convergent_prod f \<longleftrightarrow> convergent (\<lambda>n. \<Prod>i\<le>n. 1 + norm (f i - 1))"
   1.110 +  fixes f :: "nat \<Rightarrow> 'a :: {one,real_normed_vector}"
   1.111 +  shows  "abs_convergent_prod f \<longleftrightarrow> convergent (\<lambda>n. \<Prod>i\<le>n. 1 + norm (f i - 1))"
   1.112  proof
   1.113    assume "abs_convergent_prod f"
   1.114    thus "convergent (\<lambda>n. \<Prod>i\<le>n. 1 + norm (f i - 1))"
   1.115 @@ -180,7 +220,7 @@
   1.116    also have "norm (1::'a) = 1" by simp
   1.117    also note insert.IH
   1.118    also have "(\<Prod>n\<in>A. 1 + norm (f n)) - 1 + norm (f x) * (\<Prod>x\<in>A. 1 + norm (f x)) =
   1.119 -               (\<Prod>n\<in>insert x A. 1 + norm (f n)) - 1"
   1.120 +             (\<Prod>n\<in>insert x A. 1 + norm (f n)) - 1"
   1.121      using insert.hyps by (simp add: algebra_simps)
   1.122    finally show ?case by - (simp_all add: mult_left_mono)
   1.123  qed simp_all
   1.124 @@ -297,8 +337,9 @@
   1.125    shows   "convergent_prod f"
   1.126  proof -
   1.127    from assms obtain M L where "(\<lambda>n. \<Prod>k\<le>n. f (k + (M + m))) \<longlonglongrightarrow> L" "L \<noteq> 0"
   1.128 -    by (auto simp: convergent_prod_def add.assoc)
   1.129 -  thus "convergent_prod f" unfolding convergent_prod_def by blast
   1.130 +    by (auto simp: prod_defs add.assoc)
   1.131 +  thus "convergent_prod f" 
   1.132 +    unfolding prod_defs by blast
   1.133  qed
   1.134  
   1.135  lemma abs_convergent_prod_offset:
   1.136 @@ -334,7 +375,8 @@
   1.137      by (intro tendsto_divide tendsto_const) auto
   1.138    hence "(\<lambda>n. \<Prod>k\<le>n. f (k + M + m)) \<longlonglongrightarrow> L / C" by simp
   1.139    moreover from \<open>L \<noteq> 0\<close> have "L / C \<noteq> 0" by simp
   1.140 -  ultimately show ?thesis unfolding convergent_prod_def by blast
   1.141 +  ultimately show ?thesis 
   1.142 +    unfolding prod_defs by blast
   1.143  qed
   1.144  
   1.145  lemma abs_convergent_prod_ignore_initial_segment:
   1.146 @@ -343,11 +385,6 @@
   1.147    using assms unfolding abs_convergent_prod_def 
   1.148    by (rule convergent_prod_ignore_initial_segment)
   1.149  
   1.150 -lemma summable_LIMSEQ': 
   1.151 -  assumes "summable (f::nat\<Rightarrow>'a::{t2_space,comm_monoid_add})"
   1.152 -  shows   "(\<lambda>n. \<Sum>i\<le>n. f i) \<longlonglongrightarrow> suminf f"
   1.153 -  using assms sums_def_le by blast
   1.154 -
   1.155  lemma abs_convergent_prod_imp_convergent_prod:
   1.156    fixes f :: "nat \<Rightarrow> 'a :: {real_normed_div_algebra,complete_space,comm_ring_1}"
   1.157    assumes "abs_convergent_prod f"
   1.158 @@ -473,7 +510,98 @@
   1.159      qed simp_all
   1.160      thus False by simp
   1.161    qed
   1.162 -  with L show ?thesis by (auto simp: convergent_prod_def)
   1.163 +  with L show ?thesis by (auto simp: prod_defs)
   1.164 +qed
   1.165 +
   1.166 +lemma convergent_prod_offset_0:
   1.167 +  fixes f :: "nat \<Rightarrow> 'a :: {idom,topological_semigroup_mult,t2_space}"
   1.168 +  assumes "convergent_prod f" "\<And>i. f i \<noteq> 0"
   1.169 +  shows "\<exists>p. gen_has_prod f 0 p"
   1.170 +  using assms
   1.171 +  unfolding convergent_prod_def
   1.172 +proof (clarsimp simp: prod_defs)
   1.173 +  fix M p
   1.174 +  assume "(\<lambda>n. \<Prod>i\<le>n. f (i + M)) \<longlonglongrightarrow> p" "p \<noteq> 0"
   1.175 +  then have "(\<lambda>n. prod f {..<M} * (\<Prod>i\<le>n. f (i + M))) \<longlonglongrightarrow> prod f {..<M} * p"
   1.176 +    by (metis tendsto_mult_left)
   1.177 +  moreover have "prod f {..<M} * (\<Prod>i\<le>n. f (i + M)) = prod f {..n+M}" for n
   1.178 +  proof -
   1.179 +    have "{..n+M} = {..<M} \<union> {M..n+M}"
   1.180 +      by auto
   1.181 +    then have "prod f {..n+M} = prod f {..<M} * prod f {M..n+M}"
   1.182 +      by simp (subst prod.union_disjoint; force)
   1.183 +    also have "... = prod f {..<M} * (\<Prod>i\<le>n. f (i + M))"
   1.184 +      by (metis (mono_tags, lifting) add.left_neutral atMost_atLeast0 prod_shift_bounds_cl_nat_ivl)
   1.185 +    finally show ?thesis by metis
   1.186 +  qed
   1.187 +  ultimately have "(\<lambda>n. prod f {..n}) \<longlonglongrightarrow> prod f {..<M} * p"
   1.188 +    by (auto intro: LIMSEQ_offset [where k=M])
   1.189 +  then show "\<exists>p. (\<lambda>n. prod f {..n}) \<longlonglongrightarrow> p \<and> p \<noteq> 0"
   1.190 +    using \<open>p \<noteq> 0\<close> assms
   1.191 +    by (rule_tac x="prod f {..<M} * p" in exI) auto
   1.192 +qed
   1.193 +
   1.194 +lemma prodinf_eq_lim:
   1.195 +  fixes f :: "nat \<Rightarrow> 'a :: {idom,topological_semigroup_mult,t2_space}"
   1.196 +  assumes "convergent_prod f" "\<And>i. f i \<noteq> 0"
   1.197 +  shows "prodinf f = lim (\<lambda>n. \<Prod>i\<le>n. f i)"
   1.198 +  using assms convergent_prod_offset_0 [OF assms]
   1.199 +  by (simp add: prod_defs lim_def) (metis (no_types) assms(1) convergent_prod_to_zero_iff)
   1.200 +
   1.201 +lemma has_prod_one[simp, intro]: "(\<lambda>n. 1) has_prod 1"
   1.202 +  unfolding prod_defs by auto
   1.203 +
   1.204 +lemma convergent_prod_one[simp, intro]: "convergent_prod (\<lambda>n. 1)"
   1.205 +  unfolding prod_defs by auto
   1.206 +
   1.207 +lemma prodinf_cong: "(\<And>n. f n = g n) \<Longrightarrow> prodinf f = prodinf g"
   1.208 +  by presburger
   1.209 +
   1.210 +lemma convergent_prod_cong:
   1.211 +  fixes f g :: "nat \<Rightarrow> 'a::{field,topological_semigroup_mult,t2_space}"
   1.212 +  assumes ev: "eventually (\<lambda>x. f x = g x) sequentially" and f: "\<And>i. f i \<noteq> 0" and g: "\<And>i. g i \<noteq> 0"
   1.213 +  shows "convergent_prod f = convergent_prod g"
   1.214 +proof -
   1.215 +  from assms obtain N where N: "\<forall>n\<ge>N. f n = g n"
   1.216 +    by (auto simp: eventually_at_top_linorder)
   1.217 +  define C where "C = (\<Prod>k<N. f k / g k)"
   1.218 +  with g have "C \<noteq> 0"
   1.219 +    by (simp add: f)
   1.220 +  have *: "eventually (\<lambda>n. prod f {..n} = C * prod g {..n}) sequentially"
   1.221 +    using eventually_ge_at_top[of N]
   1.222 +  proof eventually_elim
   1.223 +    case (elim n)
   1.224 +    then have "{..n} = {..<N} \<union> {N..n}"
   1.225 +      by auto
   1.226 +    also have "prod f ... = prod f {..<N} * prod f {N..n}"
   1.227 +      by (intro prod.union_disjoint) auto
   1.228 +    also from N have "prod f {N..n} = prod g {N..n}"
   1.229 +      by (intro prod.cong) simp_all
   1.230 +    also have "prod f {..<N} * prod g {N..n} = C * (prod g {..<N} * prod g {N..n})"
   1.231 +      unfolding C_def by (simp add: g prod_dividef)
   1.232 +    also have "prod g {..<N} * prod g {N..n} = prod g ({..<N} \<union> {N..n})"
   1.233 +      by (intro prod.union_disjoint [symmetric]) auto
   1.234 +    also from elim have "{..<N} \<union> {N..n} = {..n}"
   1.235 +      by auto                                                                    
   1.236 +    finally show "prod f {..n} = C * prod g {..n}" .
   1.237 +  qed
   1.238 +  then have cong: "convergent (\<lambda>n. prod f {..n}) = convergent (\<lambda>n. C * prod g {..n})"
   1.239 +    by (rule convergent_cong)
   1.240 +  show ?thesis
   1.241 +  proof
   1.242 +    assume cf: "convergent_prod f"
   1.243 +    then have "\<not> (\<lambda>n. prod g {..n}) \<longlonglongrightarrow> 0"
   1.244 +      using tendsto_mult_left * convergent_prod_to_zero_iff f filterlim_cong by fastforce
   1.245 +    then show "convergent_prod g"
   1.246 +      by (metis convergent_mult_const_iff \<open>C \<noteq> 0\<close> cong cf convergent_LIMSEQ_iff convergent_prod_iff_convergent convergent_prod_imp_convergent g)
   1.247 +  next
   1.248 +    assume cg: "convergent_prod g"
   1.249 +    have "\<exists>a. C * a \<noteq> 0 \<and> (\<lambda>n. prod g {..n}) \<longlonglongrightarrow> a"
   1.250 +      by (metis (no_types) \<open>C \<noteq> 0\<close> cg convergent_prod_iff_nz_lim divide_eq_0_iff g nonzero_mult_div_cancel_right)
   1.251 +    then show "convergent_prod f"
   1.252 +      using "*" tendsto_mult_left filterlim_cong
   1.253 +      by (fastforce simp add: convergent_prod_iff_nz_lim f)
   1.254 +  qed
   1.255  qed
   1.256  
   1.257  end
     2.1 --- a/src/HOL/Limits.thy	Fri Apr 27 12:43:05 2018 +0100
     2.2 +++ b/src/HOL/Limits.thy	Wed May 02 12:47:56 2018 +0100
     2.3 @@ -787,15 +787,32 @@
     2.4  lemmas tendsto_scaleR [tendsto_intros] =
     2.5    bounded_bilinear.tendsto [OF bounded_bilinear_scaleR]
     2.6  
     2.7 -lemmas tendsto_mult [tendsto_intros] =
     2.8 -  bounded_bilinear.tendsto [OF bounded_bilinear_mult]
     2.9 +
    2.10 +text\<open>Analogous type class for multiplication\<close>
    2.11 +class topological_semigroup_mult = topological_space + semigroup_mult +
    2.12 +  assumes tendsto_mult_Pair: "LIM x (nhds a \<times>\<^sub>F nhds b). fst x * snd x :> nhds (a * b)"
    2.13 +
    2.14 +instance real_normed_algebra < topological_semigroup_mult
    2.15 +proof
    2.16 +  fix a b :: 'a
    2.17 +  show "((\<lambda>x. fst x * snd x) \<longlongrightarrow> a * b) (nhds a \<times>\<^sub>F nhds b)"
    2.18 +    unfolding nhds_prod[symmetric]
    2.19 +    using tendsto_fst[OF filterlim_ident, of "(a,b)"] tendsto_snd[OF filterlim_ident, of "(a,b)"]
    2.20 +    by (simp add: bounded_bilinear.tendsto [OF bounded_bilinear_mult])
    2.21 +qed
    2.22 +
    2.23 +lemma tendsto_mult [tendsto_intros]:
    2.24 +  fixes a b :: "'a::topological_semigroup_mult"
    2.25 +  shows "(f \<longlongrightarrow> a) F \<Longrightarrow> (g \<longlongrightarrow> b) F \<Longrightarrow> ((\<lambda>x. f x * g x) \<longlongrightarrow> a * b) F"
    2.26 +  using filterlim_compose[OF tendsto_mult_Pair, of "\<lambda>x. (f x, g x)" a b F]
    2.27 +  by (simp add: nhds_prod[symmetric] tendsto_Pair)
    2.28  
    2.29  lemma tendsto_mult_left: "(f \<longlongrightarrow> l) F \<Longrightarrow> ((\<lambda>x. c * (f x)) \<longlongrightarrow> c * l) F"
    2.30 -  for c :: "'a::real_normed_algebra"
    2.31 +  for c :: "'a::topological_semigroup_mult"
    2.32    by (rule tendsto_mult [OF tendsto_const])
    2.33  
    2.34  lemma tendsto_mult_right: "(f \<longlongrightarrow> l) F \<Longrightarrow> ((\<lambda>x. (f x) * c) \<longlongrightarrow> l * c) F"
    2.35 -  for c :: "'a::real_normed_algebra"
    2.36 +  for c :: "'a::topological_semigroup_mult"
    2.37    by (rule tendsto_mult [OF _ tendsto_const])
    2.38  
    2.39  lemmas continuous_of_real [continuous_intros] =
    2.40 @@ -2069,14 +2086,14 @@
    2.41  qed
    2.42  
    2.43  lemma convergent_add:
    2.44 -  fixes X Y :: "nat \<Rightarrow> 'a::real_normed_vector"
    2.45 +  fixes X Y :: "nat \<Rightarrow> 'a::topological_monoid_add"
    2.46    assumes "convergent (\<lambda>n. X n)"
    2.47      and "convergent (\<lambda>n. Y n)"
    2.48    shows "convergent (\<lambda>n. X n + Y n)"
    2.49    using assms unfolding convergent_def by (blast intro: tendsto_add)
    2.50  
    2.51  lemma convergent_sum:
    2.52 -  fixes X :: "'a \<Rightarrow> nat \<Rightarrow> 'b::real_normed_vector"
    2.53 +  fixes X :: "'a \<Rightarrow> nat \<Rightarrow> 'b::topological_comm_monoid_add"
    2.54    shows "(\<And>i. i \<in> A \<Longrightarrow> convergent (\<lambda>n. X i n)) \<Longrightarrow> convergent (\<lambda>n. \<Sum>i\<in>A. X i n)"
    2.55    by (induct A rule: infinite_finite_induct) (simp_all add: convergent_const convergent_add)
    2.56  
    2.57 @@ -2091,16 +2108,13 @@
    2.58    shows "convergent (\<lambda>n. X n ** Y n)"
    2.59    using assms unfolding convergent_def by (blast intro: tendsto)
    2.60  
    2.61 -lemma convergent_minus_iff: "convergent X \<longleftrightarrow> convergent (\<lambda>n. - X n)"
    2.62 -  for X :: "nat \<Rightarrow> 'a::real_normed_vector"
    2.63 -  apply (simp add: convergent_def)
    2.64 -  apply (auto dest: tendsto_minus)
    2.65 -  apply (drule tendsto_minus)
    2.66 -  apply auto
    2.67 -  done
    2.68 +lemma convergent_minus_iff:
    2.69 +  fixes X :: "nat \<Rightarrow> 'a::topological_group_add"
    2.70 +  shows "convergent X \<longleftrightarrow> convergent (\<lambda>n. - X n)"
    2.71 +  unfolding convergent_def by (force dest: tendsto_minus)
    2.72  
    2.73  lemma convergent_diff:
    2.74 -  fixes X Y :: "nat \<Rightarrow> 'a::real_normed_vector"
    2.75 +  fixes X Y :: "nat \<Rightarrow> 'a::topological_group_add"
    2.76    assumes "convergent (\<lambda>n. X n)"
    2.77    assumes "convergent (\<lambda>n. Y n)"
    2.78    shows "convergent (\<lambda>n. X n - Y n)"
    2.79 @@ -2123,7 +2137,7 @@
    2.80    unfolding convergent_def by (blast intro!: tendsto_of_real)
    2.81  
    2.82  lemma convergent_add_const_iff:
    2.83 -  "convergent (\<lambda>n. c + f n :: 'a::real_normed_vector) \<longleftrightarrow> convergent f"
    2.84 +  "convergent (\<lambda>n. c + f n :: 'a::topological_ab_group_add) \<longleftrightarrow> convergent f"
    2.85  proof
    2.86    assume "convergent (\<lambda>n. c + f n)"
    2.87    from convergent_diff[OF this convergent_const[of c]] show "convergent f"
    2.88 @@ -2135,15 +2149,15 @@
    2.89  qed
    2.90  
    2.91  lemma convergent_add_const_right_iff:
    2.92 -  "convergent (\<lambda>n. f n + c :: 'a::real_normed_vector) \<longleftrightarrow> convergent f"
    2.93 +  "convergent (\<lambda>n. f n + c :: 'a::topological_ab_group_add) \<longleftrightarrow> convergent f"
    2.94    using convergent_add_const_iff[of c f] by (simp add: add_ac)
    2.95  
    2.96  lemma convergent_diff_const_right_iff:
    2.97 -  "convergent (\<lambda>n. f n - c :: 'a::real_normed_vector) \<longleftrightarrow> convergent f"
    2.98 +  "convergent (\<lambda>n. f n - c :: 'a::topological_ab_group_add) \<longleftrightarrow> convergent f"
    2.99    using convergent_add_const_right_iff[of f "-c"] by (simp add: add_ac)
   2.100  
   2.101  lemma convergent_mult:
   2.102 -  fixes X Y :: "nat \<Rightarrow> 'a::real_normed_field"
   2.103 +  fixes X Y :: "nat \<Rightarrow> 'a::topological_semigroup_mult"
   2.104    assumes "convergent (\<lambda>n. X n)"
   2.105      and "convergent (\<lambda>n. Y n)"
   2.106    shows "convergent (\<lambda>n. X n * Y n)"
   2.107 @@ -2151,7 +2165,7 @@
   2.108  
   2.109  lemma convergent_mult_const_iff:
   2.110    assumes "c \<noteq> 0"
   2.111 -  shows "convergent (\<lambda>n. c * f n :: 'a::real_normed_field) \<longleftrightarrow> convergent f"
   2.112 +  shows "convergent (\<lambda>n. c * f n :: 'a::{field,topological_semigroup_mult}) \<longleftrightarrow> convergent f"
   2.113  proof
   2.114    assume "convergent (\<lambda>n. c * f n)"
   2.115    from assms convergent_mult[OF this convergent_const[of "inverse c"]]
   2.116 @@ -2163,7 +2177,7 @@
   2.117  qed
   2.118  
   2.119  lemma convergent_mult_const_right_iff:
   2.120 -  fixes c :: "'a::real_normed_field"
   2.121 +  fixes c :: "'a::{field,topological_semigroup_mult}"
   2.122    assumes "c \<noteq> 0"
   2.123    shows "convergent (\<lambda>n. f n * c) \<longleftrightarrow> convergent f"
   2.124    using convergent_mult_const_iff[OF assms, of f] by (simp add: mult_ac)
     3.1 --- a/src/HOL/Series.thy	Fri Apr 27 12:43:05 2018 +0100
     3.2 +++ b/src/HOL/Series.thy	Wed May 02 12:47:56 2018 +0100
     3.3 @@ -170,6 +170,9 @@
     3.4  lemma summable_LIMSEQ: "summable f \<Longrightarrow> (\<lambda>n. \<Sum>i<n. f i) \<longlonglongrightarrow> suminf f"
     3.5    by (rule summable_sums [unfolded sums_def])
     3.6  
     3.7 +lemma summable_LIMSEQ': "summable f \<Longrightarrow> (\<lambda>n. \<Sum>i\<le>n. f i) \<longlonglongrightarrow> suminf f"
     3.8 +  using sums_def_le by blast
     3.9 +
    3.10  lemma sums_unique: "f sums s \<Longrightarrow> s = suminf f"
    3.11    by (metis limI suminf_eq_lim sums_def)
    3.12  
     4.1 --- a/src/HOL/Set_Interval.thy	Fri Apr 27 12:43:05 2018 +0100
     4.2 +++ b/src/HOL/Set_Interval.thy	Wed May 02 12:47:56 2018 +0100
     4.3 @@ -2459,6 +2459,17 @@
     4.4    finally show ?thesis .
     4.5  qed
     4.6  
     4.7 +lemma prod_nat_group: "(\<Prod>m<n::nat. prod f {m * k ..< m*k + k}) = prod f {..< n * k}"
     4.8 +proof (cases "k = 0")
     4.9 +  case True
    4.10 +  then show ?thesis
    4.11 +    by auto
    4.12 +next
    4.13 +  case False
    4.14 +  then show ?thesis 
    4.15 +    by (induct "n"; simp add: prod.atLeastLessThan_concat algebra_simps atLeast0_lessThan_Suc atLeast0LessThan[symmetric])
    4.16 +qed
    4.17 +
    4.18  
    4.19  subsection \<open>Efficient folding over intervals\<close>
    4.20  
     5.1 --- a/src/HOL/Topological_Spaces.thy	Fri Apr 27 12:43:05 2018 +0100
     5.2 +++ b/src/HOL/Topological_Spaces.thy	Wed May 02 12:47:56 2018 +0100
     5.3 @@ -3105,6 +3105,12 @@
     5.4  class open_uniformity = "open" + uniformity +
     5.5    assumes open_uniformity:
     5.6      "\<And>U. open U \<longleftrightarrow> (\<forall>x\<in>U. eventually (\<lambda>(x', y). x' = x \<longrightarrow> y \<in> U) uniformity)"
     5.7 +begin
     5.8 +
     5.9 +subclass topological_space
    5.10 +  by standard (force elim: eventually_mono eventually_elim2 simp: split_beta' open_uniformity)+
    5.11 +
    5.12 +end
    5.13  
    5.14  class uniform_space = open_uniformity +
    5.15    assumes uniformity_refl: "eventually E uniformity \<Longrightarrow> E (x, x)"
    5.16 @@ -3114,9 +3120,6 @@
    5.17          \<exists>D. eventually D uniformity \<and> (\<forall>x y z. D (x, y) \<longrightarrow> D (y, z) \<longrightarrow> E (x, z))"
    5.18  begin
    5.19  
    5.20 -subclass topological_space
    5.21 -  by standard (force elim: eventually_mono eventually_elim2 simp: split_beta' open_uniformity)+
    5.22 -
    5.23  lemma uniformity_bot: "uniformity \<noteq> bot"
    5.24    using uniformity_refl by auto
    5.25