Some new lemmas. Existing lemmas modified to use uniform_limit rather than its expansion
authorpaulson <lp15@cam.ac.uk>
Tue Feb 21 15:04:01 2017 +0000 (2017-02-21)
changeset 65036ab7e11730ad8
parent 65035 b46fe5138cb0
child 65037 2cf841ff23be
Some new lemmas. Existing lemmas modified to use uniform_limit rather than its expansion
src/HOL/Analysis/Bounded_Continuous_Function.thy
src/HOL/Analysis/Cauchy_Integral_Theorem.thy
src/HOL/Analysis/Complex_Transcendental.thy
src/HOL/Analysis/Conformal_Mappings.thy
src/HOL/Analysis/Convex_Euclidean_Space.thy
src/HOL/Analysis/Finite_Product_Measure.thy
src/HOL/Analysis/Function_Topology.thy
src/HOL/Analysis/Henstock_Kurzweil_Integration.thy
src/HOL/Analysis/Topology_Euclidean_Space.thy
src/HOL/Analysis/Uniform_Limit.thy
src/HOL/Limits.thy
src/HOL/Real_Vector_Spaces.thy
src/HOL/Topological_Spaces.thy
src/HOL/Transcendental.thy
     1.1 --- a/src/HOL/Analysis/Bounded_Continuous_Function.thy	Sun Feb 19 11:58:51 2017 +0100
     1.2 +++ b/src/HOL/Analysis/Bounded_Continuous_Function.thy	Tue Feb 21 15:04:01 2017 +0000
     1.3 @@ -190,9 +190,9 @@
     1.4    have "g \<in> bcontfun"  \<comment> \<open>The limit function is bounded and continuous\<close>
     1.5    proof (intro bcontfunI)
     1.6      show "continuous_on UNIV g"
     1.7 -      using bcontfunE[OF Rep_bcontfun] limit_function
     1.8 -      by (intro continuous_uniform_limit[where f="\<lambda>n. Rep_bcontfun (f n)" and F="sequentially"])
     1.9 -        (auto simp add: eventually_sequentially trivial_limit_def dist_norm)
    1.10 +      apply (rule bcontfunE[OF Rep_bcontfun])
    1.11 +      using limit_function
    1.12 +      by (auto simp add: uniform_limit_sequentially_iff intro: uniform_limit_theorem[where f="\<lambda>n. Rep_bcontfun (f n)" and F="sequentially"])
    1.13    next
    1.14      fix x
    1.15      from fg_dist have "dist (g x) (Rep_bcontfun (f N) x) < 1"
     2.1 --- a/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Sun Feb 19 11:58:51 2017 +0100
     2.2 +++ b/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Tue Feb 21 15:04:01 2017 +0000
     2.3 @@ -82,7 +82,7 @@
     2.4    apply (blast intro: continuous_on_compose2)
     2.5    apply (rename_tac A B)
     2.6    apply (rule_tac x="A \<union> (\<Union>x\<in>B. s \<inter> f-`{x})" in exI)
     2.7 -  apply (blast intro: differentiable_chain_within)
     2.8 +  apply (blast intro!: differentiable_chain_within)
     2.9    done
    2.10  
    2.11  lemma piecewise_differentiable_affine:
    2.12 @@ -5172,7 +5172,7 @@
    2.13  
    2.14  proposition contour_integral_uniform_limit:
    2.15    assumes ev_fint: "eventually (\<lambda>n::'a. (f n) contour_integrable_on \<gamma>) F"
    2.16 -      and ev_no: "\<And>e. 0 < e \<Longrightarrow> eventually (\<lambda>n. \<forall>x \<in> path_image \<gamma>. norm(f n x - l x) < e) F"
    2.17 +      and ul_f: "uniform_limit (path_image \<gamma>) f l F"
    2.18        and noleB: "\<And>t. t \<in> {0..1} \<Longrightarrow> norm (vector_derivative \<gamma> (at t)) \<le> B"
    2.19        and \<gamma>: "valid_path \<gamma>"
    2.20        and [simp]: "~ (trivial_limit F)"
    2.21 @@ -5181,10 +5181,13 @@
    2.22    have "0 \<le> B" by (meson noleB [of 0] atLeastAtMost_iff norm_ge_zero order_refl order_trans zero_le_one)
    2.23    { fix e::real
    2.24      assume "0 < e"
    2.25 -    then have eB: "0 < e / (\<bar>B\<bar> + 1)" by simp
    2.26 +    then have "0 < e / (\<bar>B\<bar> + 1)" by simp
    2.27 +    then have "\<forall>\<^sub>F n in F. \<forall>x\<in>path_image \<gamma>. cmod (f n x - l x) < e / (\<bar>B\<bar> + 1)"
    2.28 +      using ul_f [unfolded uniform_limit_iff dist_norm] by auto
    2.29 +    with ev_fint
    2.30      obtain a where fga: "\<And>x. x \<in> {0..1} \<Longrightarrow> cmod (f a (\<gamma> x) - l (\<gamma> x)) < e / (\<bar>B\<bar> + 1)"
    2.31                 and inta: "(\<lambda>t. f a (\<gamma> t) * vector_derivative \<gamma> (at t)) integrable_on {0..1}"
    2.32 -      using eventually_happens [OF eventually_conj [OF ev_no [OF eB] ev_fint]]
    2.33 +      using eventually_happens [OF eventually_conj]
    2.34        by (fastforce simp: contour_integrable_on path_image_def)
    2.35      have Ble: "B * e / (\<bar>B\<bar> + 1) \<le> e"
    2.36        using \<open>0 \<le> B\<close>  \<open>0 < e\<close> by (simp add: divide_simps)
    2.37 @@ -5209,7 +5212,8 @@
    2.38      have B': "B' > 0" "B' > B" using  \<open>0 \<le> B\<close> by (auto simp: B'_def)
    2.39      assume "0 < e"
    2.40      then have ev_no': "\<forall>\<^sub>F n in F. \<forall>x\<in>path_image \<gamma>. 2 * cmod (f n x - l x) < e / B'"
    2.41 -      using ev_no [of "e / B' / 2"] B' by (simp add: field_simps)
    2.42 +      using ul_f [unfolded uniform_limit_iff dist_norm, rule_format, of "e / B' / 2"] B' 
    2.43 +        by (simp add: field_simps)
    2.44      have ie: "integral {0..1::real} (\<lambda>x. e / 2) < e" using \<open>0 < e\<close> by simp
    2.45      have *: "cmod (f x (\<gamma> t) * vector_derivative \<gamma> (at t) - l (\<gamma> t) * vector_derivative \<gamma> (at t)) \<le> e / 2"
    2.46               if t: "t\<in>{0..1}" and leB': "2 * cmod (f x (\<gamma> t) - l (\<gamma> t)) < e / B'" for x t
    2.47 @@ -5235,12 +5239,13 @@
    2.48      by (rule tendstoI)
    2.49  qed
    2.50  
    2.51 -proposition contour_integral_uniform_limit_circlepath:
    2.52 -  assumes ev_fint: "eventually (\<lambda>n::'a. (f n) contour_integrable_on (circlepath z r)) F"
    2.53 -      and ev_no: "\<And>e. 0 < e \<Longrightarrow> eventually (\<lambda>n. \<forall>x \<in> path_image (circlepath z r). norm(f n x - l x) < e) F"
    2.54 -      and [simp]: "~ (trivial_limit F)" "0 < r"
    2.55 -  shows "l contour_integrable_on (circlepath z r)" "((\<lambda>n. contour_integral (circlepath z r) (f n)) \<longlongrightarrow> contour_integral (circlepath z r) l) F"
    2.56 -by (auto simp: vector_derivative_circlepath norm_mult intro: contour_integral_uniform_limit assms)
    2.57 +corollary contour_integral_uniform_limit_circlepath:
    2.58 +  assumes "\<forall>\<^sub>F n::'a in F. (f n) contour_integrable_on (circlepath z r)"
    2.59 +      and "uniform_limit (sphere z r) f l F"
    2.60 +      and "~ (trivial_limit F)" "0 < r"
    2.61 +    shows "l contour_integrable_on (circlepath z r)"
    2.62 +          "((\<lambda>n. contour_integral (circlepath z r) (f n)) \<longlongrightarrow> contour_integral (circlepath z r) l) F"
    2.63 +  using assms by (auto simp: vector_derivative_circlepath norm_mult intro!: contour_integral_uniform_limit)
    2.64  
    2.65  
    2.66  subsection\<open> General stepping result for derivative formulas.\<close>
    2.67 @@ -5371,11 +5376,11 @@
    2.68        apply (force simp: \<open>d > 0\<close> dist_norm that simp del: power_Suc intro: *)
    2.69        done
    2.70    qed
    2.71 -  have 2: "\<forall>\<^sub>F n in at w.
    2.72 -              \<forall>x\<in>path_image \<gamma>.
    2.73 -               cmod (f' x * (inverse (x - n) ^ k - inverse (x - w) ^ k) / (n - w) / of_nat k - f' x / (x - w) ^ Suc k) < e"
    2.74 -          if "0 < e" for e
    2.75 -  proof -
    2.76 +  have 2: "uniform_limit (path_image \<gamma>) (\<lambda>n x. f' x * (inverse (x - n) ^ k - inverse (x - w) ^ k) / (n - w) / of_nat k) (\<lambda>x. f' x / (x - w) ^ Suc k) (at w)"
    2.77 +    unfolding uniform_limit_iff dist_norm
    2.78 +  proof clarify
    2.79 +    fix e::real
    2.80 +    assume "0 < e"
    2.81      have *: "cmod (f' (\<gamma> x) * (inverse (\<gamma> x - u) ^ k - inverse (\<gamma> x - w) ^ k) / ((u - w) * k) -
    2.82                          f' (\<gamma> x) / ((\<gamma> x - w) * (\<gamma> x - w) ^ k)) < e"
    2.83                if ec: "cmod ((inverse (\<gamma> x - u) ^ k - inverse (\<gamma> x - w) ^ k) / ((u - w) * k) -
    2.84 @@ -5402,8 +5407,10 @@
    2.85          by (metis False \<open>0 < e\<close> frac_le less_eq_real_def mult.commute pos_le_divide_eq x zero_less_norm_iff)
    2.86        finally show ?thesis .
    2.87      qed
    2.88 -    show ?thesis
    2.89 -      using twom [OF divide_pos_pos [OF that \<open>C > 0\<close>]]   unfolding path_image_def
    2.90 +    show "\<forall>\<^sub>F n in at w.
    2.91 +              \<forall>x\<in>path_image \<gamma>.
    2.92 +               cmod (f' x * (inverse (x - n) ^ k - inverse (x - w) ^ k) / (n - w) / of_nat k - f' x / (x - w) ^ Suc k) < e"
    2.93 +      using twom [OF divide_pos_pos [OF \<open>0 < e\<close> \<open>C > 0\<close>]]   unfolding path_image_def
    2.94        by (force intro: * elim: eventually_mono)
    2.95    qed
    2.96    show "(\<lambda>u. f' u / (u - w) ^ (Suc k)) contour_integrable_on \<gamma>"
    2.97 @@ -6017,10 +6024,11 @@
    2.98      using w
    2.99      apply (auto simp: dist_norm norm_minus_commute)
   2.100      by (metis add_diff_eq diff_add_cancel norm_diff_ineq norm_minus_commute)
   2.101 -  have *: "\<forall>\<^sub>F n in sequentially. \<forall>x\<in>path_image (circlepath z r).
   2.102 -                norm ((\<Sum>k<n. (w - z) ^ k * (f x / (x - z) ^ Suc k)) - f x / (x - w)) < e"
   2.103 -          if "0 < e" for e
   2.104 -  proof -
   2.105 +  have ul: "uniform_limit (sphere z r) (\<lambda>n x. (\<Sum>k<n. (w - z) ^ k * (f x / (x - z) ^ Suc k))) (\<lambda>x. f x / (x - w)) sequentially"
   2.106 +    unfolding uniform_limit_iff dist_norm 
   2.107 +  proof clarify
   2.108 +    fix e::real
   2.109 +    assume "0 < e"
   2.110      have rr: "0 \<le> (r - k) / r" "(r - k) / r < 1" using  k by auto
   2.111      obtain n where n: "((r - k) / r) ^ n < e / B * k"
   2.112        using real_arch_pow_inv [of "e/B*k" "(r - k)/r"] \<open>0 < e\<close> \<open>0 < B\<close> k by force
   2.113 @@ -6061,7 +6069,8 @@
   2.114        finally show ?thesis
   2.115          by (simp add: divide_simps norm_divide del: power_Suc)
   2.116      qed
   2.117 -    with \<open>0 < r\<close> show ?thesis
   2.118 +    with \<open>0 < r\<close> show "\<forall>\<^sub>F n in sequentially. \<forall>x\<in>sphere z r.
   2.119 +                norm ((\<Sum>k<n. (w - z) ^ k * (f x / (x - z) ^ Suc k)) - f x / (x - w)) < e"
   2.120        by (auto simp: mult_ac less_imp_le eventually_sequentially Ball_def)
   2.121    qed
   2.122    have eq: "\<forall>\<^sub>F x in sequentially.
   2.123 @@ -6076,7 +6085,7 @@
   2.124          sums contour_integral (circlepath z r) (\<lambda>u. f u/(u - w))"
   2.125      unfolding sums_def
   2.126      apply (rule Lim_transform_eventually [OF eq])
   2.127 -    apply (rule contour_integral_uniform_limit_circlepath [OF eventuallyI *])
   2.128 +    apply (rule contour_integral_uniform_limit_circlepath [OF eventuallyI ul])
   2.129      apply (rule contour_integrable_sum, simp)
   2.130      apply (rule contour_integrable_lmul)
   2.131      apply (rule Cauchy_higher_derivative_integral_circlepath [OF contf holf])
   2.132 @@ -6189,7 +6198,7 @@
   2.133  
   2.134  proposition holomorphic_uniform_limit:
   2.135    assumes cont: "eventually (\<lambda>n. continuous_on (cball z r) (f n) \<and> (f n) holomorphic_on ball z r) F"
   2.136 -      and lim: "\<And>e. 0 < e \<Longrightarrow> eventually (\<lambda>n. \<forall>x \<in> cball z r. norm(f n x - g x) < e) F"
   2.137 +      and ulim: "uniform_limit (cball z r) f g F"
   2.138        and F:  "~ trivial_limit F"
   2.139    obtains "continuous_on (cball z r) g" "g holomorphic_on ball z r"
   2.140  proof (cases r "0::real" rule: linorder_cases)
   2.141 @@ -6200,8 +6209,7 @@
   2.142  next
   2.143    case greater
   2.144    have contg: "continuous_on (cball z r) g"
   2.145 -    using cont
   2.146 -    by (fastforce simp: eventually_conj_iff dist_norm intro: eventually_mono [OF lim] continuous_uniform_limit [OF F])
   2.147 +    using cont uniform_limit_theorem [OF eventually_mono ulim F]  by blast
   2.148    have 1: "continuous_on (path_image (circlepath z r)) (\<lambda>x. 1 / (2 * complex_of_real pi * \<i>) * g x)"
   2.149      apply (rule continuous_intros continuous_on_subset [OF contg])+
   2.150      using \<open>0 < r\<close> by auto
   2.151 @@ -6217,17 +6225,16 @@
   2.152        using w
   2.153        apply (auto intro: Cauchy_higher_derivative_integral_circlepath [where k=0, simplified])
   2.154        done
   2.155 -    have ev_less: "\<forall>\<^sub>F n in F. \<forall>x\<in>path_image (circlepath z r). cmod (f n x / (x - w) - g x / (x - w)) < e"
   2.156 -         if "e > 0" for e
   2.157 -      using greater \<open>0 < d\<close> \<open>0 < e\<close>
   2.158 -      apply (simp add: norm_divide diff_divide_distrib [symmetric] divide_simps)
   2.159 -      apply (rule_tac e1="e * d" in eventually_mono [OF lim])
   2.160 -      apply (force simp: dist_norm intro: dle mult_left_mono less_le_trans)+
   2.161 +    have ul_less: "uniform_limit (sphere z r) (\<lambda>n x. f n x / (x - w)) (\<lambda>x. g x / (x - w)) F"
   2.162 +      using greater \<open>0 < d\<close> 
   2.163 +      apply (clarsimp simp add: uniform_limit_iff dist_norm norm_divide diff_divide_distrib [symmetric] divide_simps)
   2.164 +      apply (rule_tac e1="e * d" in eventually_mono [OF uniform_limitD [OF ulim]])
   2.165 +       apply (force simp: dist_norm intro: dle mult_left_mono less_le_trans)+
   2.166        done
   2.167      have g_cint: "(\<lambda>u. g u/(u - w)) contour_integrable_on circlepath z r"
   2.168 -      by (rule contour_integral_uniform_limit_circlepath [OF ev_int ev_less F \<open>0 < r\<close>])
   2.169 +      by (rule contour_integral_uniform_limit_circlepath [OF ev_int ul_less F \<open>0 < r\<close>])
   2.170      have cif_tends_cig: "((\<lambda>n. contour_integral(circlepath z r) (\<lambda>u. f n u / (u - w))) \<longlongrightarrow> contour_integral(circlepath z r) (\<lambda>u. g u/(u - w))) F"
   2.171 -      by (rule contour_integral_uniform_limit_circlepath [OF ev_int ev_less F \<open>0 < r\<close>])
   2.172 +      by (rule contour_integral_uniform_limit_circlepath [OF ev_int ul_less F \<open>0 < r\<close>])
   2.173      have f_tends_cig: "((\<lambda>n. 2 * of_real pi * \<i> * f n w) \<longlongrightarrow> contour_integral (circlepath z r) (\<lambda>u. g u / (u - w))) F"
   2.174        apply (rule Lim_transform_eventually [where f = "\<lambda>n. contour_integral (circlepath z r) (\<lambda>u. f n u/(u - w))"])
   2.175        apply (rule eventually_mono [OF cont])
   2.176 @@ -6237,7 +6244,7 @@
   2.177        done
   2.178      have "((\<lambda>n. 2 * of_real pi * \<i> * f n w) \<longlongrightarrow> 2 * of_real pi * \<i> * g w) F"
   2.179        apply (rule tendsto_mult_left [OF tendstoI])
   2.180 -      apply (rule eventually_mono [OF lim], assumption)
   2.181 +      apply (rule eventually_mono [OF uniform_limitD [OF ulim]], assumption)
   2.182        using w
   2.183        apply (force simp add: dist_norm)
   2.184        done
   2.185 @@ -6262,7 +6269,7 @@
   2.186    fixes z::complex
   2.187    assumes cont: "eventually (\<lambda>n. continuous_on (cball z r) (f n) \<and>
   2.188                                 (\<forall>w \<in> ball z r. ((f n) has_field_derivative (f' n w)) (at w))) F"
   2.189 -      and lim: "\<And>e. 0 < e \<Longrightarrow> eventually (\<lambda>n. \<forall>x \<in> cball z r. norm(f n x - g x) < e) F"
   2.190 +      and ulim: "uniform_limit (cball z r) f g F"
   2.191        and F:  "~ trivial_limit F" and "0 < r"
   2.192    obtains g' where
   2.193        "continuous_on (cball z r) g"
   2.194 @@ -6270,7 +6277,7 @@
   2.195  proof -
   2.196    let ?conint = "contour_integral (circlepath z r)"
   2.197    have g: "continuous_on (cball z r) g" "g holomorphic_on ball z r"
   2.198 -    by (rule holomorphic_uniform_limit [OF eventually_mono [OF cont] lim F];
   2.199 +    by (rule holomorphic_uniform_limit [OF eventually_mono [OF cont] ulim F];
   2.200               auto simp: holomorphic_on_open field_differentiable_def)+
   2.201    then obtain g' where g': "\<And>x. x \<in> ball z r \<Longrightarrow> (g has_field_derivative g' x) (at x)"
   2.202      using DERIV_deriv_iff_has_field_derivative
   2.203 @@ -6303,13 +6310,19 @@
   2.204        done
   2.205      have 1: "\<forall>\<^sub>F n in F. (\<lambda>x. f n x / (x - w)\<^sup>2) contour_integrable_on circlepath z r"
   2.206        by (force simp add: holomorphic_on_open intro: w Cauchy_derivative_integral_circlepath eventually_mono [OF cont])
   2.207 -    have 2: "0 < e \<Longrightarrow> \<forall>\<^sub>F n in F. \<forall>x \<in> path_image (circlepath z r). cmod (f n x / (x - w)\<^sup>2 - g x / (x - w)\<^sup>2) < e" for e
   2.208 -      using \<open>r > 0\<close>
   2.209 -      apply (simp add: diff_divide_distrib [symmetric] norm_divide divide_simps sphere_def)
   2.210 -      apply (rule eventually_mono [OF lim, of "e*d"])
   2.211 -      apply (simp add: \<open>0 < d\<close>)
   2.212 -      apply (force simp add: dist_norm dle intro: less_le_trans)
   2.213 -      done
   2.214 +    have 2: "uniform_limit (sphere z r) (\<lambda>n x. f n x / (x - w)\<^sup>2) (\<lambda>x. g x / (x - w)\<^sup>2) F"
   2.215 +      unfolding uniform_limit_iff
   2.216 +    proof clarify
   2.217 +      fix e::real
   2.218 +      assume "0 < e"
   2.219 +      with  \<open>r > 0\<close>
   2.220 +      show "\<forall>\<^sub>F n in F. \<forall>x\<in>sphere z r. dist (f n x / (x - w)\<^sup>2) (g x / (x - w)\<^sup>2) < e"
   2.221 +        apply (simp add: diff_divide_distrib [symmetric] norm_divide divide_simps sphere_def dist_norm)
   2.222 +        apply (rule eventually_mono [OF uniform_limitD [OF ulim], of "e*d"])
   2.223 +         apply (simp add: \<open>0 < d\<close>)
   2.224 +        apply (force simp add: dist_norm dle intro: less_le_trans)
   2.225 +        done
   2.226 +    qed
   2.227      have "((\<lambda>n. contour_integral (circlepath z r) (\<lambda>x. f n x / (x - w)\<^sup>2))
   2.228               \<longlongrightarrow> contour_integral (circlepath z r) ((\<lambda>x. g x / (x - w)\<^sup>2))) F"
   2.229        by (rule contour_integral_uniform_limit_circlepath [OF 1 2 F \<open>0 < r\<close>])
   2.230 @@ -6331,18 +6344,16 @@
   2.231  subsection\<open>Some more simple/convenient versions for applications.\<close>
   2.232  
   2.233  lemma holomorphic_uniform_sequence:
   2.234 -  assumes s: "open s"
   2.235 -      and hol_fn: "\<And>n. (f n) holomorphic_on s"
   2.236 -      and to_g: "\<And>x. x \<in> s
   2.237 -                     \<Longrightarrow> \<exists>d. 0 < d \<and> cball x d \<subseteq> s \<and>
   2.238 -                             (\<forall>e. 0 < e \<longrightarrow> eventually (\<lambda>n. \<forall>y \<in> cball x d. norm(f n y - g y) < e) sequentially)"
   2.239 -  shows "g holomorphic_on s"
   2.240 +  assumes S: "open S"
   2.241 +      and hol_fn: "\<And>n. (f n) holomorphic_on S"
   2.242 +      and ulim_g: "\<And>x. x \<in> S \<Longrightarrow> \<exists>d. 0 < d \<and> cball x d \<subseteq> S \<and> uniform_limit (cball x d) f g sequentially"
   2.243 +  shows "g holomorphic_on S"
   2.244  proof -
   2.245 -  have "\<exists>f'. (g has_field_derivative f') (at z)" if "z \<in> s" for z
   2.246 +  have "\<exists>f'. (g has_field_derivative f') (at z)" if "z \<in> S" for z
   2.247    proof -
   2.248 -    obtain r where "0 < r" and r: "cball z r \<subseteq> s"
   2.249 -               and fg: "\<forall>e. 0 < e \<longrightarrow> eventually (\<lambda>n. \<forall>y \<in> cball z r. norm(f n y - g y) < e) sequentially"
   2.250 -      using to_g [OF \<open>z \<in> s\<close>] by blast
   2.251 +    obtain r where "0 < r" and r: "cball z r \<subseteq> S"
   2.252 +               and ul: "uniform_limit (cball z r) f g sequentially"
   2.253 +      using ulim_g [OF \<open>z \<in> S\<close>] by blast 
   2.254      have *: "\<forall>\<^sub>F n in sequentially. continuous_on (cball z r) (f n) \<and> f n holomorphic_on ball z r"
   2.255        apply (intro eventuallyI conjI)
   2.256        using hol_fn holomorphic_on_imp_continuous_on holomorphic_on_subset r apply blast
   2.257 @@ -6350,37 +6361,36 @@
   2.258        done
   2.259      show ?thesis
   2.260        apply (rule holomorphic_uniform_limit [OF *])
   2.261 -      using \<open>0 < r\<close> centre_in_ball fg
   2.262 +      using \<open>0 < r\<close> centre_in_ball ul
   2.263        apply (auto simp: holomorphic_on_open)
   2.264        done
   2.265    qed
   2.266 -  with s show ?thesis
   2.267 +  with S show ?thesis
   2.268      by (simp add: holomorphic_on_open)
   2.269  qed
   2.270  
   2.271  lemma has_complex_derivative_uniform_sequence:
   2.272 -  fixes s :: "complex set"
   2.273 -  assumes s: "open s"
   2.274 -      and hfd: "\<And>n x. x \<in> s \<Longrightarrow> ((f n) has_field_derivative f' n x) (at x)"
   2.275 -      and to_g: "\<And>x. x \<in> s
   2.276 -             \<Longrightarrow> \<exists>d. 0 < d \<and> cball x d \<subseteq> s \<and>
   2.277 -                     (\<forall>e. 0 < e \<longrightarrow> eventually (\<lambda>n. \<forall>y \<in> cball x d. norm(f n y - g y) < e) sequentially)"
   2.278 -  shows "\<exists>g'. \<forall>x \<in> s. (g has_field_derivative g' x) (at x) \<and> ((\<lambda>n. f' n x) \<longlongrightarrow> g' x) sequentially"
   2.279 +  fixes S :: "complex set"
   2.280 +  assumes S: "open S"
   2.281 +      and hfd: "\<And>n x. x \<in> S \<Longrightarrow> ((f n) has_field_derivative f' n x) (at x)"
   2.282 +      and ulim_g: "\<And>x. x \<in> S
   2.283 +             \<Longrightarrow> \<exists>d. 0 < d \<and> cball x d \<subseteq> S \<and> uniform_limit (cball x d) f g sequentially"
   2.284 +  shows "\<exists>g'. \<forall>x \<in> S. (g has_field_derivative g' x) (at x) \<and> ((\<lambda>n. f' n x) \<longlongrightarrow> g' x) sequentially"
   2.285  proof -
   2.286 -  have y: "\<exists>y. (g has_field_derivative y) (at z) \<and> (\<lambda>n. f' n z) \<longlonglongrightarrow> y" if "z \<in> s" for z
   2.287 +  have y: "\<exists>y. (g has_field_derivative y) (at z) \<and> (\<lambda>n. f' n z) \<longlonglongrightarrow> y" if "z \<in> S" for z
   2.288    proof -
   2.289 -    obtain r where "0 < r" and r: "cball z r \<subseteq> s"
   2.290 -               and fg: "\<forall>e. 0 < e \<longrightarrow> eventually (\<lambda>n. \<forall>y \<in> cball z r. norm(f n y - g y) < e) sequentially"
   2.291 -      using to_g [OF \<open>z \<in> s\<close>] by blast
   2.292 +    obtain r where "0 < r" and r: "cball z r \<subseteq> S"
   2.293 +               and ul: "uniform_limit (cball z r) f g sequentially"
   2.294 +      using ulim_g [OF \<open>z \<in> S\<close>] by blast 
   2.295      have *: "\<forall>\<^sub>F n in sequentially. continuous_on (cball z r) (f n) \<and>
   2.296                                     (\<forall>w \<in> ball z r. ((f n) has_field_derivative (f' n w)) (at w))"
   2.297        apply (intro eventuallyI conjI)
   2.298 -      apply (meson hfd holomorphic_on_imp_continuous_on holomorphic_on_open holomorphic_on_subset r s)
   2.299 +      apply (meson hfd holomorphic_on_imp_continuous_on holomorphic_on_open holomorphic_on_subset r S)
   2.300        using ball_subset_cball hfd r apply blast
   2.301        done
   2.302      show ?thesis
   2.303        apply (rule has_complex_derivative_uniform_limit [OF *, of g])
   2.304 -      using \<open>0 < r\<close> centre_in_ball fg
   2.305 +      using \<open>0 < r\<close> centre_in_ball ul
   2.306        apply force+
   2.307        done
   2.308    qed
   2.309 @@ -6390,67 +6400,67 @@
   2.310  
   2.311  
   2.312  subsection\<open>On analytic functions defined by a series.\<close>
   2.313 -
   2.314 + 
   2.315  lemma series_and_derivative_comparison:
   2.316 -  fixes s :: "complex set"
   2.317 -  assumes s: "open s"
   2.318 +  fixes S :: "complex set"
   2.319 +  assumes S: "open S"
   2.320        and h: "summable h"
   2.321 -      and hfd: "\<And>n x. x \<in> s \<Longrightarrow> (f n has_field_derivative f' n x) (at x)"
   2.322 -      and to_g: "\<And>n x. \<lbrakk>N \<le> n; x \<in> s\<rbrakk> \<Longrightarrow> norm(f n x) \<le> h n"
   2.323 -  obtains g g' where "\<forall>x \<in> s. ((\<lambda>n. f n x) sums g x) \<and> ((\<lambda>n. f' n x) sums g' x) \<and> (g has_field_derivative g' x) (at x)"
   2.324 +      and hfd: "\<And>n x. x \<in> S \<Longrightarrow> (f n has_field_derivative f' n x) (at x)"
   2.325 +      and to_g: "\<forall>\<^sub>F n in sequentially. \<forall>x\<in>S. norm (f n x) \<le> h n"
   2.326 +  obtains g g' where "\<forall>x \<in> S. ((\<lambda>n. f n x) sums g x) \<and> ((\<lambda>n. f' n x) sums g' x) \<and> (g has_field_derivative g' x) (at x)"
   2.327  proof -
   2.328 -  obtain g where g: "\<And>e. e>0 \<Longrightarrow> \<exists>N. \<forall>n x. N \<le> n \<and> x \<in> s \<longrightarrow> dist (\<Sum>n<n. f n x) (g x) < e"
   2.329 -    using series_comparison_uniform [OF h to_g, of N s] by force
   2.330 -  have *: "\<exists>d>0. cball x d \<subseteq> s \<and> (\<forall>e>0. \<forall>\<^sub>F n in sequentially. \<forall>y\<in>cball x d. cmod ((\<Sum>a<n. f a y) - g y) < e)"
   2.331 -         if "x \<in> s" for x
   2.332 +  obtain g where g: "uniform_limit S (\<lambda>n x. \<Sum>i<n. f i x) g sequentially"
   2.333 +    using weierstrass_m_test_ev [OF to_g h]  by force
   2.334 +  have *: "\<exists>d>0. cball x d \<subseteq> S \<and> uniform_limit (cball x d) (\<lambda>n x. \<Sum>i<n. f i x) g sequentially"
   2.335 +         if "x \<in> S" for x
   2.336    proof -
   2.337 -    obtain d where "d>0" and d: "cball x d \<subseteq> s"
   2.338 -      using open_contains_cball [of "s"] \<open>x \<in> s\<close> s by blast
   2.339 +    obtain d where "d>0" and d: "cball x d \<subseteq> S"
   2.340 +      using open_contains_cball [of "S"] \<open>x \<in> S\<close> S by blast
   2.341      then show ?thesis
   2.342        apply (rule_tac x=d in exI)
   2.343 -      apply (auto simp: dist_norm eventually_sequentially)
   2.344 -      apply (metis g contra_subsetD dist_norm)
   2.345 -      done
   2.346 +        using g uniform_limit_on_subset
   2.347 +        apply (force simp: dist_norm eventually_sequentially)
   2.348 +          done
   2.349    qed
   2.350 -  have "(\<forall>x\<in>s. (\<lambda>n. \<Sum>i<n. f i x) \<longlonglongrightarrow> g x)"
   2.351 -    using g by (force simp add: lim_sequentially)
   2.352 -  moreover have "\<exists>g'. \<forall>x\<in>s. (g has_field_derivative g' x) (at x) \<and> (\<lambda>n. \<Sum>i<n. f' i x) \<longlonglongrightarrow> g' x"
   2.353 -    by (rule has_complex_derivative_uniform_sequence [OF s]) (auto intro: * hfd DERIV_sum)+
   2.354 +  have "\<And>x. x \<in> S \<Longrightarrow> (\<lambda>n. \<Sum>i<n. f i x) \<longlonglongrightarrow> g x"
   2.355 +    by (metis tendsto_uniform_limitI [OF g])
   2.356 +  moreover have "\<exists>g'. \<forall>x\<in>S. (g has_field_derivative g' x) (at x) \<and> (\<lambda>n. \<Sum>i<n. f' i x) \<longlonglongrightarrow> g' x"
   2.357 +    by (rule has_complex_derivative_uniform_sequence [OF S]) (auto intro: * hfd DERIV_sum)+
   2.358    ultimately show ?thesis
   2.359 -    by (force simp add: sums_def  conj_commute intro: that)
   2.360 +    by (metis sums_def that)
   2.361  qed
   2.362  
   2.363  text\<open>A version where we only have local uniform/comparative convergence.\<close>
   2.364  
   2.365  lemma series_and_derivative_comparison_local:
   2.366 -  fixes s :: "complex set"
   2.367 -  assumes s: "open s"
   2.368 -      and hfd: "\<And>n x. x \<in> s \<Longrightarrow> (f n has_field_derivative f' n x) (at x)"
   2.369 -      and to_g: "\<And>x. x \<in> s \<Longrightarrow>
   2.370 -                      \<exists>d h N. 0 < d \<and> summable h \<and> (\<forall>n y. N \<le> n \<and> y \<in> ball x d \<longrightarrow> norm(f n y) \<le> h n)"
   2.371 -  shows "\<exists>g g'. \<forall>x \<in> s. ((\<lambda>n. f n x) sums g x) \<and> ((\<lambda>n. f' n x) sums g' x) \<and> (g has_field_derivative g' x) (at x)"
   2.372 +  fixes S :: "complex set"
   2.373 +  assumes S: "open S"
   2.374 +      and hfd: "\<And>n x. x \<in> S \<Longrightarrow> (f n has_field_derivative f' n x) (at x)"
   2.375 +      and to_g: "\<And>x. x \<in> S \<Longrightarrow> \<exists>d h. 0 < d \<and> summable h \<and> (\<forall>\<^sub>F n in sequentially. \<forall>y\<in>ball x d \<inter> S. norm (f n y) \<le> h n)"
   2.376 +  shows "\<exists>g g'. \<forall>x \<in> S. ((\<lambda>n. f n x) sums g x) \<and> ((\<lambda>n. f' n x) sums g' x) \<and> (g has_field_derivative g' x) (at x)"
   2.377  proof -
   2.378    have "\<exists>y. (\<lambda>n. f n z) sums (\<Sum>n. f n z) \<and> (\<lambda>n. f' n z) sums y \<and> ((\<lambda>x. \<Sum>n. f n x) has_field_derivative y) (at z)"
   2.379 -       if "z \<in> s" for z
   2.380 +       if "z \<in> S" for z
   2.381    proof -
   2.382 -    obtain d h N where "0 < d" "summable h" and le_h: "\<And>n y. \<lbrakk>N \<le> n; y \<in> ball z d\<rbrakk> \<Longrightarrow> norm(f n y) \<le> h n"
   2.383 -      using to_g \<open>z \<in> s\<close> by meson
   2.384 -    then obtain r where "r>0" and r: "ball z r \<subseteq> ball z d \<inter> s" using \<open>z \<in> s\<close> s
   2.385 +    obtain d h where "0 < d" "summable h" and le_h: "\<forall>\<^sub>F n in sequentially. \<forall>y\<in>ball z d \<inter> S. norm (f n y) \<le> h n"
   2.386 +      using to_g \<open>z \<in> S\<close> by meson
   2.387 +    then obtain r where "r>0" and r: "ball z r \<subseteq> ball z d \<inter> S" using \<open>z \<in> S\<close> S
   2.388        by (metis Int_iff open_ball centre_in_ball open_Int open_contains_ball_eq)
   2.389 -    have 1: "open (ball z d \<inter> s)"
   2.390 -      by (simp add: open_Int s)
   2.391 -    have 2: "\<And>n x. x \<in> ball z d \<inter> s \<Longrightarrow> (f n has_field_derivative f' n x) (at x)"
   2.392 +    have 1: "open (ball z d \<inter> S)"
   2.393 +      by (simp add: open_Int S)
   2.394 +    have 2: "\<And>n x. x \<in> ball z d \<inter> S \<Longrightarrow> (f n has_field_derivative f' n x) (at x)"
   2.395        by (auto simp: hfd)
   2.396 -    obtain g g' where gg': "\<forall>x \<in> ball z d \<inter> s. ((\<lambda>n. f n x) sums g x) \<and>
   2.397 +    obtain g g' where gg': "\<forall>x \<in> ball z d \<inter> S. ((\<lambda>n. f n x) sums g x) \<and>
   2.398                                      ((\<lambda>n. f' n x) sums g' x) \<and> (g has_field_derivative g' x) (at x)"
   2.399        by (auto intro: le_h series_and_derivative_comparison [OF 1 \<open>summable h\<close> hfd])
   2.400      then have "(\<lambda>n. f' n z) sums g' z"
   2.401        by (meson \<open>0 < r\<close> centre_in_ball contra_subsetD r)
   2.402      moreover have "(\<lambda>n. f n z) sums (\<Sum>n. f n z)"
   2.403 -      by (metis summable_comparison_test' summable_sums centre_in_ball \<open>0 < d\<close> \<open>summable h\<close> le_h)
   2.404 +      using  summable_sums centre_in_ball \<open>0 < d\<close> \<open>summable h\<close> le_h
   2.405 +      by (metis (full_types) Int_iff gg' summable_def that)
   2.406      moreover have "((\<lambda>x. \<Sum>n. f n x) has_field_derivative g' z) (at z)"
   2.407        apply (rule_tac f=g in DERIV_transform_at [OF _ \<open>0 < r\<close>])
   2.408 -      apply (simp add: gg' \<open>z \<in> s\<close> \<open>0 < d\<close>)
   2.409 +      apply (simp add: gg' \<open>z \<in> S\<close> \<open>0 < d\<close>)
   2.410        apply (metis (full_types) contra_subsetD dist_commute gg' mem_ball r sums_unique)
   2.411        done
   2.412      ultimately show ?thesis by auto
   2.413 @@ -6463,21 +6473,16 @@
   2.414  text\<open>Sometimes convenient to compare with a complex series of positive reals. (?)\<close>
   2.415  
   2.416  lemma series_and_derivative_comparison_complex:
   2.417 -  fixes s :: "complex set"
   2.418 -  assumes s: "open s"
   2.419 -      and hfd: "\<And>n x. x \<in> s \<Longrightarrow> (f n has_field_derivative f' n x) (at x)"
   2.420 -      and to_g: "\<And>x. x \<in> s \<Longrightarrow>
   2.421 -                      \<exists>d h N. 0 < d \<and> summable h \<and> range h \<subseteq> nonneg_Reals \<and> (\<forall>n y. N \<le> n \<and> y \<in> ball x d \<longrightarrow> cmod(f n y) \<le> cmod (h n))"
   2.422 -  shows "\<exists>g g'. \<forall>x \<in> s. ((\<lambda>n. f n x) sums g x) \<and> ((\<lambda>n. f' n x) sums g' x) \<and> (g has_field_derivative g' x) (at x)"
   2.423 -apply (rule series_and_derivative_comparison_local [OF s hfd], assumption)
   2.424 -apply (frule to_g)
   2.425 -apply (erule ex_forward)
   2.426 +  fixes S :: "complex set"
   2.427 +  assumes S: "open S"
   2.428 +      and hfd: "\<And>n x. x \<in> S \<Longrightarrow> (f n has_field_derivative f' n x) (at x)"
   2.429 +      and to_g: "\<And>x. x \<in> S \<Longrightarrow> \<exists>d h. 0 < d \<and> summable h \<and> range h \<subseteq> \<real>\<^sub>\<ge>\<^sub>0 \<and> (\<forall>\<^sub>F n in sequentially. \<forall>y\<in>ball x d \<inter> S. cmod(f n y) \<le> cmod (h n))"
   2.430 +  shows "\<exists>g g'. \<forall>x \<in> S. ((\<lambda>n. f n x) sums g x) \<and> ((\<lambda>n. f' n x) sums g' x) \<and> (g has_field_derivative g' x) (at x)"
   2.431 +apply (rule series_and_derivative_comparison_local [OF S hfd], assumption)
   2.432 +apply (rule ex_forward [OF to_g], assumption)
   2.433  apply (erule exE)
   2.434  apply (rule_tac x="Re o h" in exI)
   2.435 -apply (erule ex_forward)
   2.436 -apply (simp add: summable_Re o_def )
   2.437 -apply (elim conjE all_forward)
   2.438 -apply (simp add: nonneg_Reals_cmod_eq_Re image_subset_iff)
   2.439 +apply (force simp add: summable_Re o_def nonneg_Reals_cmod_eq_Re image_subset_iff)
   2.440  done
   2.441  
   2.442  
   2.443 @@ -6512,12 +6517,12 @@
   2.444        apply (simp add: dist_norm)
   2.445        apply (rule_tac x="\<lambda>n. of_real(norm(a n)*((r + norm z)/2)^n)" in exI)
   2.446        using \<open>r > 0\<close>
   2.447 -      apply (auto simp: sum nonneg_Reals_divide_I)
   2.448 +      apply (auto simp: sum eventually_sequentially norm_mult norm_divide norm_power)
   2.449        apply (rule_tac x=0 in exI)
   2.450 -      apply (force simp: norm_mult norm_divide norm_power intro!: mult_left_mono power_mono y_le)
   2.451 +      apply (force simp: dist_norm intro!: mult_left_mono power_mono y_le)
   2.452        done
   2.453    then show ?thesis
   2.454 -    by (simp add: dist_0_norm ball_def)
   2.455 +    by (simp add: ball_def)
   2.456  next
   2.457    case False then show ?thesis
   2.458      apply (simp add: not_less)
   2.459 @@ -6833,7 +6838,6 @@
   2.460  qed
   2.461  
   2.462  
   2.463 -
   2.464  subsection\<open>General, homology form of Cauchy's theorem.\<close>
   2.465  
   2.466  text\<open>Proof is based on Dixon's, as presented in Lang's "Complex Analysis" book (page 147).\<close>
   2.467 @@ -7196,28 +7200,34 @@
   2.468        then have A1: "\<forall>\<^sub>F n in sequentially. d (a n) contour_integrable_on \<gamma>"
   2.469          by (meson U contour_integrable_on_def eventuallyI)
   2.470        obtain dd where "dd>0" and dd: "cball x dd \<subseteq> u" using open_contains_cball u x by force
   2.471 -      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
   2.472 -      proof -
   2.473 -        let ?ddpa = "{(w,z) |w z. w \<in> cball x dd \<and> z \<in> path_image \<gamma>}"
   2.474 -        have "uniformly_continuous_on ?ddpa (\<lambda>(x,y). d x y)"
   2.475 -          apply (rule compact_uniformly_continuous [OF continuous_on_subset[OF cond_uu]])
   2.476 -          using dd pasz \<open>valid_path \<gamma>\<close>
   2.477 -          apply (auto simp: compact_Times compact_valid_path_image simp del: mem_cball)
   2.478 -          done
   2.479 -        then obtain kk where "kk>0"
   2.480 +      have A2: "uniform_limit (path_image \<gamma>) (\<lambda>n. d (a n)) (d x) sequentially"
   2.481 +        unfolding uniform_limit_iff dist_norm
   2.482 +      proof clarify
   2.483 +        fix ee::real
   2.484 +        assume "0 < ee"
   2.485 +        show "\<forall>\<^sub>F n in sequentially. \<forall>\<xi>\<in>path_image \<gamma>. cmod (d (a n) \<xi> - d x \<xi>) < ee"
   2.486 +        proof -
   2.487 +          let ?ddpa = "{(w,z) |w z. w \<in> cball x dd \<and> z \<in> path_image \<gamma>}"
   2.488 +          have "uniformly_continuous_on ?ddpa (\<lambda>(x,y). d x y)"
   2.489 +            apply (rule compact_uniformly_continuous [OF continuous_on_subset[OF cond_uu]])
   2.490 +            using dd pasz \<open>valid_path \<gamma>\<close>
   2.491 +             apply (auto simp: compact_Times compact_valid_path_image simp del: mem_cball)
   2.492 +            done
   2.493 +          then obtain kk where "kk>0"
   2.494              and kk: "\<And>x x'. \<lbrakk>x\<in>?ddpa; x'\<in>?ddpa; dist x' x < kk\<rbrakk> \<Longrightarrow>
   2.495                               dist ((\<lambda>(x,y). d x y) x') ((\<lambda>(x,y). d x y) x) < ee"
   2.496 -          apply (rule uniformly_continuous_onE [where e = ee])
   2.497 -          using \<open>0 < ee\<close> by auto
   2.498 -        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"
   2.499 -                 for  w z
   2.500 -          using \<open>dd>0\<close> kk [of "(x,z)" "(w,z)"] by (force simp add: norm_minus_commute dist_norm)
   2.501 -        show ?thesis
   2.502 -          using ax unfolding lim_sequentially eventually_sequentially
   2.503 -          apply (drule_tac x="min dd kk" in spec)
   2.504 -          using \<open>dd > 0\<close> \<open>kk > 0\<close>
   2.505 -          apply (fastforce simp: kk dist_norm)
   2.506 -          done
   2.507 +            apply (rule uniformly_continuous_onE [where e = ee])
   2.508 +            using \<open>0 < ee\<close> by auto
   2.509 +          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"
   2.510 +            for  w z
   2.511 +            using \<open>dd>0\<close> kk [of "(x,z)" "(w,z)"] by (force simp add: norm_minus_commute dist_norm)
   2.512 +          show ?thesis
   2.513 +            using ax unfolding lim_sequentially eventually_sequentially
   2.514 +            apply (drule_tac x="min dd kk" in spec)
   2.515 +            using \<open>dd > 0\<close> \<open>kk > 0\<close>
   2.516 +            apply (fastforce simp: kk dist_norm)
   2.517 +            done
   2.518 +        qed
   2.519        qed
   2.520        have tendsto_hx: "(\<lambda>n. contour_integral \<gamma> (d (a n))) \<longlonglongrightarrow> h x"
   2.521          apply (simp add: contour_integral_unique [OF U, symmetric] x)
   2.522 @@ -7285,87 +7295,87 @@
   2.523  
   2.524  
   2.525  theorem Cauchy_integral_formula_global:
   2.526 -    assumes s: "open s" and holf: "f holomorphic_on s"
   2.527 -        and z: "z \<in> s" and vpg: "valid_path \<gamma>"
   2.528 -        and pasz: "path_image \<gamma> \<subseteq> s - {z}" and loop: "pathfinish \<gamma> = pathstart \<gamma>"
   2.529 -        and zero: "\<And>w. w \<notin> s \<Longrightarrow> winding_number \<gamma> w = 0"
   2.530 +    assumes S: "open S" and holf: "f holomorphic_on S"
   2.531 +        and z: "z \<in> S" and vpg: "valid_path \<gamma>"
   2.532 +        and pasz: "path_image \<gamma> \<subseteq> S - {z}" and loop: "pathfinish \<gamma> = pathstart \<gamma>"
   2.533 +        and zero: "\<And>w. w \<notin> S \<Longrightarrow> winding_number \<gamma> w = 0"
   2.534        shows "((\<lambda>w. f w / (w - z)) has_contour_integral (2*pi * \<i> * winding_number \<gamma> z * f z)) \<gamma>"
   2.535  proof -
   2.536    have "path \<gamma>" using vpg by (blast intro: valid_path_imp_path)
   2.537 -  have hols: "(\<lambda>w. f w / (w - z)) holomorphic_on s - {z}" "(\<lambda>w. 1 / (w - z)) holomorphic_on s - {z}"
   2.538 +  have hols: "(\<lambda>w. f w / (w - z)) holomorphic_on S - {z}" "(\<lambda>w. 1 / (w - z)) holomorphic_on S - {z}"
   2.539      by (rule holomorphic_intros holomorphic_on_subset [OF holf] | force)+
   2.540    then have cint_fw: "(\<lambda>w. f w / (w - z)) contour_integrable_on \<gamma>"
   2.541 -    by (meson contour_integrable_holomorphic_simple holomorphic_on_imp_continuous_on open_delete s vpg pasz)
   2.542 +    by (meson contour_integrable_holomorphic_simple holomorphic_on_imp_continuous_on open_delete S vpg pasz)
   2.543    obtain d where "d>0"
   2.544        and d: "\<And>g h. \<lbrakk>valid_path g; valid_path h; \<forall>t\<in>{0..1}. cmod (g t - \<gamma> t) < d \<and> cmod (h t - \<gamma> t) < d;
   2.545                       pathstart h = pathstart g \<and> pathfinish h = pathfinish g\<rbrakk>
   2.546 -                     \<Longrightarrow> path_image h \<subseteq> s - {z} \<and> (\<forall>f. f holomorphic_on s - {z} \<longrightarrow> contour_integral h f = contour_integral g f)"
   2.547 -    using contour_integral_nearby_ends [OF _ \<open>path \<gamma>\<close> pasz] s by (simp add: open_Diff) metis
   2.548 +                     \<Longrightarrow> path_image h \<subseteq> S - {z} \<and> (\<forall>f. f holomorphic_on S - {z} \<longrightarrow> contour_integral h f = contour_integral g f)"
   2.549 +    using contour_integral_nearby_ends [OF _ \<open>path \<gamma>\<close> pasz] S by (simp add: open_Diff) metis
   2.550    obtain p where polyp: "polynomial_function p"
   2.551               and ps: "pathstart p = pathstart \<gamma>" and pf: "pathfinish p = pathfinish \<gamma>" and led: "\<forall>t\<in>{0..1}. cmod (p t - \<gamma> t) < d"
   2.552      using path_approx_polynomial_function [OF \<open>path \<gamma>\<close> \<open>d > 0\<close>] by blast
   2.553    then have ploop: "pathfinish p = pathstart p" using loop by auto
   2.554    have vpp: "valid_path p"  using polyp valid_path_polynomial_function by blast
   2.555    have [simp]: "z \<notin> path_image \<gamma>" using pasz by blast
   2.556 -  have paps: "path_image p \<subseteq> s - {z}" and cint_eq: "(\<And>f. f holomorphic_on s - {z} \<Longrightarrow> contour_integral p f = contour_integral \<gamma> f)"
   2.557 +  have paps: "path_image p \<subseteq> S - {z}" and cint_eq: "(\<And>f. f holomorphic_on S - {z} \<Longrightarrow> contour_integral p f = contour_integral \<gamma> f)"
   2.558      using pf ps led d [OF vpg vpp] \<open>d > 0\<close> by auto
   2.559    have wn_eq: "winding_number p z = winding_number \<gamma> z"
   2.560      using vpp paps
   2.561      by (simp add: subset_Diff_insert vpg valid_path_polynomial_function winding_number_valid_path cint_eq hols)
   2.562 -  have "winding_number p w = winding_number \<gamma> w" if "w \<notin> s" for w
   2.563 +  have "winding_number p w = winding_number \<gamma> w" if "w \<notin> S" for w
   2.564    proof -
   2.565 -    have hol: "(\<lambda>v. 1 / (v - w)) holomorphic_on s - {z}"
   2.566 +    have hol: "(\<lambda>v. 1 / (v - w)) holomorphic_on S - {z}"
   2.567        using that by (force intro: holomorphic_intros holomorphic_on_subset [OF holf])
   2.568     have "w \<notin> path_image p" "w \<notin> path_image \<gamma>" using paps pasz that by auto
   2.569     then show ?thesis
   2.570      using vpp vpg by (simp add: subset_Diff_insert valid_path_polynomial_function winding_number_valid_path cint_eq [OF hol])
   2.571    qed
   2.572 -  then have wn0: "\<And>w. w \<notin> s \<Longrightarrow> winding_number p w = 0"
   2.573 +  then have wn0: "\<And>w. w \<notin> S \<Longrightarrow> winding_number p w = 0"
   2.574      by (simp add: zero)
   2.575    show ?thesis
   2.576 -    using Cauchy_integral_formula_global_weak [OF s holf z polyp paps ploop wn0] hols
   2.577 +    using Cauchy_integral_formula_global_weak [OF S holf z polyp paps ploop wn0] hols
   2.578      by (metis wn_eq cint_eq has_contour_integral_eqpath cint_fw cint_eq)
   2.579  qed
   2.580  
   2.581  theorem Cauchy_theorem_global:
   2.582 -    assumes s: "open s" and holf: "f holomorphic_on s"
   2.583 +    assumes S: "open S" and holf: "f holomorphic_on S"
   2.584          and vpg: "valid_path \<gamma>" and loop: "pathfinish \<gamma> = pathstart \<gamma>"
   2.585 -        and pas: "path_image \<gamma> \<subseteq> s"
   2.586 -        and zero: "\<And>w. w \<notin> s \<Longrightarrow> winding_number \<gamma> w = 0"
   2.587 +        and pas: "path_image \<gamma> \<subseteq> S"
   2.588 +        and zero: "\<And>w. w \<notin> S \<Longrightarrow> winding_number \<gamma> w = 0"
   2.589        shows "(f has_contour_integral 0) \<gamma>"
   2.590  proof -
   2.591 -  obtain z where "z \<in> s" and znot: "z \<notin> path_image \<gamma>"
   2.592 +  obtain z where "z \<in> S" and znot: "z \<notin> path_image \<gamma>"
   2.593    proof -
   2.594      have "compact (path_image \<gamma>)"
   2.595        using compact_valid_path_image vpg by blast
   2.596 -    then have "path_image \<gamma> \<noteq> s"
   2.597 -      by (metis (no_types) compact_open path_image_nonempty s)
   2.598 +    then have "path_image \<gamma> \<noteq> S"
   2.599 +      by (metis (no_types) compact_open path_image_nonempty S)
   2.600      with pas show ?thesis by (blast intro: that)
   2.601    qed
   2.602 -  then have pasz: "path_image \<gamma> \<subseteq> s - {z}" using pas by blast
   2.603 -  have hol: "(\<lambda>w. (w - z) * f w) holomorphic_on s"
   2.604 +  then have pasz: "path_image \<gamma> \<subseteq> S - {z}" using pas by blast
   2.605 +  have hol: "(\<lambda>w. (w - z) * f w) holomorphic_on S"
   2.606      by (rule holomorphic_intros holf)+
   2.607    show ?thesis
   2.608 -    using Cauchy_integral_formula_global [OF s hol \<open>z \<in> s\<close> vpg pasz loop zero]
   2.609 +    using Cauchy_integral_formula_global [OF S hol \<open>z \<in> S\<close> vpg pasz loop zero]
   2.610      by (auto simp: znot elim!: has_contour_integral_eq)
   2.611  qed
   2.612  
   2.613  corollary Cauchy_theorem_global_outside:
   2.614 -    assumes "open s" "f holomorphic_on s" "valid_path \<gamma>"  "pathfinish \<gamma> = pathstart \<gamma>" "path_image \<gamma> \<subseteq> s"
   2.615 -            "\<And>w. w \<notin> s \<Longrightarrow> w \<in> outside(path_image \<gamma>)"
   2.616 +    assumes "open S" "f holomorphic_on S" "valid_path \<gamma>"  "pathfinish \<gamma> = pathstart \<gamma>" "path_image \<gamma> \<subseteq> S"
   2.617 +            "\<And>w. w \<notin> S \<Longrightarrow> w \<in> outside(path_image \<gamma>)"
   2.618        shows "(f has_contour_integral 0) \<gamma>"
   2.619  by (metis Cauchy_theorem_global assms winding_number_zero_in_outside valid_path_imp_path)
   2.620  
   2.621  
   2.622  lemma simply_connected_imp_winding_number_zero:
   2.623 -  assumes "simply_connected s" "path g"
   2.624 -           "path_image g \<subseteq> s" "pathfinish g = pathstart g" "z \<notin> s"
   2.625 +  assumes "simply_connected S" "path g"
   2.626 +           "path_image g \<subseteq> S" "pathfinish g = pathstart g" "z \<notin> S"
   2.627      shows "winding_number g z = 0"
   2.628  proof -
   2.629    have "winding_number g z = winding_number(linepath (pathstart g) (pathstart g)) z"
   2.630      apply (rule winding_number_homotopic_paths)
   2.631      apply (rule homotopic_loops_imp_homotopic_paths_null [where a = "pathstart g"])
   2.632 -    apply (rule homotopic_loops_subset [of s])
   2.633 +    apply (rule homotopic_loops_subset [of S])
   2.634      using assms
   2.635      apply (auto simp: homotopic_paths_imp_homotopic_loops path_defs simply_connected_eq_contractible_path)
   2.636      done
   2.637 @@ -7375,8 +7385,8 @@
   2.638  qed
   2.639  
   2.640  lemma Cauchy_theorem_simply_connected:
   2.641 -  assumes "open s" "simply_connected s" "f holomorphic_on s" "valid_path g"
   2.642 -           "path_image g \<subseteq> s" "pathfinish g = pathstart g"
   2.643 +  assumes "open S" "simply_connected S" "f holomorphic_on S" "valid_path g"
   2.644 +           "path_image g \<subseteq> S" "pathfinish g = pathstart g"
   2.645      shows "(f has_contour_integral 0) g"
   2.646  using assms
   2.647  apply (simp add: simply_connected_eq_contractible_path)
     3.1 --- a/src/HOL/Analysis/Complex_Transcendental.thy	Sun Feb 19 11:58:51 2017 +0100
     3.2 +++ b/src/HOL/Analysis/Complex_Transcendental.thy	Tue Feb 21 15:04:01 2017 +0000
     3.3 @@ -1386,7 +1386,7 @@
     3.4                            else Ln(z) - \<i> * of_real(3 * pi/2))"
     3.5    using Im_Ln_le_pi [of z] mpi_less_Im_Ln [of z] assms
     3.6          Im_Ln_eq_pi [of z] Im_Ln_pos_lt [of z] Re_Ln_pos_le [of z]
     3.7 -  by (auto simp: Ln_times)
     3.8 +  by (simp add: Ln_times) auto 
     3.9  
    3.10  lemma Ln_of_nat: "0 < n \<Longrightarrow> Ln (of_nat n) = of_real (ln (of_nat n))"
    3.11    by (subst of_real_of_nat_eq[symmetric], subst Ln_of_real[symmetric]) simp_all
     4.1 --- a/src/HOL/Analysis/Conformal_Mappings.thy	Sun Feb 19 11:58:51 2017 +0100
     4.2 +++ b/src/HOL/Analysis/Conformal_Mappings.thy	Tue Feb 21 15:04:01 2017 +0000
     4.3 @@ -14,8 +14,8 @@
     4.4  lemma Cauchy_higher_deriv_bound:
     4.5      assumes holf: "f holomorphic_on (ball z r)"
     4.6          and contf: "continuous_on (cball z r) f"
     4.7 +        and fin : "\<And>w. w \<in> ball z r \<Longrightarrow> f w \<in> ball y B0"
     4.8          and "0 < r" and "0 < n"
     4.9 -        and fin : "\<And>w. w \<in> ball z r \<Longrightarrow> f w \<in> ball y B0"
    4.10        shows "norm ((deriv ^^ n) f z) \<le> (fact n) * B0 / r^n"
    4.11  proof -
    4.12    have "0 < B0" using \<open>0 < r\<close> fin [of z]
     5.1 --- a/src/HOL/Analysis/Convex_Euclidean_Space.thy	Sun Feb 19 11:58:51 2017 +0100
     5.2 +++ b/src/HOL/Analysis/Convex_Euclidean_Space.thy	Tue Feb 21 15:04:01 2017 +0000
     5.3 @@ -1369,19 +1369,6 @@
     5.4      by (auto simp add:norm_minus_commute)
     5.5  qed
     5.6  
     5.7 -lemma norm_minus_eqI: "x = - y \<Longrightarrow> norm x = norm y" by auto
     5.8 -
     5.9 -lemma Min_grI:
    5.10 -  assumes "finite A" "A \<noteq> {}" "\<forall>a\<in>A. x < a"
    5.11 -  shows "x < Min A"
    5.12 -  unfolding Min_gr_iff[OF assms(1,2)] using assms(3) by auto
    5.13 -
    5.14 -lemma norm_lt: "norm x < norm y \<longleftrightarrow> inner x x < inner y y"
    5.15 -  unfolding norm_eq_sqrt_inner by simp
    5.16 -
    5.17 -lemma norm_le: "norm x \<le> norm y \<longleftrightarrow> inner x x \<le> inner y y"
    5.18 -  unfolding norm_eq_sqrt_inner by simp
    5.19 -
    5.20  
    5.21  subsection \<open>Affine set and affine hull\<close>
    5.22  
    5.23 @@ -8474,19 +8461,8 @@
    5.24    assume as: "\<forall>i\<in>Basis. 0 < x \<bullet> i" "sum (op \<bullet> x) Basis < 1"
    5.25    obtain a :: 'b where "a \<in> UNIV" using UNIV_witness ..
    5.26    let ?d = "(1 - sum (op \<bullet> x) Basis) / real (DIM('a))"
    5.27 -  have "Min ((op \<bullet> x) ` Basis) > 0"
    5.28 -    apply (rule Min_grI)
    5.29 -    using as(1)
    5.30 -    apply auto
    5.31 -    done
    5.32 -  moreover have "?d > 0"
    5.33 -    using as(2) by (auto simp: Suc_le_eq DIM_positive)
    5.34 -  ultimately show "\<exists>e>0. \<forall>y. dist x y < e \<longrightarrow> (\<forall>i\<in>Basis. 0 \<le> y \<bullet> i) \<and> sum (op \<bullet> y) Basis \<le> 1"
    5.35 -    apply (rule_tac x="min (Min ((op \<bullet> x) ` Basis)) D" for D in exI)
    5.36 -    apply rule
    5.37 -    defer
    5.38 -    apply (rule, rule)
    5.39 -  proof -
    5.40 +  show "\<exists>e>0. \<forall>y. dist x y < e \<longrightarrow> (\<forall>i\<in>Basis. 0 \<le> y \<bullet> i) \<and> sum (op \<bullet> y) Basis \<le> 1"
    5.41 +  proof (rule_tac x="min (Min ((op \<bullet> x) ` Basis)) D" for D in exI, intro conjI impI allI)
    5.42      fix y
    5.43      assume y: "dist x y < min (Min (op \<bullet> x ` Basis)) ?d"
    5.44      have "sum (op \<bullet> y) Basis \<le> sum (\<lambda>i. x\<bullet>i + ?d) Basis"
    5.45 @@ -8505,7 +8481,8 @@
    5.46      also have "\<dots> \<le> 1"
    5.47        unfolding sum.distrib sum_constant
    5.48        by (auto simp add: Suc_le_eq)
    5.49 -    finally show "(\<forall>i\<in>Basis. 0 \<le> y \<bullet> i) \<and> sum (op \<bullet> y) Basis \<le> 1"
    5.50 +    finally show "sum (op \<bullet> y) Basis \<le> 1" .
    5.51 +    show "(\<forall>i\<in>Basis. 0 \<le> y \<bullet> i)"
    5.52      proof safe
    5.53        fix i :: 'a
    5.54        assume i: "i \<in> Basis"
    5.55 @@ -8519,7 +8496,14 @@
    5.56          using Basis_le_norm[OF i, of "x - y"] and as(1)[rule_format, OF i]
    5.57          by (auto simp: inner_simps)
    5.58      qed
    5.59 -  qed auto
    5.60 +  next
    5.61 +    have "Min ((op \<bullet> x) ` Basis) > 0"
    5.62 +      using as by simp
    5.63 +    moreover have "?d > 0"
    5.64 +      using as by (auto simp: Suc_le_eq)
    5.65 +    ultimately show "0 < min (Min (op \<bullet> x ` Basis)) ((1 - sum (op \<bullet> x) Basis) / real DIM('a))"
    5.66 +      by linarith
    5.67 +  qed 
    5.68  qed
    5.69  
    5.70  lemma interior_std_simplex_nonempty:
    5.71 @@ -8655,7 +8639,7 @@
    5.72        have "0 < card d" using \<open>d \<noteq> {}\<close> \<open>finite d\<close>
    5.73          by (simp add: card_gt_0_iff)
    5.74        have "Min ((op \<bullet> x) ` d) > 0"
    5.75 -        using as \<open>d \<noteq> {}\<close> \<open>finite d\<close> by (simp add: Min_grI)
    5.76 +        using as \<open>d \<noteq> {}\<close> \<open>finite d\<close> by (simp add: Min_gr_iff)
    5.77        moreover have "?d > 0" using as using \<open>0 < card d\<close> by auto
    5.78        ultimately have h3: "min (Min ((op \<bullet> x) ` d)) ?d > 0"
    5.79          by auto
     6.1 --- a/src/HOL/Analysis/Finite_Product_Measure.thy	Sun Feb 19 11:58:51 2017 +0100
     6.2 +++ b/src/HOL/Analysis/Finite_Product_Measure.thy	Tue Feb 21 15:04:01 2017 +0000
     6.3 @@ -1135,7 +1135,7 @@
     6.4  proof (intro PiM_eqI)
     6.5    fix A assume A: "\<And>ia. ia \<in> {i} \<Longrightarrow> A ia \<in> sets (M ia)"
     6.6    then have "(\<lambda>x. \<lambda>i\<in>{i}. x) -` Pi\<^sub>E {i} A \<inter> space (M i) = A i"
     6.7 -    by (auto dest: sets.sets_into_space)
     6.8 +    by (fastforce dest: sets.sets_into_space)
     6.9    with A show "emeasure (distr (M i) (Pi\<^sub>M {i} M) (\<lambda>x. \<lambda>i\<in>{i}. x)) (Pi\<^sub>E {i} A) = (\<Prod>i\<in>{i}. emeasure (M i) (A i))"
    6.10      by (subst emeasure_distr) (auto intro!: sets_PiM_I_finite measurable_restrict)
    6.11  qed simp_all
     7.1 --- a/src/HOL/Analysis/Function_Topology.thy	Sun Feb 19 11:58:51 2017 +0100
     7.2 +++ b/src/HOL/Analysis/Function_Topology.thy	Tue Feb 21 15:04:01 2017 +0000
     7.3 @@ -967,7 +967,7 @@
     7.4      by blast
     7.5    define m where "m = Min {(1/2)^(to_nat i) * e i|i. i \<in> I}"
     7.6    have "m > 0" if "I\<noteq>{}"
     7.7 -    unfolding m_def apply (rule Min_grI) using \<open>finite I\<close> \<open>I \<noteq> {}\<close> \<open>\<And>i. e i > 0\<close> by auto
     7.8 +    unfolding m_def Min_gr_iff using \<open>finite I\<close> \<open>I \<noteq> {}\<close> \<open>\<And>i. e i > 0\<close> by auto
     7.9    moreover have "{y. dist x y < m} \<subseteq> U"
    7.10    proof (auto)
    7.11      fix y assume "dist x y < m"
     8.1 --- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Sun Feb 19 11:58:51 2017 +0100
     8.2 +++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Tue Feb 21 15:04:01 2017 +0000
     8.3 @@ -9,10 +9,7 @@
     8.4    Lebesgue_Measure Tagged_Division
     8.5  begin
     8.6  
     8.7 -(* BEGIN MOVE *)
     8.8 -lemma norm_minus2: "norm (x1-x2, y1-y2) = norm (x2-x1, y2-y1)"
     8.9 -  by (simp add: norm_minus_eqI)
    8.10 -
    8.11 +(* try instead structured proofs below *)
    8.12  lemma norm_diff2: "\<lbrakk>y = y1 + y2; x = x1 + x2; e = e1 + e2; norm(y1 - x1) \<le> e1; norm(y2 - x2) \<le> e2\<rbrakk>
    8.13    \<Longrightarrow> norm(y - x) \<le> e"
    8.14    using norm_triangle_mono [of "y1 - x1" "e1" "y2 - x2" "e2"]
    8.15 @@ -7696,10 +7693,12 @@
    8.16          assume xuvwz: "x1 \<in> cbox u v" "x2 \<in> cbox w z"
    8.17          then have x: "x1 \<in> cbox a b" "x2 \<in> cbox c d"
    8.18            using uwvz_sub by auto
    8.19 -        have "norm (x1 - t1, x2 - t2) < k"
    8.20 +        have "norm (x1 - t1, x2 - t2) = norm (t1 - x1, t2 - x2)"
    8.21 +          by (simp add: norm_Pair norm_minus_commute)
    8.22 +        also have "norm (t1 - x1, t2 - x2) < k"
    8.23            using xuvwz ls uwvz_sub unfolding ball_def
    8.24 -          by (force simp add: cbox_Pair_eq dist_norm norm_minus2)
    8.25 -        then have "norm (f (x1,x2) - f (t1,t2)) \<le> e / content ?CBOX / 2"
    8.26 +          by (force simp add: cbox_Pair_eq dist_norm )
    8.27 +        finally have "norm (f (x1,x2) - f (t1,t2)) \<le> e / content ?CBOX / 2"
    8.28            using nf [OF t x]  by simp
    8.29        } note nf' = this
    8.30        have f_int_uwvz: "f integrable_on cbox (u,w) (v,z)"
    8.31 @@ -7852,7 +7851,7 @@
    8.32        finally show ?thesis .
    8.33      qed (insert a, simp_all add: integral_f)
    8.34      thus "bounded {integral {c..} (f k) |k. True}"
    8.35 -      by (intro bounded_realI[of _ "exp (-a*c)/a"]) auto
    8.36 +      by (intro boundedI[of _ "exp (-a*c)/a"]) auto
    8.37    qed (auto simp: f_def)
    8.38  
    8.39    from eventually_gt_at_top[of "nat \<lceil>c\<rceil>"] have "eventually (\<lambda>k. of_nat k > c) sequentially"
    8.40 @@ -7945,7 +7944,7 @@
    8.41        finally have "abs (F k) \<le>  c powr (a + 1) / (a + 1)" .
    8.42      }
    8.43      thus "bounded {integral {0..c} (f k) |k. True}"
    8.44 -      by (intro bounded_realI[of _ "c powr (a+1) / (a+1)"]) (auto simp: integral_f)
    8.45 +      by (intro boundedI[of _ "c powr (a+1) / (a+1)"]) (auto simp: integral_f)
    8.46    qed
    8.47  
    8.48    from False c have "c > 0" by simp
     9.1 --- a/src/HOL/Analysis/Topology_Euclidean_Space.thy	Sun Feb 19 11:58:51 2017 +0100
     9.2 +++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy	Tue Feb 21 15:04:01 2017 +0000
     9.3 @@ -92,12 +92,6 @@
     9.4    "finite I \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> countable (F i)) \<Longrightarrow> countable (Pi\<^sub>E I F)"
     9.5    by (induct I arbitrary: F rule: finite_induct) (auto simp: PiE_insert_eq)
     9.6  
     9.7 -lemma continuous_on_cases:
     9.8 -  "closed s \<Longrightarrow> closed t \<Longrightarrow> continuous_on s f \<Longrightarrow> continuous_on t g \<Longrightarrow>
     9.9 -    \<forall>x. (x\<in>s \<and> \<not> P x) \<or> (x \<in> t \<and> P x) \<longrightarrow> f x = g x \<Longrightarrow>
    9.10 -    continuous_on (s \<union> t) (\<lambda>x. if P x then f x else g x)"
    9.11 -  by (rule continuous_on_If) auto
    9.12 -
    9.13  lemma open_sums:
    9.14    fixes T :: "('b::real_normed_vector) set"
    9.15    assumes "open S \<or> open T"
    9.16 @@ -3946,11 +3940,10 @@
    9.17  lemma bdd_above_norm: "bdd_above (norm ` X) \<longleftrightarrow> bounded X"
    9.18    by (simp add: bounded_iff bdd_above_def)
    9.19  
    9.20 -lemma bounded_realI:
    9.21 -  assumes "\<forall>x\<in>s. \<bar>x::real\<bar> \<le> B"
    9.22 -  shows "bounded s"
    9.23 -  unfolding bounded_def dist_real_def
    9.24 -  by (metis abs_minus_commute assms diff_0_right)
    9.25 +lemma boundedI:
    9.26 +  assumes "\<And>x. x \<in> S \<Longrightarrow> norm x \<le> B"
    9.27 +  shows "bounded S"
    9.28 +  using assms bounded_iff by blast
    9.29  
    9.30  lemma bounded_empty [simp]: "bounded {}"
    9.31    by (simp add: bounded_def)
    9.32 @@ -5100,7 +5093,7 @@
    9.33    "compact (s :: 'a::metric_space set) \<longleftrightarrow> seq_compact s"
    9.34    using compact_imp_seq_compact seq_compact_imp_heine_borel by blast
    9.35  
    9.36 -lemma compact_def:
    9.37 +lemma compact_def: --\<open>this is the definition of compactness in HOL Light\<close>
    9.38    "compact (S :: 'a::metric_space set) \<longleftrightarrow>
    9.39     (\<forall>f. (\<forall>n. f n \<in> S) \<longrightarrow> (\<exists>l\<in>S. \<exists>r. subseq r \<and> (f \<circ> r) \<longlonglongrightarrow> l))"
    9.40    unfolding compact_eq_seq_compact_metric seq_compact_def by auto
    9.41 @@ -7576,48 +7569,6 @@
    9.42    qed (insert D, auto)
    9.43  qed auto
    9.44  
    9.45 -text \<open>A uniformly convergent limit of continuous functions is continuous.\<close>
    9.46 -
    9.47 -lemma continuous_uniform_limit:
    9.48 -  fixes f :: "'a \<Rightarrow> 'b::metric_space \<Rightarrow> 'c::metric_space"
    9.49 -  assumes "\<not> trivial_limit F"
    9.50 -    and "eventually (\<lambda>n. continuous_on s (f n)) F"
    9.51 -    and "\<forall>e>0. eventually (\<lambda>n. \<forall>x\<in>s. dist (f n x) (g x) < e) F"
    9.52 -  shows "continuous_on s g"
    9.53 -proof -
    9.54 -  {
    9.55 -    fix x and e :: real
    9.56 -    assume "x\<in>s" "e>0"
    9.57 -    have "eventually (\<lambda>n. \<forall>x\<in>s. dist (f n x) (g x) < e / 3) F"
    9.58 -      using \<open>e>0\<close> assms(3)[THEN spec[where x="e/3"]] by auto
    9.59 -    from eventually_happens [OF eventually_conj [OF this assms(2)]]
    9.60 -    obtain n where n:"\<forall>x\<in>s. dist (f n x) (g x) < e / 3"  "continuous_on s (f n)"
    9.61 -      using assms(1) by blast
    9.62 -    have "e / 3 > 0" using \<open>e>0\<close> by auto
    9.63 -    then obtain d where "d>0" and d:"\<forall>x'\<in>s. dist x' x < d \<longrightarrow> dist (f n x') (f n x) < e / 3"
    9.64 -      using n(2)[unfolded continuous_on_iff, THEN bspec[where x=x], OF \<open>x\<in>s\<close>, THEN spec[where x="e/3"]] by blast
    9.65 -    {
    9.66 -      fix y
    9.67 -      assume "y \<in> s" and "dist y x < d"
    9.68 -      then have "dist (f n y) (f n x) < e / 3"
    9.69 -        by (rule d [rule_format])
    9.70 -      then have "dist (f n y) (g x) < 2 * e / 3"
    9.71 -        using dist_triangle [of "f n y" "g x" "f n x"]
    9.72 -        using n(1)[THEN bspec[where x=x], OF \<open>x\<in>s\<close>]
    9.73 -        by auto
    9.74 -      then have "dist (g y) (g x) < e"
    9.75 -        using n(1)[THEN bspec[where x=y], OF \<open>y\<in>s\<close>]
    9.76 -        using dist_triangle3 [of "g y" "g x" "f n y"]
    9.77 -        by auto
    9.78 -    }
    9.79 -    then have "\<exists>d>0. \<forall>x'\<in>s. dist x' x < d \<longrightarrow> dist (g x') (g x) < e"
    9.80 -      using \<open>d>0\<close> by auto
    9.81 -  }
    9.82 -  then show ?thesis
    9.83 -    unfolding continuous_on_iff by auto
    9.84 -qed
    9.85 -
    9.86 -
    9.87  subsection \<open>Topological stuff about the set of Reals\<close>
    9.88  
    9.89  lemma open_real:
    10.1 --- a/src/HOL/Analysis/Uniform_Limit.thy	Sun Feb 19 11:58:51 2017 +0100
    10.2 +++ b/src/HOL/Analysis/Uniform_Limit.thy	Tue Feb 21 15:04:01 2017 +0000
    10.3 @@ -472,6 +472,73 @@
    10.4    bounded_bilinear.bounded_uniform_limit[OF Real_Vector_Spaces.bounded_bilinear_mult]
    10.5    bounded_bilinear.bounded_uniform_limit[OF Real_Vector_Spaces.bounded_bilinear_scaleR]
    10.6  
    10.7 +lemma uniform_lim_mult:
    10.8 +  fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'c::real_normed_algebra"
    10.9 +  assumes f: "uniform_limit S f l F"
   10.10 +      and g: "uniform_limit S g m F"
   10.11 +      and l: "bounded (l ` S)"
   10.12 +      and m: "bounded (m ` S)"
   10.13 +    shows "uniform_limit S (\<lambda>a b. f a b * g a b) (\<lambda>a. l a * m a) F"
   10.14 +  by (intro bounded_bilinear_bounded_uniform_limit_intros assms)
   10.15 +
   10.16 +lemma uniform_lim_inverse:
   10.17 +  fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'c::real_normed_field"
   10.18 +  assumes f: "uniform_limit S f l F"
   10.19 +      and b: "\<And>x. x \<in> S \<Longrightarrow> b \<le> norm(l x)"
   10.20 +      and "b > 0"
   10.21 +    shows "uniform_limit S (\<lambda>x y. inverse (f x y)) (inverse \<circ> l) F"
   10.22 +proof (rule uniform_limitI)
   10.23 +  fix e::real
   10.24 +  assume "e > 0"
   10.25 +  have lte: "dist (inverse (f x y)) ((inverse \<circ> l) y) < e"
   10.26 +           if "b/2 \<le> norm (f x y)" "norm (f x y - l y) < e * b\<^sup>2 / 2" "y \<in> S"
   10.27 +           for x y
   10.28 +  proof -
   10.29 +    have [simp]: "l y \<noteq> 0" "f x y \<noteq> 0"
   10.30 +      using \<open>b > 0\<close> that b [OF \<open>y \<in> S\<close>] by fastforce+
   10.31 +    have "norm (l y - f x y) <  e * b\<^sup>2 / 2"
   10.32 +      by (metis norm_minus_commute that(2))
   10.33 +    also have "... \<le> e * (norm (f x y) * norm (l y))"
   10.34 +      using \<open>e > 0\<close> that b [OF \<open>y \<in> S\<close>] apply (simp add: power2_eq_square)
   10.35 +      by (metis \<open>b > 0\<close> less_eq_real_def mult.left_commute mult_mono')
   10.36 +    finally show ?thesis
   10.37 +      by (auto simp: dist_norm divide_simps norm_mult norm_divide)
   10.38 +  qed
   10.39 +  have "\<forall>\<^sub>F n in F. \<forall>x\<in>S. dist (f n x) (l x) < b/2"
   10.40 +    using uniform_limitD [OF f, of "b/2"] by (simp add: \<open>b > 0\<close>)
   10.41 +  then have "\<forall>\<^sub>F x in F. \<forall>y\<in>S. b/2 \<le> norm (f x y)"
   10.42 +    apply (rule eventually_mono)
   10.43 +    using b apply (simp only: dist_norm)
   10.44 +    by (metis (no_types, hide_lams) diff_zero dist_commute dist_norm norm_triangle_half_l not_less)
   10.45 +  then have "\<forall>\<^sub>F x in F. \<forall>y\<in>S. b/2 \<le> norm (f x y) \<and> norm (f x y - l y) < e * b\<^sup>2 / 2"
   10.46 +    apply (simp only: ball_conj_distrib dist_norm [symmetric])
   10.47 +    apply (rule eventually_conj, assumption)
   10.48 +      apply (rule uniform_limitD [OF f, of "e * b ^ 2 / 2"])
   10.49 +    using \<open>b > 0\<close> \<open>e > 0\<close> by auto
   10.50 +  then show "\<forall>\<^sub>F x in F. \<forall>y\<in>S. dist (inverse (f x y)) ((inverse \<circ> l) y) < e"
   10.51 +    using lte by (force intro: eventually_mono)
   10.52 +qed
   10.53 +
   10.54 +lemma uniform_lim_div:
   10.55 +  fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'c::real_normed_field"
   10.56 +  assumes f: "uniform_limit S f l F"
   10.57 +      and g: "uniform_limit S g m F"
   10.58 +      and l: "bounded (l ` S)"
   10.59 +      and b: "\<And>x. x \<in> S \<Longrightarrow> b \<le> norm(m x)"
   10.60 +      and "b > 0"
   10.61 +    shows "uniform_limit S (\<lambda>a b. f a b / g a b) (\<lambda>a. l a / m a) F"
   10.62 +proof -
   10.63 +  have m: "bounded ((inverse \<circ> m) ` S)"
   10.64 +    using b \<open>b > 0\<close>
   10.65 +    apply (simp add: bounded_iff)
   10.66 +    by (metis le_imp_inverse_le norm_inverse)
   10.67 +  have "uniform_limit S (\<lambda>a b. f a b * inverse (g a b))
   10.68 +         (\<lambda>a. l a * (inverse \<circ> m) a) F"
   10.69 +    by (rule uniform_lim_mult [OF f uniform_lim_inverse [OF g b \<open>b > 0\<close>] l m])
   10.70 +  then show ?thesis
   10.71 +    by (simp add: field_class.field_divide_inverse)
   10.72 +qed
   10.73 +
   10.74  lemma uniform_limit_null_comparison:
   10.75    assumes "\<forall>\<^sub>F x in F. \<forall>a\<in>S. norm (f x a) \<le> g x a"
   10.76    assumes "uniform_limit S g (\<lambda>_. 0) F"
   10.77 @@ -482,7 +549,7 @@
   10.78      using assms(1) by (rule eventually_mono) (force simp add: dist_norm)
   10.79  qed
   10.80  
   10.81 -lemma uniform_limit_on_union:
   10.82 +lemma uniform_limit_on_Un:
   10.83    "uniform_limit I f g F \<Longrightarrow> uniform_limit J f g F \<Longrightarrow> uniform_limit (I \<union> J) f g F"
   10.84    by (auto intro!: uniform_limitI dest!: uniform_limitD elim: eventually_elim2)
   10.85  
   10.86 @@ -495,7 +562,7 @@
   10.87    assumes "\<And>s. s \<in> S \<Longrightarrow> uniform_limit (h s) f g F"
   10.88    shows "uniform_limit (UNION S h) f g F"
   10.89    using assms
   10.90 -  by induct (auto intro: uniform_limit_on_empty uniform_limit_on_union)
   10.91 +  by induct (auto intro: uniform_limit_on_empty uniform_limit_on_Un)
   10.92  
   10.93  lemma uniform_limit_on_Union:
   10.94    assumes "finite I"
   10.95 @@ -523,7 +590,6 @@
   10.96    unfolding uniformly_convergent_on_def
   10.97    by (blast dest: bounded_linear_uniform_limit_intros(13))
   10.98  
   10.99 -
  10.100  subsection\<open>Power series and uniform convergence\<close>
  10.101  
  10.102  proposition powser_uniformly_convergent:
    11.1 --- a/src/HOL/Limits.thy	Sun Feb 19 11:58:51 2017 +0100
    11.2 +++ b/src/HOL/Limits.thy	Tue Feb 21 15:04:01 2017 +0000
    11.3 @@ -1696,7 +1696,7 @@
    11.4    unfolding tendsto_def eventually_sequentially
    11.5    by (metis div_le_dividend div_mult_self1_is_m le_trans mult.commute)
    11.6  
    11.7 -lemma Bseq_inverse_lemma: "r \<le> norm x \<Longrightarrow> 0 < r \<Longrightarrow> norm (inverse x) \<le> inverse r"
    11.8 +lemma norm_inverse_le_norm: "r \<le> norm x \<Longrightarrow> 0 < r \<Longrightarrow> norm (inverse x) \<le> inverse r"
    11.9    for x :: "'a::real_normed_div_algebra"
   11.10    apply (subst nonzero_norm_inverse, clarsimp)
   11.11    apply (erule (1) le_imp_inverse_le)
    12.1 --- a/src/HOL/Real_Vector_Spaces.thy	Sun Feb 19 11:58:51 2017 +0100
    12.2 +++ b/src/HOL/Real_Vector_Spaces.thy	Tue Feb 21 15:04:01 2017 +0000
    12.3 @@ -1128,6 +1128,18 @@
    12.4  lemma dist_triangle_half_r: "dist y x1 < e / 2 \<Longrightarrow> dist y x2 < e / 2 \<Longrightarrow> dist x1 x2 < e"
    12.5    by (rule dist_triangle_half_l) (simp_all add: dist_commute)
    12.6  
    12.7 +lemma dist_triangle_third:
    12.8 +  assumes "dist x1 x2 < e/3" "dist x2 x3 < e/3" "dist x3 x4 < e/3"
    12.9 +  shows "dist x1 x4 < e"
   12.10 +proof -
   12.11 +  have "dist x1 x3 < e/3 + e/3"
   12.12 +    by (metis assms(1) assms(2) dist_commute dist_triangle_less_add)
   12.13 +  then have "dist x1 x4 < (e/3 + e/3) + e/3"
   12.14 +    by (metis assms(3) dist_commute dist_triangle_less_add)
   12.15 +  then show ?thesis
   12.16 +    by simp
   12.17 +qed
   12.18 +
   12.19  subclass uniform_space
   12.20  proof
   12.21    fix E x
    13.1 --- a/src/HOL/Topological_Spaces.thy	Sun Feb 19 11:58:51 2017 +0100
    13.2 +++ b/src/HOL/Topological_Spaces.thy	Tue Feb 21 15:04:01 2017 +0000
    13.3 @@ -468,9 +468,9 @@
    13.4    "eventually P (nhds a) \<longleftrightarrow> (\<exists>S. open S \<and> a \<in> S \<and> (\<forall>x\<in>S. P x))"
    13.5    unfolding nhds_def by (subst eventually_INF_base) (auto simp: eventually_principal)
    13.6  
    13.7 -lemma eventually_eventually: 
    13.8 +lemma eventually_eventually:
    13.9    "eventually (\<lambda>y. eventually P (nhds y)) (nhds x) = eventually P (nhds x)"
   13.10 -  by (auto simp: eventually_nhds)    
   13.11 +  by (auto simp: eventually_nhds)
   13.12  
   13.13  lemma (in topological_space) eventually_nhds_in_open:
   13.14    "open s \<Longrightarrow> x \<in> s \<Longrightarrow> eventually (\<lambda>y. y \<in> s) (nhds x)"
   13.15 @@ -1050,6 +1050,12 @@
   13.16  definition subseq :: "(nat \<Rightarrow> nat) \<Rightarrow> bool"
   13.17    where "subseq f \<longleftrightarrow> (\<forall>m. \<forall>n>m. f m < f n)"
   13.18  
   13.19 +lemma subseq_le_mono: "subseq r \<Longrightarrow> m \<le> n \<Longrightarrow> r m \<le> r n"
   13.20 +  by (simp add: less_mono_imp_le_mono subseq_def)
   13.21 +
   13.22 +lemma subseq_id: "subseq id"
   13.23 +  by (simp add: subseq_def)
   13.24 +
   13.25  lemma incseq_SucI: "(\<And>n. X n \<le> X (Suc n)) \<Longrightarrow> incseq X"
   13.26    using lift_Suc_mono_le[of X] by (auto simp: incseq_def)
   13.27  
   13.28 @@ -1818,6 +1824,12 @@
   13.29      by (rule continuous_on_closed_Un)
   13.30  qed
   13.31  
   13.32 +lemma continuous_on_cases:
   13.33 +  "closed s \<Longrightarrow> closed t \<Longrightarrow> continuous_on s f \<Longrightarrow> continuous_on t g \<Longrightarrow>
   13.34 +    \<forall>x. (x\<in>s \<and> \<not> P x) \<or> (x \<in> t \<and> P x) \<longrightarrow> f x = g x \<Longrightarrow>
   13.35 +    continuous_on (s \<union> t) (\<lambda>x. if P x then f x else g x)"
   13.36 +  by (rule continuous_on_If) auto
   13.37 +
   13.38  lemma continuous_on_id[continuous_intros]: "continuous_on s (\<lambda>x. x)"
   13.39    unfolding continuous_on_def by fast
   13.40  
    14.1 --- a/src/HOL/Transcendental.thy	Sun Feb 19 11:58:51 2017 +0100
    14.2 +++ b/src/HOL/Transcendental.thy	Tue Feb 21 15:04:01 2017 +0000
    14.3 @@ -3194,6 +3194,12 @@
    14.4  lemma diffs_cos_coeff: "diffs cos_coeff = (\<lambda>n. - sin_coeff n)"
    14.5    by (simp add: diffs_def cos_coeff_Suc del: of_nat_Suc)
    14.6  
    14.7 +lemma sin_int_times_real: "sin (of_int m * of_real x) = of_real (sin (of_int m * x))"
    14.8 +  by (metis sin_of_real of_real_mult of_real_of_int_eq)
    14.9 +
   14.10 +lemma cos_int_times_real: "cos (of_int m * of_real x) = of_real (cos (of_int m * x))"
   14.11 +  by (metis cos_of_real of_real_mult of_real_of_int_eq)
   14.12 +
   14.13  text \<open>Now at last we can get the derivatives of exp, sin and cos.\<close>
   14.14  
   14.15  lemma DERIV_sin [simp]: "DERIV sin x :> cos x"
   14.16 @@ -4077,6 +4083,9 @@
   14.17    using dvd_triv_left apply fastforce
   14.18    done
   14.19  
   14.20 +lemma sin_npi_int [simp]: "sin (pi * of_int n) = 0"
   14.21 +  by (simp add: sin_zero_iff_int2)
   14.22 +
   14.23  lemma cos_monotone_0_pi:
   14.24    assumes "0 \<le> y" and "y < x" and "x \<le> pi"
   14.25    shows "cos x < cos y"
   14.26 @@ -4271,13 +4280,23 @@
   14.27      by (metis cos_2npi cos_minus mult.assoc mult.left_commute)
   14.28  qed
   14.29  
   14.30 -lemma cos_one_2pi_int: "cos x = 1 \<longleftrightarrow> (\<exists>n::int. x = n * 2 * pi)"
   14.31 -  apply auto  (* FIXME simproc bug? *)
   14.32 -   apply (auto simp: cos_one_2pi)
   14.33 -    apply (metis of_int_of_nat_eq)
   14.34 -   apply (metis mult_minus_right of_int_minus of_int_of_nat_eq)
   14.35 -  apply (metis mult_minus_right of_int_of_nat)
   14.36 -  done
   14.37 +lemma cos_one_2pi_int: "cos x = 1 \<longleftrightarrow> (\<exists>n::int. x = n * 2 * pi)" (is "?lhs = ?rhs")
   14.38 +proof
   14.39 +  assume "cos x = 1"
   14.40 +  then show ?rhs
   14.41 +    apply (auto simp: cos_one_2pi)
   14.42 +     apply (metis of_int_of_nat_eq)
   14.43 +    apply (metis mult_minus_right of_int_minus of_int_of_nat_eq)
   14.44 +    done
   14.45 +next
   14.46 +  assume ?rhs
   14.47 +  then show "cos x = 1"
   14.48 +    by (clarsimp simp add: cos_one_2pi) (metis mult_minus_right of_int_of_nat)
   14.49 +qed
   14.50 +
   14.51 +lemma cos_npi_int [simp]:
   14.52 +  fixes n::int shows "cos (pi * of_int n) = (if even n then 1 else -1)"
   14.53 +    by (auto simp: algebra_simps cos_one_2pi_int elim!: oddE evenE)
   14.54  
   14.55  lemma sin_cos_sqrt: "0 \<le> sin x \<Longrightarrow> sin x = sqrt (1 - (cos(x) ^ 2))"
   14.56    using sin_squared_eq real_sqrt_unique by fastforce