Reorganised a huge proof
authorpaulson <lp15@cam.ac.uk>
Fri Jan 22 16:00:03 2016 +0000 (2016-01-22 ago)
changeset 62217527488dc8b90
parent 62216 5fb86150a579
child 62218 42202671777c
Reorganised a huge proof
src/HOL/IMP/Denotational.thy
src/HOL/Library/Product_Vector.thy
src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy
src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy
src/HOL/Nat.thy
src/HOL/Series.thy
src/HOL/Topological_Spaces.thy
     1.1 --- a/src/HOL/IMP/Denotational.thy	Wed Jan 20 20:19:05 2016 +0100
     1.2 +++ b/src/HOL/IMP/Denotational.thy	Fri Jan 22 16:00:03 2016 +0000
     1.3 @@ -105,7 +105,7 @@
     1.4        by(simp add: cont_def)
     1.5      also have "\<dots> = (f^^0){} \<union> \<dots>" by simp
     1.6      also have "\<dots> = ?U"
     1.7 -      by(auto simp del: funpow.simps) (metis not0_implies_Suc)
     1.8 +      using assms funpow_decreasing le_SucI mono_if_cont by blast
     1.9      finally show "f ?U \<subseteq> ?U" by simp
    1.10    qed
    1.11  next
     2.1 --- a/src/HOL/Library/Product_Vector.thy	Wed Jan 20 20:19:05 2016 +0100
     2.2 +++ b/src/HOL/Library/Product_Vector.thy	Fri Jan 22 16:00:03 2016 +0000
     2.3 @@ -218,6 +218,20 @@
     2.4  lemma continuous_on_swap[continuous_intros]: "continuous_on A prod.swap"
     2.5    by (simp add: prod.swap_def continuous_on_fst continuous_on_snd continuous_on_Pair continuous_on_id)
     2.6  
     2.7 +lemma continuous_on_swap_args:
     2.8 +  assumes "continuous_on (A\<times>B) (\<lambda>(x,y). d x y)" 
     2.9 +    shows "continuous_on (B\<times>A) (\<lambda>(x,y). d y x)"
    2.10 +proof -
    2.11 +  have "(\<lambda>(x,y). d y x) = (\<lambda>(x,y). d x y) o prod.swap"
    2.12 +    by force
    2.13 +  then show ?thesis
    2.14 +    apply (rule ssubst)
    2.15 +    apply (rule continuous_on_compose)
    2.16 +     apply (force intro: continuous_on_subset [OF continuous_on_swap])
    2.17 +    apply (force intro: continuous_on_subset [OF assms])
    2.18 +    done
    2.19 +qed
    2.20 +
    2.21  lemma isCont_fst [simp]: "isCont f a \<Longrightarrow> isCont (\<lambda>x. fst (f x)) a"
    2.22    by (fact continuous_fst)
    2.23  
     3.1 --- a/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy	Wed Jan 20 20:19:05 2016 +0100
     3.2 +++ b/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy	Fri Jan 22 16:00:03 2016 +0000
     3.3 @@ -5722,8 +5722,8 @@
     3.4  
     3.5  lemma higher_deriv_ident [simp]:
     3.6       "(deriv ^^ n) (\<lambda>w. w) z = (if n = 0 then z else if n = 1 then 1 else 0)"
     3.7 -  apply (induction n)
     3.8 -  apply (simp_all add: deriv_ident funpow_Suc_right del: funpow.simps, simp)
     3.9 +  apply (induction n, simp)
    3.10 +  apply (metis higher_deriv_linear lambda_one)
    3.11    done
    3.12  
    3.13  corollary higher_deriv_id [simp]:
    3.14 @@ -6893,6 +6893,60 @@
    3.15  
    3.16  text\<open>Proof is based on Dixon's, as presented in Lang's "Complex Analysis" book (page 147).\<close>
    3.17  
    3.18 +lemma contour_integral_continuous_on_linepath_2D:
    3.19 +  assumes "open u" and cont_dw: "\<And>w. w \<in> u \<Longrightarrow> F w contour_integrable_on (linepath a b)"
    3.20 +      and cond_uu: "continuous_on (u \<times> u) (\<lambda>(x,y). F x y)"
    3.21 +      and abu: "closed_segment a b \<subseteq> u"
    3.22 +    shows "continuous_on u (\<lambda>w. contour_integral (linepath a b) (F w))"
    3.23 +proof -
    3.24 +  have *: "\<exists>d>0. \<forall>x'\<in>u. dist x' w < d \<longrightarrow>
    3.25 +                         dist (contour_integral (linepath a b) (F x'))
    3.26 +                              (contour_integral (linepath a b) (F w)) \<le> \<epsilon>"
    3.27 +          if "w \<in> u" "0 < \<epsilon>" "a \<noteq> b" for w \<epsilon>
    3.28 +  proof -
    3.29 +    obtain \<delta> where "\<delta>>0" and \<delta>: "cball w \<delta> \<subseteq> u" using open_contains_cball \<open>open u\<close> \<open>w \<in> u\<close> by force
    3.30 +    let ?TZ = "{(t,z) |t z. t \<in> cball w \<delta> \<and> z \<in> closed_segment a b}"
    3.31 +    have "uniformly_continuous_on ?TZ (\<lambda>(x,y). F x y)"
    3.32 +      apply (rule compact_uniformly_continuous)
    3.33 +      apply (rule continuous_on_subset[OF cond_uu])
    3.34 +      using abu \<delta>
    3.35 +      apply (auto simp: compact_Times simp del: mem_cball)
    3.36 +      done
    3.37 +    then obtain \<eta> where "\<eta>>0"
    3.38 +        and \<eta>: "\<And>x x'. \<lbrakk>x\<in>?TZ; x'\<in>?TZ; dist x' x < \<eta>\<rbrakk> \<Longrightarrow>
    3.39 +                         dist ((\<lambda>(x,y). F x y) x') ((\<lambda>(x,y). F x y) x) < \<epsilon>/norm(b - a)"
    3.40 +      apply (rule uniformly_continuous_onE [where e = "\<epsilon>/norm(b - a)"])
    3.41 +      using \<open>0 < \<epsilon>\<close> \<open>a \<noteq> b\<close> by auto
    3.42 +    have \<eta>: "\<lbrakk>norm (w - x1) \<le> \<delta>;   x2 \<in> closed_segment a b; 
    3.43 +              norm (w - x1') \<le> \<delta>;  x2' \<in> closed_segment a b; norm ((x1', x2') - (x1, x2)) < \<eta>\<rbrakk>
    3.44 +              \<Longrightarrow> norm (F x1' x2' - F x1 x2) \<le> \<epsilon> / cmod (b - a)"
    3.45 +             for x1 x2 x1' x2'
    3.46 +      using \<eta> [of "(x1,x2)" "(x1',x2')"] by (force simp add: dist_norm)
    3.47 +    have le_ee: "cmod (contour_integral (linepath a b) (\<lambda>x. F x' x - F w x)) \<le> \<epsilon>"
    3.48 +                if "x' \<in> u" "cmod (x' - w) < \<delta>" "cmod (x' - w) < \<eta>"  for x'
    3.49 +    proof -
    3.50 +      have "cmod (contour_integral (linepath a b) (\<lambda>x. F x' x - F w x)) \<le> \<epsilon>/norm(b - a) * norm(b - a)"
    3.51 +        apply (rule has_contour_integral_bound_linepath [OF has_contour_integral_integral _ \<eta>])
    3.52 +        apply (rule contour_integrable_diff [OF cont_dw cont_dw])
    3.53 +        using \<open>0 < \<epsilon>\<close> \<open>a \<noteq> b\<close> \<open>0 < \<delta>\<close> \<open>w \<in> u\<close> that
    3.54 +        apply (auto simp: norm_minus_commute)
    3.55 +        done
    3.56 +      also have "... = \<epsilon>" using \<open>a \<noteq> b\<close> by simp
    3.57 +      finally show ?thesis .
    3.58 +    qed
    3.59 +    show ?thesis
    3.60 +      apply (rule_tac x="min \<delta> \<eta>" in exI)
    3.61 +      using \<open>0 < \<delta>\<close> \<open>0 < \<eta>\<close>
    3.62 +      apply (auto simp: dist_norm contour_integral_diff [OF cont_dw cont_dw, symmetric] \<open>w \<in> u\<close> intro: le_ee)
    3.63 +      done
    3.64 +  qed
    3.65 +  show ?thesis 
    3.66 +    apply (rule continuous_onI)
    3.67 +    apply (cases "a=b")
    3.68 +    apply (auto intro: *)
    3.69 +    done
    3.70 +qed  
    3.71 +
    3.72  text\<open>This version has @{term"polynomial_function \<gamma>"} as an additional assumption.\<close>
    3.73  lemma Cauchy_integral_formula_global_weak:
    3.74      assumes u: "open u" and holf: "f holomorphic_on u"
    3.75 @@ -7065,10 +7119,10 @@
    3.76      by (meson Lim_at_infinityI)
    3.77    moreover have "h holomorphic_on UNIV"
    3.78    proof -
    3.79 -    have con_ff: "continuous (at (x,z)) (\<lambda>y. (f(snd y) - f(fst y)) / (snd y - fst y))"
    3.80 +    have con_ff: "continuous (at (x,z)) (\<lambda>(x,y). (f y - f x) / (y - x))"
    3.81                   if "x \<in> u" "z \<in> u" "x \<noteq> z" for x z
    3.82        using that conf
    3.83 -      apply (simp add: continuous_on_eq_continuous_at u)
    3.84 +      apply (simp add: split_def continuous_on_eq_continuous_at u)
    3.85        apply (simp | rule continuous_intros continuous_within_compose2 [where g=f])+
    3.86        done
    3.87      have con_fstsnd: "continuous_on UNIV (\<lambda>x. (fst x - snd x) ::complex)"
    3.88 @@ -7083,8 +7137,8 @@
    3.89        apply (rule continuous_on_interior [of u])
    3.90        apply (simp add: holf holomorphic_deriv holomorphic_on_imp_continuous_on u)
    3.91        by (simp add: interior_open that u)
    3.92 -    have tendsto_f': "((\<lambda>x. if snd x = fst x then deriv f (fst x)
    3.93 -                                    else (f (snd x) - f (fst x)) / (snd x - fst x)) \<longlongrightarrow> deriv f x)
    3.94 +    have tendsto_f': "((\<lambda>(x,y). if y = x then deriv f (x)
    3.95 +                                else (f (y) - f (x)) / (y - x)) \<longlongrightarrow> deriv f x)
    3.96                        (at (x, x) within u \<times> u)" if "x \<in> u" for x
    3.97      proof (rule Lim_withinI)
    3.98        fix e::real assume "0 < e"
    3.99 @@ -7120,8 +7174,7 @@
   3.100        qed
   3.101        show "\<exists>d>0. \<forall>xa\<in>u \<times> u.
   3.102                    0 < dist xa (x, x) \<and> dist xa (x, x) < d \<longrightarrow>
   3.103 -                  dist (if snd xa = fst xa then deriv f (fst xa) else (f (snd xa) - f (fst xa)) / (snd xa - fst xa))
   3.104 -                       (deriv f x)  \<le>  e"
   3.105 +                  dist (case xa of (x, y) \<Rightarrow> if y = x then deriv f x else (f y - f x) / (y - x)) (deriv f x) \<le> e"
   3.106          apply (rule_tac x="min k1 k2" in exI)
   3.107          using \<open>k1>0\<close> \<open>k2>0\<close> \<open>e>0\<close>
   3.108          apply (force simp: dist_norm neq intro: dual_order.strict_trans2 k1 less_imp_le norm_fst_le)
   3.109 @@ -7134,16 +7187,16 @@
   3.110        using \<gamma>' using path_image_def vector_derivative_at by fastforce
   3.111      have f_has_cint: "\<And>w. w \<in> v - path_image \<gamma> \<Longrightarrow> ((\<lambda>u. f u / (u - w) ^ 1) has_contour_integral h w) \<gamma>"
   3.112        by (simp add: V)
   3.113 -    have cond_uu: "continuous_on (u \<times> u) (\<lambda>y. d (fst y) (snd y))"
   3.114 +    have cond_uu: "continuous_on (u \<times> u) (\<lambda>(x,y). d x y)"
   3.115        apply (simp add: continuous_on_eq_continuous_within d_def continuous_within tendsto_f')
   3.116        apply (simp add: Lim_within_open_NO_MATCH open_Times u, clarify)
   3.117 -      apply (rule Lim_transform_within_open [OF _ open_uu_Id, where f = "(\<lambda>x. (f (snd x) - f (fst x)) / (snd x - fst x))"])
   3.118 +      apply (rule Lim_transform_within_open [OF _ open_uu_Id, where f = "(\<lambda>(x,y). (f y - f x) / (y - x))"])
   3.119        using con_ff
   3.120        apply (auto simp: continuous_within)
   3.121        done
   3.122      have hol_dw: "(\<lambda>z. d z w) holomorphic_on u" if "w \<in> u" for w
   3.123      proof -
   3.124 -      have "continuous_on u ((\<lambda>y. d (fst y) (snd y)) o (\<lambda>z. (w,z)))"
   3.125 +      have "continuous_on u ((\<lambda>(x,y). d x y) o (\<lambda>z. (w,z)))"
   3.126          by (rule continuous_on_compose continuous_intros continuous_on_subset [OF cond_uu] | force intro: that)+
   3.127        then have *: "continuous_on u (\<lambda>z. if w = z then deriv f z else (f w - f z) / (w - z))"
   3.128          by (rule rev_iffD1 [OF _ continuous_on_cong [OF refl]]) (simp add: d_def field_simps)
   3.129 @@ -7159,53 +7212,11 @@
   3.130      qed
   3.131      { fix a b
   3.132        assume abu: "closed_segment a b \<subseteq> u"
   3.133 -      then have cont_dw: "\<And>w. w \<in> u \<Longrightarrow> (\<lambda>z. d z w) contour_integrable_on (linepath a b)"
   3.134 +      then have "\<And>w. w \<in> u \<Longrightarrow> (\<lambda>z. d z w) contour_integrable_on (linepath a b)"
   3.135          by (metis hol_dw continuous_on_subset contour_integrable_continuous_linepath holomorphic_on_imp_continuous_on)
   3.136 -      have *: "\<exists>da>0. \<forall>x'\<in>u. dist x' w < da \<longrightarrow>
   3.137 -                             dist (contour_integral (linepath a b) (\<lambda>z. d z x'))
   3.138 -                                  (contour_integral (linepath a b) (\<lambda>z. d z w)) \<le> ee"
   3.139 -              if "w \<in> u" "0 < ee" "a \<noteq> b" for w ee
   3.140 -      proof -
   3.141 -        obtain dd where "dd>0" and dd: "cball w dd \<subseteq> u" using open_contains_cball u \<open>w \<in> u\<close> by force
   3.142 -        let ?abdd = "{(z,t) |z t. z \<in> closed_segment a b \<and> t \<in> cball w dd}"
   3.143 -        have "uniformly_continuous_on ?abdd (\<lambda>y. d (fst y) (snd y))"
   3.144 -          apply (rule compact_uniformly_continuous)
   3.145 -          apply (rule continuous_on_subset[OF cond_uu])
   3.146 -          using abu dd
   3.147 -          apply (auto simp: compact_Times simp del: mem_cball)
   3.148 -          done
   3.149 -        then obtain kk where "kk>0"
   3.150 -            and kk: "\<And>x x'. \<lbrakk>x\<in>?abdd; x'\<in>?abdd; dist x' x < kk\<rbrakk> \<Longrightarrow>
   3.151 -                             dist ((\<lambda>y. d (fst y) (snd y)) x') ((\<lambda>y. d (fst y) (snd y)) x) < ee/norm(b - a)"
   3.152 -          apply (rule uniformly_continuous_onE [where e = "ee/norm(b - a)"])
   3.153 -          using \<open>0 < ee\<close> \<open>a \<noteq> b\<close> by auto
   3.154 -        have kk: "\<lbrakk>x1 \<in> closed_segment a b; norm (w - x2) \<le> dd;
   3.155 -                   x1' \<in> closed_segment a b; norm (w - x2') \<le> dd; norm ((x1', x2') - (x1, x2)) < kk\<rbrakk>
   3.156 -                  \<Longrightarrow> norm (d x1' x2' - d x1 x2) \<le> ee / cmod (b - a)"
   3.157 -                 for x1 x2 x1' x2'
   3.158 -          using kk [of "(x1,x2)" "(x1',x2')"] by (force simp add: dist_norm)
   3.159 -        have le_ee: "cmod (contour_integral (linepath a b) (\<lambda>x. d x x' - d x w)) \<le> ee"
   3.160 -                    if "x' \<in> u" "cmod (x' - w) < dd" "cmod (x' - w) < kk"  for x'
   3.161 -        proof -
   3.162 -          have "cmod (contour_integral (linepath a b) (\<lambda>x. d x x' - d x w)) \<le> ee/norm(b - a) * norm(b - a)"
   3.163 -            apply (rule has_contour_integral_bound_linepath [OF has_contour_integral_integral _ kk])
   3.164 -            apply (rule contour_integrable_diff [OF cont_dw cont_dw])
   3.165 -            using \<open>0 < ee\<close> \<open>a \<noteq> b\<close> \<open>0 < dd\<close> \<open>w \<in> u\<close> that
   3.166 -            apply (auto simp: norm_minus_commute)
   3.167 -            done
   3.168 -          also have "... = ee" using \<open>a \<noteq> b\<close> by simp
   3.169 -          finally show ?thesis .
   3.170 -        qed
   3.171 -        show ?thesis
   3.172 -          apply (rule_tac x="min dd kk" in exI)
   3.173 -          using \<open>0 < dd\<close> \<open>0 < kk\<close>
   3.174 -          apply (auto simp: dist_norm contour_integral_diff [OF cont_dw cont_dw, symmetric] \<open>w \<in> u\<close> intro: le_ee)
   3.175 -          done
   3.176 -      qed
   3.177 -      have cont_cint_d: "continuous_on u (\<lambda>w. contour_integral (linepath a b) (\<lambda>z. d z w))"
   3.178 -        apply (rule continuous_onI)
   3.179 -        apply (cases "a=b")
   3.180 -        apply (auto intro: *)
   3.181 +      then have cont_cint_d: "continuous_on u (\<lambda>w. contour_integral (linepath a b) (\<lambda>z. d z w))"
   3.182 +        apply (rule contour_integral_continuous_on_linepath_2D [OF \<open>open u\<close> _ _ abu])
   3.183 +        apply (auto simp: intro: continuous_on_swap_args cond_uu)
   3.184          done
   3.185        have cont_cint_d\<gamma>: "continuous_on {0..1} ((\<lambda>w. contour_integral (linepath a b) (\<lambda>z. d z w)) o \<gamma>)"
   3.186          apply (rule continuous_on_compose)
   3.187 @@ -7223,7 +7234,6 @@
   3.188          using abu  by (force simp add: h_def intro: contour_integral_eq)
   3.189        also have "... =  contour_integral \<gamma> (\<lambda>w. contour_integral (linepath a b) (\<lambda>z. d z w))"
   3.190          apply (rule contour_integral_swap)
   3.191 -        apply (simp add: split_def)
   3.192          apply (rule continuous_on_subset [OF cond_uu])
   3.193          using abu pasz \<open>valid_path \<gamma>\<close>
   3.194          apply (auto intro!: continuous_intros)
   3.195 @@ -7243,17 +7253,16 @@
   3.196        have A2: "\<forall>\<^sub>F n in sequentially. \<forall>xa\<in>path_image \<gamma>. cmod (d (a n) xa - d x xa) < ee" if "0 < ee" for ee
   3.197        proof -
   3.198          let ?ddpa = "{(w,z) |w z. w \<in> cball x dd \<and> z \<in> path_image \<gamma>}"
   3.199 -        have "uniformly_continuous_on ?ddpa (\<lambda>y. d (fst y) (snd y))"
   3.200 +        have "uniformly_continuous_on ?ddpa (\<lambda>(x,y). d x y)"
   3.201            apply (rule compact_uniformly_continuous [OF continuous_on_subset[OF cond_uu]])
   3.202            using dd pasz \<open>valid_path \<gamma>\<close>
   3.203            apply (auto simp: compact_Times compact_valid_path_image simp del: mem_cball)
   3.204            done
   3.205          then obtain kk where "kk>0"
   3.206              and kk: "\<And>x x'. \<lbrakk>x\<in>?ddpa; x'\<in>?ddpa; dist x' x < kk\<rbrakk> \<Longrightarrow>
   3.207 -                             dist ((\<lambda>y. d (fst y) (snd y)) x') ((\<lambda>y. d (fst y) (snd y)) x) < ee"
   3.208 +                             dist ((\<lambda>(x,y). d x y) x') ((\<lambda>(x,y). d x y) x) < ee"
   3.209            apply (rule uniformly_continuous_onE [where e = ee])
   3.210            using \<open>0 < ee\<close> by auto
   3.211 -
   3.212          have kk: "\<lbrakk>norm (w - x) \<le> dd; z \<in> path_image \<gamma>; norm ((w, z) - (x, z)) < kk\<rbrakk> \<Longrightarrow> norm (d w z - d x z) < ee"
   3.213                   for  w z
   3.214            using \<open>dd>0\<close> kk [of "(x,z)" "(w,z)"] by (force simp add: norm_minus_commute dist_norm)
     4.1 --- a/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy	Wed Jan 20 20:19:05 2016 +0100
     4.2 +++ b/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy	Fri Jan 22 16:00:03 2016 +0000
     4.3 @@ -447,16 +447,16 @@
     4.4  lemma holomorphic_cong: "s = t ==> (\<And>x. x \<in> s \<Longrightarrow> f x = g x) \<Longrightarrow> f holomorphic_on s \<longleftrightarrow> g holomorphic_on t"
     4.5    by (metis holomorphic_transform)
     4.6  
     4.7 -lemma holomorphic_on_linear [holomorphic_intros]: "(op * c) holomorphic_on s"
     4.8 +lemma holomorphic_on_linear [simp, holomorphic_intros]: "(op * c) holomorphic_on s"
     4.9    unfolding holomorphic_on_def by (metis complex_differentiable_linear)
    4.10  
    4.11 -lemma holomorphic_on_const [holomorphic_intros]: "(\<lambda>z. c) holomorphic_on s"
    4.12 +lemma holomorphic_on_const [simp, holomorphic_intros]: "(\<lambda>z. c) holomorphic_on s"
    4.13    unfolding holomorphic_on_def by (metis complex_differentiable_const)
    4.14  
    4.15 -lemma holomorphic_on_ident [holomorphic_intros]: "(\<lambda>x. x) holomorphic_on s"
    4.16 +lemma holomorphic_on_ident [simp, holomorphic_intros]: "(\<lambda>x. x) holomorphic_on s"
    4.17    unfolding holomorphic_on_def by (metis complex_differentiable_ident)
    4.18  
    4.19 -lemma holomorphic_on_id [holomorphic_intros]: "id holomorphic_on s"
    4.20 +lemma holomorphic_on_id [simp, holomorphic_intros]: "id holomorphic_on s"
    4.21    unfolding id_def by (rule holomorphic_on_ident)
    4.22  
    4.23  lemma holomorphic_on_compose:
    4.24 @@ -545,6 +545,11 @@
    4.25    unfolding DERIV_deriv_iff_complex_differentiable[symmetric]
    4.26    by (auto intro!: DERIV_imp_deriv derivative_eq_intros)
    4.27  
    4.28 +lemma complex_derivative_cdivide_right:
    4.29 +  "f complex_differentiable at z \<Longrightarrow> deriv (\<lambda>w. f w / c) z = deriv f z / c"
    4.30 +  unfolding Fields.field_class.field_divide_inverse
    4.31 +  by (blast intro: complex_derivative_cmult_right)
    4.32 +
    4.33  lemma complex_derivative_transform_within_open:
    4.34    "\<lbrakk>f holomorphic_on s; g holomorphic_on s; open s; z \<in> s; \<And>w. w \<in> s \<Longrightarrow> f w = g w\<rbrakk>
    4.35     \<Longrightarrow> deriv f z = deriv g z"
     5.1 --- a/src/HOL/Nat.thy	Wed Jan 20 20:19:05 2016 +0100
     5.2 +++ b/src/HOL/Nat.thy	Fri Jan 22 16:00:03 2016 +0000
     5.3 @@ -1329,6 +1329,9 @@
     5.4  
     5.5  end
     5.6  
     5.7 +lemma funpow_0 [simp]: "(f ^^ 0) x = x"
     5.8 +  by simp
     5.9 +
    5.10  lemma funpow_Suc_right:
    5.11    "f ^^ Suc n = f ^^ n \<circ> f"
    5.12  proof (induct n)
     6.1 --- a/src/HOL/Series.thy	Wed Jan 20 20:19:05 2016 +0100
     6.2 +++ b/src/HOL/Series.thy	Fri Jan 22 16:00:03 2016 +0000
     6.3 @@ -129,6 +129,10 @@
     6.4         (simp add: eq atLeast0LessThan del: add_Suc_right)
     6.5  qed
     6.6  
     6.7 +corollary sums_0:
     6.8 +   "(\<And>n. f n = 0) \<Longrightarrow> (f sums 0)"
     6.9 +    by (metis (no_types) finite.emptyI setsum.empty sums_finite)
    6.10 +
    6.11  lemma summable_finite: "finite N \<Longrightarrow> (\<And>n. n \<notin> N \<Longrightarrow> f n = 0) \<Longrightarrow> summable f"
    6.12    by (rule sums_summable) (rule sums_finite)
    6.13  
     7.1 --- a/src/HOL/Topological_Spaces.thy	Wed Jan 20 20:19:05 2016 +0100
     7.2 +++ b/src/HOL/Topological_Spaces.thy	Fri Jan 22 16:00:03 2016 +0000
     7.3 @@ -1076,6 +1076,9 @@
     7.4  lemma lim_le: "convergent f \<Longrightarrow> (\<And>n. f n \<le> (x::'a::linorder_topology)) \<Longrightarrow> lim f \<le> x"
     7.5    using LIMSEQ_le_const2[of f "lim f" x] by (simp add: convergent_LIMSEQ_iff)
     7.6  
     7.7 +lemma lim_const [simp]: "lim (\<lambda>m. a) = a"
     7.8 +  by (simp add: limI)
     7.9 +
    7.10  subsubsection\<open>Increasing and Decreasing Series\<close>
    7.11  
    7.12  lemma incseq_le: "incseq X \<Longrightarrow> X \<longlonglongrightarrow> L \<Longrightarrow> X n \<le> (L::'a::linorder_topology)"