src/HOL/Analysis/Cauchy_Integral_Theorem.thy
changeset 68420 529d6b132c27
parent 68403 223172b97d0b
child 68493 143b4cc8fc74
     1.1 --- a/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Sat Jun 09 21:52:16 2018 +0200
     1.2 +++ b/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Mon Jun 11 22:43:33 2018 +0100
     1.3 @@ -6338,12 +6338,10 @@
     1.4    have 1: "(\<lambda>z. \<Sum>i\<le>n. a i * z^i) holomorphic_on UNIV"
     1.5      by (rule holomorphic_intros)+
     1.6    show thesis
     1.7 -    apply (rule Liouville_weak_inverse [OF 1])
     1.8 -    apply (rule polyfun_extremal)
     1.9 -    apply (rule nz)
    1.10 -    using i that
    1.11 -    apply auto
    1.12 -    done
    1.13 +  proof (rule Liouville_weak_inverse [OF 1])
    1.14 +    show "\<forall>\<^sub>F x in at_infinity. B \<le> cmod (\<Sum>i\<le>n. a i * x ^ i)" for B
    1.15 +      using i polyfun_extremal nz by force
    1.16 +  qed (use that in auto)
    1.17  qed
    1.18  
    1.19  
    1.20 @@ -6358,14 +6356,15 @@
    1.21    case less then show ?thesis by (force simp: ball_empty less_imp_le continuous_on_def holomorphic_on_def intro: that)
    1.22  next
    1.23    case equal then show ?thesis
    1.24 -    by (force simp: holomorphic_on_def continuous_on_sing intro: that)
    1.25 +    by (force simp: holomorphic_on_def intro: that)
    1.26  next
    1.27    case greater
    1.28    have contg: "continuous_on (cball z r) g"
    1.29      using cont uniform_limit_theorem [OF eventually_mono ulim F]  by blast
    1.30 -  have 1: "continuous_on (path_image (circlepath z r)) (\<lambda>x. 1 / (2 * complex_of_real pi * \<i>) * g x)"
    1.31 -    apply (rule continuous_intros continuous_on_subset [OF contg])+
    1.32 +  have "path_image (circlepath z r) \<subseteq> cball z r"
    1.33      using \<open>0 < r\<close> by auto
    1.34 +  then have 1: "continuous_on (path_image (circlepath z r)) (\<lambda>x. 1 / (2 * complex_of_real pi * \<i>) * g x)"
    1.35 +    by (intro continuous_intros continuous_on_subset [OF contg])
    1.36    have 2: "((\<lambda>u. 1 / (2 * of_real pi * \<i>) * g u / (u - w) ^ 1) has_contour_integral g w) (circlepath z r)"
    1.37         if w: "w \<in> ball z r" for w
    1.38    proof -
    1.39 @@ -6389,18 +6388,16 @@
    1.40      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"
    1.41        by (rule contour_integral_uniform_limit_circlepath [OF ev_int ul_less F \<open>0 < r\<close>])
    1.42      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"
    1.43 -      apply (rule Lim_transform_eventually [where f = "\<lambda>n. contour_integral (circlepath z r) (\<lambda>u. f n u/(u - w))"])
    1.44 -      apply (rule eventually_mono [OF cont])
    1.45 -      apply (rule contour_integral_unique [OF Cauchy_integral_circlepath])
    1.46 -      using w
    1.47 -      apply (auto simp: norm_minus_commute dist_norm cif_tends_cig)
    1.48 -      done
    1.49 -    have "((\<lambda>n. 2 * of_real pi * \<i> * f n w) \<longlongrightarrow> 2 * of_real pi * \<i> * g w) F"
    1.50 -      apply (rule tendsto_mult_left [OF tendstoI])
    1.51 -      apply (rule eventually_mono [OF uniform_limitD [OF ulim]], assumption)
    1.52 -      using w
    1.53 -      apply (force simp: dist_norm)
    1.54 -      done
    1.55 +    proof (rule Lim_transform_eventually)
    1.56 +      show "\<forall>\<^sub>F x in F. contour_integral (circlepath z r) (\<lambda>u. f x u / (u - w)) 
    1.57 +                     = 2 * of_real pi * \<i> * f x w"
    1.58 +        apply (rule eventually_mono [OF cont contour_integral_unique [OF Cauchy_integral_circlepath]])
    1.59 +        using w\<open>0 < d\<close> d_def by auto
    1.60 +    qed (auto simp: cif_tends_cig)
    1.61 +    have "\<And>e. 0 < e \<Longrightarrow> \<forall>\<^sub>F n in F. dist (f n w) (g w) < e"
    1.62 +      by (rule eventually_mono [OF uniform_limitD [OF ulim]]) (use w in auto)
    1.63 +    then have "((\<lambda>n. 2 * of_real pi * \<i> * f n w) \<longlongrightarrow> 2 * of_real pi * \<i> * g w) F"
    1.64 +      by (rule tendsto_mult_left [OF tendstoI])
    1.65      then have "((\<lambda>u. g u / (u - w)) has_contour_integral 2 * of_real pi * \<i> * g w) (circlepath z r)"
    1.66        using has_contour_integral_integral [OF g_cint] tendsto_unique [OF F f_tends_cig] w
    1.67        by (force simp: dist_norm)
    1.68 @@ -6455,12 +6452,17 @@
    1.69      define d where "d = (r - norm(w - z))^2"
    1.70      have "d > 0"
    1.71        using w by (simp add: dist_commute dist_norm d_def)
    1.72 -    have dle: "\<And>y. r = cmod (z - y) \<Longrightarrow> d \<le> cmod ((y - w)\<^sup>2)"
    1.73 -      apply (simp add: d_def norm_power)
    1.74 -      apply (rule power_mono)
    1.75 -      apply (metis add_diff_eq diff_add_cancel norm_diff_ineq norm_minus_commute)
    1.76 -      apply (metis diff_ge_0_iff_ge dist_commute dist_norm less_eq_real_def mem_ball w)
    1.77 -      done
    1.78 +    have dle: "d \<le> cmod ((y - w)\<^sup>2)" if "r = cmod (z - y)" for y
    1.79 +    proof -
    1.80 +      have "w \<in> ball z (cmod (z - y))"
    1.81 +        using that w by fastforce
    1.82 +      then have "cmod (w - z) \<le> cmod (z - y)"
    1.83 +        by (simp add: dist_complex_def norm_minus_commute)
    1.84 +      moreover have "cmod (z - y) - cmod (w - z) \<le> cmod (y - w)"
    1.85 +        by (metis diff_add_cancel diff_add_eq_diff_diff_swap norm_minus_commute norm_triangle_ineq2)
    1.86 +      ultimately show ?thesis
    1.87 +        using that by (simp add: d_def norm_power power_mono)
    1.88 +    qed
    1.89      have 1: "\<forall>\<^sub>F n in F. (\<lambda>x. f n x / (x - w)\<^sup>2) contour_integrable_on circlepath z r"
    1.90        by (force simp: holomorphic_on_open intro: w Cauchy_derivative_integral_circlepath eventually_mono [OF cont])
    1.91      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"
    1.92 @@ -6468,9 +6470,8 @@
    1.93      proof clarify
    1.94        fix e::real
    1.95        assume "0 < e"
    1.96 -      with  \<open>r > 0\<close>
    1.97 -      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"
    1.98 -        apply (simp add: diff_divide_distrib [symmetric] norm_divide divide_simps sphere_def dist_norm)
    1.99 +      with \<open>r > 0\<close> 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"
   1.100 +        apply (simp add: norm_divide divide_simps sphere_def dist_norm)
   1.101          apply (rule eventually_mono [OF uniform_limitD [OF ulim], of "e*d"])
   1.102           apply (simp add: \<open>0 < d\<close>)
   1.103          apply (force simp: dist_norm dle intro: less_le_trans)
   1.104 @@ -6508,10 +6509,12 @@
   1.105                 and ul: "uniform_limit (cball z r) f g sequentially"
   1.106        using ulim_g [OF \<open>z \<in> S\<close>] by blast 
   1.107      have *: "\<forall>\<^sub>F n in sequentially. continuous_on (cball z r) (f n) \<and> f n holomorphic_on ball z r"
   1.108 -      apply (intro eventuallyI conjI)
   1.109 -      using hol_fn holomorphic_on_imp_continuous_on holomorphic_on_subset r apply blast
   1.110 -      apply (metis hol_fn holomorphic_on_subset interior_cball interior_subset r)
   1.111 -      done
   1.112 +    proof (intro eventuallyI conjI)
   1.113 +      show "continuous_on (cball z r) (f x)" for x
   1.114 +        using hol_fn holomorphic_on_imp_continuous_on holomorphic_on_subset r by blast
   1.115 +      show "f x holomorphic_on ball z r" for x
   1.116 +        by (metis hol_fn holomorphic_on_subset interior_cball interior_subset r)
   1.117 +    qed
   1.118      show ?thesis
   1.119        apply (rule holomorphic_uniform_limit [OF *])
   1.120        using \<open>0 < r\<close> centre_in_ball ul
   1.121 @@ -6537,15 +6540,14 @@
   1.122        using ulim_g [OF \<open>z \<in> S\<close>] by blast 
   1.123      have *: "\<forall>\<^sub>F n in sequentially. continuous_on (cball z r) (f n) \<and>
   1.124                                     (\<forall>w \<in> ball z r. ((f n) has_field_derivative (f' n w)) (at w))"
   1.125 -      apply (intro eventuallyI conjI)
   1.126 -      apply (meson hfd holomorphic_on_imp_continuous_on holomorphic_on_open holomorphic_on_subset r S)
   1.127 -      using ball_subset_cball hfd r apply blast
   1.128 -      done
   1.129 +    proof (intro eventuallyI conjI ballI)
   1.130 +      show "continuous_on (cball z r) (f x)" for x
   1.131 +        by (meson S continuous_on_subset hfd holomorphic_on_imp_continuous_on holomorphic_on_open r)
   1.132 +      show "w \<in> ball z r \<Longrightarrow> (f x has_field_derivative f' x w) (at w)" for w x
   1.133 +        using ball_subset_cball hfd r by blast
   1.134 +    qed
   1.135      show ?thesis
   1.136 -      apply (rule has_complex_derivative_uniform_limit [OF *, of g])
   1.137 -      using \<open>0 < r\<close> centre_in_ball ul
   1.138 -      apply force+
   1.139 -      done
   1.140 +      by (rule has_complex_derivative_uniform_limit [OF *, of g]) (use \<open>0 < r\<close> ul in \<open>force+\<close>)
   1.141    qed
   1.142    show ?thesis
   1.143      by (rule bchoice) (blast intro: y)
   1.144 @@ -6569,11 +6571,11 @@
   1.145    proof -
   1.146      obtain d where "d>0" and d: "cball x d \<subseteq> S"
   1.147        using open_contains_cball [of "S"] \<open>x \<in> S\<close> S by blast
   1.148 -    then show ?thesis
   1.149 -      apply (rule_tac x=d in exI)
   1.150 -        using g uniform_limit_on_subset
   1.151 -        apply (force simp: dist_norm eventually_sequentially)
   1.152 -          done
   1.153 +    show ?thesis
   1.154 +    proof (intro conjI exI)
   1.155 +      show "uniform_limit (cball x d) (\<lambda>n x. \<Sum>i<n. f i x) g sequentially"
   1.156 +        using d g uniform_limit_on_subset by (force simp: dist_norm eventually_sequentially)
   1.157 +    qed (use \<open>d > 0\<close> d in auto)
   1.158    qed
   1.159    have "\<And>x. x \<in> S \<Longrightarrow> (\<lambda>n. \<Sum>i<n. f i x) \<longlonglongrightarrow> g x"
   1.160      by (metis tendsto_uniform_limitI [OF g])
   1.161 @@ -6612,14 +6614,14 @@
   1.162        using  summable_sums centre_in_ball \<open>0 < d\<close> \<open>summable h\<close> le_h
   1.163        by (metis (full_types) Int_iff gg' summable_def that)
   1.164      moreover have "((\<lambda>x. \<Sum>n. f n x) has_field_derivative g' z) (at z)"
   1.165 -      apply (rule_tac f=g in DERIV_transform_at [OF _ \<open>0 < r\<close>])
   1.166 -      apply (simp add: gg' \<open>z \<in> S\<close> \<open>0 < d\<close>)
   1.167 -      apply (metis (full_types) contra_subsetD dist_commute gg' mem_ball r sums_unique)
   1.168 -      done
   1.169 +    proof (rule DERIV_transform_at)
   1.170 +      show "\<And>x. dist x z < r \<Longrightarrow> g x = (\<Sum>n. f n x)"
   1.171 +        by (metis subsetD dist_commute gg' mem_ball r sums_unique)
   1.172 +    qed (use \<open>0 < r\<close> gg' \<open>z \<in> S\<close> \<open>0 < d\<close> in auto)
   1.173      ultimately show ?thesis by auto
   1.174    qed
   1.175    then show ?thesis
   1.176 -    by (rule_tac x="\<lambda>x. suminf  (\<lambda>n. f n x)" in exI) meson
   1.177 +    by (rule_tac x="\<lambda>x. suminf (\<lambda>n. f n x)" in exI) meson
   1.178  qed
   1.179  
   1.180  
   1.181 @@ -6682,12 +6684,9 @@
   1.182                 (\<lambda>n. of_nat n * (a n) * z ^ (n - 1)) sums g' z \<and> (g has_field_derivative g' z) (at z)"
   1.183        apply (rule series_and_derivative_comparison_complex [OF open_ball der])
   1.184        apply (rule_tac x="(r - norm z)/2" in exI)
   1.185 -      apply (simp add: dist_norm)
   1.186        apply (rule_tac x="\<lambda>n. of_real(norm(a n)*((r + norm z)/2)^n)" in exI)
   1.187        using \<open>r > 0\<close>
   1.188 -      apply (auto simp: sum eventually_sequentially norm_mult norm_divide norm_power)
   1.189 -      apply (rule_tac x=0 in exI)
   1.190 -      apply (force simp: dist_norm intro!: mult_left_mono power_mono y_le)
   1.191 +      apply (auto simp: sum eventually_sequentially norm_mult norm_power dist_norm intro!: mult_left_mono power_mono y_le)
   1.192        done
   1.193    then show ?thesis
   1.194      by (simp add: ball_def)
   1.195 @@ -6742,12 +6741,10 @@
   1.196          apply (auto simp: assms dist_norm)
   1.197          done
   1.198      qed
   1.199 -    show ?thesis
   1.200 -      apply (rule_tac x="g' w" in exI)
   1.201 -      apply (rule DERIV_transform_at [where f=g and d="(r - norm(z - w))/2"])
   1.202 -      using w gg' [of w]
   1.203 -      apply (auto simp: dist_norm)
   1.204 -      done
   1.205 +    have "(f has_field_derivative g' w) (at w)"
   1.206 +      by (rule DERIV_transform_at [where d="(r - norm(z - w))/2"])
   1.207 +      (use w gg' [of w] in \<open>(force simp: dist_norm)+\<close>)
   1.208 +    then show ?thesis ..
   1.209    qed
   1.210    then show ?thesis by (simp add: holomorphic_on_open)
   1.211  qed
   1.212 @@ -6755,10 +6752,8 @@
   1.213  corollary holomorphic_iff_power_series:
   1.214       "f holomorphic_on ball z r \<longleftrightarrow>
   1.215        (\<forall>w \<in> ball z r. (\<lambda>n. (deriv ^^ n) f z / (fact n) * (w - z)^n) sums f w)"
   1.216 -  apply (intro iffI ballI)
   1.217 -   using holomorphic_power_series  apply force
   1.218 -  apply (rule power_series_holomorphic [where a = "\<lambda>n. (deriv ^^ n) f z / (fact n)"])
   1.219 -  apply force
   1.220 +  apply (intro iffI ballI holomorphic_power_series, assumption+)
   1.221 +  apply (force intro: power_series_holomorphic [where a = "\<lambda>n. (deriv ^^ n) f z / (fact n)"])
   1.222    done
   1.223  
   1.224  corollary power_series_analytic:
   1.225 @@ -6791,102 +6786,104 @@
   1.226    done
   1.227  
   1.228  lemma holomorphic_fun_eq_0_on_connected:
   1.229 -  assumes holf: "f holomorphic_on s" and "open s"
   1.230 -      and cons: "connected s"
   1.231 +  assumes holf: "f holomorphic_on S" and "open S"
   1.232 +      and cons: "connected S"
   1.233        and der: "\<And>n. (deriv ^^ n) f z = 0"
   1.234 -      and "z \<in> s" "w \<in> s"
   1.235 +      and "z \<in> S" "w \<in> S"
   1.236      shows "f w = 0"
   1.237  proof -
   1.238 -  have *: "\<And>x e. \<lbrakk> \<forall>xa. (deriv ^^ xa) f x = 0;  ball x e \<subseteq> s\<rbrakk>
   1.239 -           \<Longrightarrow> ball x e \<subseteq> (\<Inter>n. {w \<in> s. (deriv ^^ n) f w = 0})"
   1.240 -    apply auto
   1.241 -    apply (rule holomorphic_fun_eq_0_on_ball [OF holomorphic_higher_deriv])
   1.242 -    apply (rule holomorphic_on_subset [OF holf], simp_all)
   1.243 -    by (metis funpow_add o_apply)
   1.244 -  have 1: "openin (subtopology euclidean s) (\<Inter>n. {w \<in> s. (deriv ^^ n) f w = 0})"
   1.245 +  have *: "ball x e \<subseteq> (\<Inter>n. {w \<in> S. (deriv ^^ n) f w = 0})"
   1.246 +    if "\<forall>u. (deriv ^^ u) f x = 0" "ball x e \<subseteq> S" for x e
   1.247 +  proof -
   1.248 +    have "\<And>x' n. dist x x' < e \<Longrightarrow> (deriv ^^ n) f x' = 0"
   1.249 +      apply (rule holomorphic_fun_eq_0_on_ball [OF holomorphic_higher_deriv])
   1.250 +         apply (rule holomorphic_on_subset [OF holf])
   1.251 +      using that apply simp_all
   1.252 +      by (metis funpow_add o_apply)
   1.253 +    with that show ?thesis by auto
   1.254 +  qed
   1.255 +  have 1: "openin (subtopology euclidean S) (\<Inter>n. {w \<in> S. (deriv ^^ n) f w = 0})"
   1.256      apply (rule open_subset, force)
   1.257 -    using \<open>open s\<close>
   1.258 +    using \<open>open S\<close>
   1.259      apply (simp add: open_contains_ball Ball_def)
   1.260      apply (erule all_forward)
   1.261      using "*" by auto blast+
   1.262 -  have 2: "closedin (subtopology euclidean s) (\<Inter>n. {w \<in> s. (deriv ^^ n) f w = 0})"
   1.263 +  have 2: "closedin (subtopology euclidean S) (\<Inter>n. {w \<in> S. (deriv ^^ n) f w = 0})"
   1.264      using assms
   1.265      by (auto intro: continuous_closedin_preimage_constant holomorphic_on_imp_continuous_on holomorphic_higher_deriv)
   1.266 -  obtain e where "e>0" and e: "ball w e \<subseteq> s" using openE [OF \<open>open s\<close> \<open>w \<in> s\<close>] .
   1.267 +  obtain e where "e>0" and e: "ball w e \<subseteq> S" using openE [OF \<open>open S\<close> \<open>w \<in> S\<close>] .
   1.268    then have holfb: "f holomorphic_on ball w e"
   1.269      using holf holomorphic_on_subset by blast
   1.270 -  have 3: "(\<Inter>n. {w \<in> s. (deriv ^^ n) f w = 0}) = s \<Longrightarrow> f w = 0"
   1.271 +  have 3: "(\<Inter>n. {w \<in> S. (deriv ^^ n) f w = 0}) = S \<Longrightarrow> f w = 0"
   1.272      using \<open>e>0\<close> e by (force intro: holomorphic_fun_eq_0_on_ball [OF holfb])
   1.273    show ?thesis
   1.274 -    using cons der \<open>z \<in> s\<close>
   1.275 +    using cons der \<open>z \<in> S\<close>
   1.276      apply (simp add: connected_clopen)
   1.277 -    apply (drule_tac x="\<Inter>n. {w \<in> s. (deriv ^^ n) f w = 0}" in spec)
   1.278 +    apply (drule_tac x="\<Inter>n. {w \<in> S. (deriv ^^ n) f w = 0}" in spec)
   1.279      apply (auto simp: 1 2 3)
   1.280      done
   1.281  qed
   1.282  
   1.283  lemma holomorphic_fun_eq_on_connected:
   1.284 -  assumes "f holomorphic_on s" "g holomorphic_on s" and "open s"  "connected s"
   1.285 +  assumes "f holomorphic_on S" "g holomorphic_on S" and "open S"  "connected S"
   1.286        and "\<And>n. (deriv ^^ n) f z = (deriv ^^ n) g z"
   1.287 -      and "z \<in> s" "w \<in> s"
   1.288 +      and "z \<in> S" "w \<in> S"
   1.289      shows "f w = g w"
   1.290 -  apply (rule holomorphic_fun_eq_0_on_connected [of "\<lambda>x. f x - g x" s z, simplified])
   1.291 -  apply (intro assms holomorphic_intros)
   1.292 -  using assms apply simp_all
   1.293 -  apply (subst higher_deriv_diff, auto)
   1.294 -  done
   1.295 +proof (rule holomorphic_fun_eq_0_on_connected [of "\<lambda>x. f x - g x" S z, simplified])
   1.296 +  show "(\<lambda>x. f x - g x) holomorphic_on S"
   1.297 +    by (intro assms holomorphic_intros)
   1.298 +  show "\<And>n. (deriv ^^ n) (\<lambda>x. f x - g x) z = 0"
   1.299 +    using assms higher_deriv_diff by auto
   1.300 +qed (use assms in auto)
   1.301  
   1.302  lemma holomorphic_fun_eq_const_on_connected:
   1.303 -  assumes holf: "f holomorphic_on s" and "open s"
   1.304 -      and cons: "connected s"
   1.305 +  assumes holf: "f holomorphic_on S" and "open S"
   1.306 +      and cons: "connected S"
   1.307        and der: "\<And>n. 0 < n \<Longrightarrow> (deriv ^^ n) f z = 0"
   1.308 -      and "z \<in> s" "w \<in> s"
   1.309 +      and "z \<in> S" "w \<in> S"
   1.310      shows "f w = f z"
   1.311 -  apply (rule holomorphic_fun_eq_0_on_connected [of "\<lambda>w. f w - f z" s z, simplified])
   1.312 -  apply (intro assms holomorphic_intros)
   1.313 -  using assms apply simp_all
   1.314 -  apply (subst higher_deriv_diff)
   1.315 -  apply (intro holomorphic_intros | simp)+
   1.316 -  done
   1.317 -
   1.318 +proof (rule holomorphic_fun_eq_0_on_connected [of "\<lambda>w. f w - f z" S z, simplified])
   1.319 +  show "(\<lambda>w. f w - f z) holomorphic_on S"
   1.320 +    by (intro assms holomorphic_intros)
   1.321 +  show "\<And>n. (deriv ^^ n) (\<lambda>w. f w - f z) z = 0"
   1.322 +    by (subst higher_deriv_diff) (use assms in \<open>auto intro: holomorphic_intros\<close>)
   1.323 +qed (use assms in auto)
   1.324  
   1.325  subsection\<open>Some basic lemmas about poles/singularities\<close>
   1.326  
   1.327  lemma pole_lemma:
   1.328 -  assumes holf: "f holomorphic_on s" and a: "a \<in> interior s"
   1.329 +  assumes holf: "f holomorphic_on S" and a: "a \<in> interior S"
   1.330      shows "(\<lambda>z. if z = a then deriv f a
   1.331 -                 else (f z - f a) / (z - a)) holomorphic_on s" (is "?F holomorphic_on s")
   1.332 +                 else (f z - f a) / (z - a)) holomorphic_on S" (is "?F holomorphic_on S")
   1.333  proof -
   1.334 -  have F1: "?F field_differentiable (at u within s)" if "u \<in> s" "u \<noteq> a" for u
   1.335 +  have F1: "?F field_differentiable (at u within S)" if "u \<in> S" "u \<noteq> a" for u
   1.336    proof -
   1.337 -    have fcd: "f field_differentiable at u within s"
   1.338 -      using holf holomorphic_on_def by (simp add: \<open>u \<in> s\<close>)
   1.339 -    have cd: "(\<lambda>z. (f z - f a) / (z - a)) field_differentiable at u within s"
   1.340 +    have fcd: "f field_differentiable at u within S"
   1.341 +      using holf holomorphic_on_def by (simp add: \<open>u \<in> S\<close>)
   1.342 +    have cd: "(\<lambda>z. (f z - f a) / (z - a)) field_differentiable at u within S"
   1.343        by (rule fcd derivative_intros | simp add: that)+
   1.344      have "0 < dist a u" using that dist_nz by blast
   1.345      then show ?thesis
   1.346 -      by (rule field_differentiable_transform_within [OF _ _ _ cd]) (auto simp: \<open>u \<in> s\<close>)
   1.347 +      by (rule field_differentiable_transform_within [OF _ _ _ cd]) (auto simp: \<open>u \<in> S\<close>)
   1.348    qed
   1.349 -  have F2: "?F field_differentiable at a" if "0 < e" "ball a e \<subseteq> s" for e
   1.350 +  have F2: "?F field_differentiable at a" if "0 < e" "ball a e \<subseteq> S" for e
   1.351    proof -
   1.352      have holfb: "f holomorphic_on ball a e"
   1.353 -      by (rule holomorphic_on_subset [OF holf \<open>ball a e \<subseteq> s\<close>])
   1.354 +      by (rule holomorphic_on_subset [OF holf \<open>ball a e \<subseteq> S\<close>])
   1.355      have 2: "?F holomorphic_on ball a e - {a}"
   1.356 -      apply (rule holomorphic_on_subset [where s = "s - {a}"])
   1.357 -      apply (simp add: holomorphic_on_def field_differentiable_def [symmetric])
   1.358 +      apply (simp add: holomorphic_on_def flip: field_differentiable_def)
   1.359        using mem_ball that
   1.360        apply (auto intro: F1 field_differentiable_within_subset)
   1.361        done
   1.362      have "isCont (\<lambda>z. if z = a then deriv f a else (f z - f a) / (z - a)) x"
   1.363              if "dist a x < e" for x
   1.364      proof (cases "x=a")
   1.365 -      case True then show ?thesis
   1.366 -      using holfb \<open>0 < e\<close>
   1.367 -      apply (simp add: holomorphic_on_open field_differentiable_def [symmetric])
   1.368 -      apply (drule_tac x=a in bspec)
   1.369 -      apply (auto simp: DERIV_deriv_iff_field_differentiable [symmetric] continuous_at DERIV_iff2
   1.370 +      case True 
   1.371 +      then have "f field_differentiable at a"
   1.372 +        using holfb \<open>0 < e\<close> holomorphic_on_imp_differentiable_at by auto
   1.373 +      with True show ?thesis
   1.374 +        by (auto simp: continuous_at DERIV_iff2 simp flip: DERIV_deriv_iff_field_differentiable
   1.375                  elim: rev_iffD1 [OF _ LIM_equal])
   1.376 -      done
   1.377      next
   1.378        case False with 2 that show ?thesis
   1.379          by (force simp: holomorphic_on_open open_Diff field_differentiable_def [symmetric] field_differentiable_imp_continuous_at)
   1.380 @@ -6901,29 +6898,29 @@
   1.381    qed
   1.382    show ?thesis
   1.383    proof
   1.384 -    fix x assume "x \<in> s" show "?F field_differentiable at x within s"
   1.385 +    fix x assume "x \<in> S" show "?F field_differentiable at x within S"
   1.386      proof (cases "x=a")
   1.387        case True then show ?thesis
   1.388        using a by (auto simp: mem_interior intro: field_differentiable_at_within F2)
   1.389      next
   1.390 -      case False with F1 \<open>x \<in> s\<close>
   1.391 +      case False with F1 \<open>x \<in> S\<close>
   1.392        show ?thesis by blast
   1.393      qed
   1.394    qed
   1.395  qed
   1.396  
   1.397  proposition pole_theorem:
   1.398 -  assumes holg: "g holomorphic_on s" and a: "a \<in> interior s"
   1.399 -      and eq: "\<And>z. z \<in> s - {a} \<Longrightarrow> g z = (z - a) * f z"
   1.400 +  assumes holg: "g holomorphic_on S" and a: "a \<in> interior S"
   1.401 +      and eq: "\<And>z. z \<in> S - {a} \<Longrightarrow> g z = (z - a) * f z"
   1.402      shows "(\<lambda>z. if z = a then deriv g a
   1.403 -                 else f z - g a/(z - a)) holomorphic_on s"
   1.404 +                 else f z - g a/(z - a)) holomorphic_on S"
   1.405    using pole_lemma [OF holg a]
   1.406    by (rule holomorphic_transform) (simp add: eq divide_simps)
   1.407  
   1.408  lemma pole_lemma_open:
   1.409 -  assumes "f holomorphic_on s" "open s"
   1.410 -    shows "(\<lambda>z. if z = a then deriv f a else (f z - f a)/(z - a)) holomorphic_on s"
   1.411 -proof (cases "a \<in> s")
   1.412 +  assumes "f holomorphic_on S" "open S"
   1.413 +    shows "(\<lambda>z. if z = a then deriv f a else (f z - f a)/(z - a)) holomorphic_on S"
   1.414 +proof (cases "a \<in> S")
   1.415    case True with assms interior_eq pole_lemma
   1.416      show ?thesis by fastforce
   1.417  next
   1.418 @@ -6935,48 +6932,53 @@
   1.419  qed
   1.420  
   1.421  proposition pole_theorem_open:
   1.422 -  assumes holg: "g holomorphic_on s" and s: "open s"
   1.423 -      and eq: "\<And>z. z \<in> s - {a} \<Longrightarrow> g z = (z - a) * f z"
   1.424 +  assumes holg: "g holomorphic_on S" and S: "open S"
   1.425 +      and eq: "\<And>z. z \<in> S - {a} \<Longrightarrow> g z = (z - a) * f z"
   1.426      shows "(\<lambda>z. if z = a then deriv g a
   1.427 -                 else f z - g a/(z - a)) holomorphic_on s"
   1.428 -  using pole_lemma_open [OF holg s]
   1.429 +                 else f z - g a/(z - a)) holomorphic_on S"
   1.430 +  using pole_lemma_open [OF holg S]
   1.431    by (rule holomorphic_transform) (auto simp: eq divide_simps)
   1.432  
   1.433  proposition pole_theorem_0:
   1.434 -  assumes holg: "g holomorphic_on s" and a: "a \<in> interior s"
   1.435 -      and eq: "\<And>z. z \<in> s - {a} \<Longrightarrow> g z = (z - a) * f z"
   1.436 +  assumes holg: "g holomorphic_on S" and a: "a \<in> interior S"
   1.437 +      and eq: "\<And>z. z \<in> S - {a} \<Longrightarrow> g z = (z - a) * f z"
   1.438        and [simp]: "f a = deriv g a" "g a = 0"
   1.439 -    shows "f holomorphic_on s"
   1.440 +    shows "f holomorphic_on S"
   1.441    using pole_theorem [OF holg a eq]
   1.442    by (rule holomorphic_transform) (auto simp: eq divide_simps)
   1.443  
   1.444  proposition pole_theorem_open_0:
   1.445 -  assumes holg: "g holomorphic_on s" and s: "open s"
   1.446 -      and eq: "\<And>z. z \<in> s - {a} \<Longrightarrow> g z = (z - a) * f z"
   1.447 +  assumes holg: "g holomorphic_on S" and S: "open S"
   1.448 +      and eq: "\<And>z. z \<in> S - {a} \<Longrightarrow> g z = (z - a) * f z"
   1.449        and [simp]: "f a = deriv g a" "g a = 0"
   1.450 -    shows "f holomorphic_on s"
   1.451 -  using pole_theorem_open [OF holg s eq]
   1.452 +    shows "f holomorphic_on S"
   1.453 +  using pole_theorem_open [OF holg S eq]
   1.454    by (rule holomorphic_transform) (auto simp: eq divide_simps)
   1.455  
   1.456  lemma pole_theorem_analytic:
   1.457 -  assumes g: "g analytic_on s"
   1.458 -      and eq: "\<And>z. z \<in> s
   1.459 +  assumes g: "g analytic_on S"
   1.460 +      and eq: "\<And>z. z \<in> S
   1.461               \<Longrightarrow> \<exists>d. 0 < d \<and> (\<forall>w \<in> ball z d - {a}. g w = (w - a) * f w)"
   1.462 -    shows "(\<lambda>z. if z = a then deriv g a
   1.463 -                 else f z - g a/(z - a)) analytic_on s"
   1.464 -using g
   1.465 -apply (simp add: analytic_on_def Ball_def)
   1.466 -apply (safe elim!: all_forward dest!: eq)
   1.467 -apply (rule_tac x="min d e" in exI, simp)
   1.468 -apply (rule pole_theorem_open)
   1.469 -apply (auto simp: holomorphic_on_subset subset_ball)
   1.470 -done
   1.471 +    shows "(\<lambda>z. if z = a then deriv g a else f z - g a/(z - a)) analytic_on S" (is "?F analytic_on S")
   1.472 +  unfolding analytic_on_def
   1.473 +proof 
   1.474 +  fix x
   1.475 +  assume "x \<in> S"
   1.476 +  with g obtain e where "0 < e" and e: "g holomorphic_on ball x e" 
   1.477 +    by (auto simp add: analytic_on_def)
   1.478 +  obtain d where "0 < d" and d: "\<And>w. w \<in> ball x d - {a} \<Longrightarrow> g w = (w - a) * f w"
   1.479 +    using \<open>x \<in> S\<close> eq by blast
   1.480 +  have "?F holomorphic_on ball x (min d e)"
   1.481 +    using d e \<open>x \<in> S\<close> by (fastforce simp: holomorphic_on_subset subset_ball intro!: pole_theorem_open)
   1.482 +  then show "\<exists>e>0. ?F holomorphic_on ball x e"
   1.483 +    using \<open>0 < d\<close> \<open>0 < e\<close> not_le by fastforce
   1.484 +qed
   1.485  
   1.486  lemma pole_theorem_analytic_0:
   1.487 -  assumes g: "g analytic_on s"
   1.488 -      and eq: "\<And>z. z \<in> s \<Longrightarrow> \<exists>d. 0 < d \<and> (\<forall>w \<in> ball z d - {a}. g w = (w - a) * f w)"
   1.489 +  assumes g: "g analytic_on S"
   1.490 +      and eq: "\<And>z. z \<in> S \<Longrightarrow> \<exists>d. 0 < d \<and> (\<forall>w \<in> ball z d - {a}. g w = (w - a) * f w)"
   1.491        and [simp]: "f a = deriv g a" "g a = 0"
   1.492 -    shows "f analytic_on s"
   1.493 +    shows "f analytic_on S"
   1.494  proof -
   1.495    have [simp]: "(\<lambda>z. if z = a then deriv g a else f z - g a / (z - a)) = f"
   1.496      by auto
   1.497 @@ -6985,22 +6987,27 @@
   1.498  qed
   1.499  
   1.500  lemma pole_theorem_analytic_open_superset:
   1.501 -  assumes g: "g analytic_on s" and "s \<subseteq> t" "open t"
   1.502 -      and eq: "\<And>z. z \<in> t - {a} \<Longrightarrow> g z = (z - a) * f z"
   1.503 +  assumes g: "g analytic_on S" and "S \<subseteq> T" "open T"
   1.504 +      and eq: "\<And>z. z \<in> T - {a} \<Longrightarrow> g z = (z - a) * f z"
   1.505      shows "(\<lambda>z. if z = a then deriv g a
   1.506 -                 else f z - g a/(z - a)) analytic_on s"
   1.507 -  apply (rule pole_theorem_analytic [OF g])
   1.508 -  apply (rule openE [OF \<open>open t\<close>])
   1.509 -  using assms eq by auto
   1.510 +                 else f z - g a/(z - a)) analytic_on S"
   1.511 +proof (rule pole_theorem_analytic [OF g])
   1.512 +  fix z
   1.513 +  assume "z \<in> S"
   1.514 +  then obtain e where "0 < e" and e: "ball z e \<subseteq> T"
   1.515 +    using assms openE by blast
   1.516 +  then show "\<exists>d>0. \<forall>w\<in>ball z d - {a}. g w = (w - a) * f w"
   1.517 +    using eq by auto
   1.518 +qed
   1.519  
   1.520  lemma pole_theorem_analytic_open_superset_0:
   1.521 -  assumes g: "g analytic_on s" "s \<subseteq> t" "open t" "\<And>z. z \<in> t - {a} \<Longrightarrow> g z = (z - a) * f z"
   1.522 +  assumes g: "g analytic_on S" "S \<subseteq> T" "open T" "\<And>z. z \<in> T - {a} \<Longrightarrow> g z = (z - a) * f z"
   1.523        and [simp]: "f a = deriv g a" "g a = 0"
   1.524 -    shows "f analytic_on s"
   1.525 +    shows "f analytic_on S"
   1.526  proof -
   1.527    have [simp]: "(\<lambda>z. if z = a then deriv g a else f z - g a / (z - a)) = f"
   1.528      by auto
   1.529 -  have "(\<lambda>z. if z = a then deriv g a else f z - g a/(z - a)) analytic_on s"
   1.530 +  have "(\<lambda>z. if z = a then deriv g a else f z - g a/(z - a)) analytic_on S"
   1.531      by (rule pole_theorem_analytic_open_superset [OF g])
   1.532    then show ?thesis by simp
   1.533  qed
   1.534 @@ -7011,24 +7018,25 @@
   1.535  text\<open>Proof is based on Dixon's, as presented in Lang's "Complex Analysis" book (page 147).\<close>
   1.536  
   1.537  lemma contour_integral_continuous_on_linepath_2D:
   1.538 -  assumes "open u" and cont_dw: "\<And>w. w \<in> u \<Longrightarrow> F w contour_integrable_on (linepath a b)"
   1.539 -      and cond_uu: "continuous_on (u \<times> u) (\<lambda>(x,y). F x y)"
   1.540 -      and abu: "closed_segment a b \<subseteq> u"
   1.541 -    shows "continuous_on u (\<lambda>w. contour_integral (linepath a b) (F w))"
   1.542 +  assumes "open U" and cont_dw: "\<And>w. w \<in> U \<Longrightarrow> F w contour_integrable_on (linepath a b)"
   1.543 +      and cond_uu: "continuous_on (U \<times> U) (\<lambda>(x,y). F x y)"
   1.544 +      and abu: "closed_segment a b \<subseteq> U"
   1.545 +    shows "continuous_on U (\<lambda>w. contour_integral (linepath a b) (F w))"
   1.546  proof -
   1.547 -  have *: "\<exists>d>0. \<forall>x'\<in>u. dist x' w < d \<longrightarrow>
   1.548 +  have *: "\<exists>d>0. \<forall>x'\<in>U. dist x' w < d \<longrightarrow>
   1.549                           dist (contour_integral (linepath a b) (F x'))
   1.550                                (contour_integral (linepath a b) (F w)) \<le> \<epsilon>"
   1.551 -          if "w \<in> u" "0 < \<epsilon>" "a \<noteq> b" for w \<epsilon>
   1.552 +          if "w \<in> U" "0 < \<epsilon>" "a \<noteq> b" for w \<epsilon>
   1.553    proof -
   1.554 -    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
   1.555 -    let ?TZ = "{(t,z) |t z. t \<in> cball w \<delta> \<and> z \<in> closed_segment a b}"
   1.556 +    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
   1.557 +    let ?TZ = "cball w \<delta>  \<times> closed_segment a b"
   1.558      have "uniformly_continuous_on ?TZ (\<lambda>(x,y). F x y)"
   1.559 -      apply (rule compact_uniformly_continuous)
   1.560 -      apply (rule continuous_on_subset[OF cond_uu])
   1.561 -      using abu \<delta>
   1.562 -      apply (auto simp: compact_Times simp del: mem_cball)
   1.563 -      done
   1.564 +    proof (rule compact_uniformly_continuous)
   1.565 +      show "continuous_on ?TZ (\<lambda>(x,y). F x y)"
   1.566 +        by (rule continuous_on_subset[OF cond_uu]) (use SigmaE \<delta> abu in blast)
   1.567 +      show "compact ?TZ"
   1.568 +        by (simp add: compact_Times)
   1.569 +    qed
   1.570      then obtain \<eta> where "\<eta>>0"
   1.571          and \<eta>: "\<And>x x'. \<lbrakk>x\<in>?TZ; x'\<in>?TZ; dist x' x < \<eta>\<rbrakk> \<Longrightarrow>
   1.572                           dist ((\<lambda>(x,y). F x y) x') ((\<lambda>(x,y). F x y) x) < \<epsilon>/norm(b - a)"
   1.573 @@ -7040,13 +7048,13 @@
   1.574               for x1 x2 x1' x2'
   1.575        using \<eta> [of "(x1,x2)" "(x1',x2')"] by (force simp: dist_norm)
   1.576      have le_ee: "cmod (contour_integral (linepath a b) (\<lambda>x. F x' x - F w x)) \<le> \<epsilon>"
   1.577 -                if "x' \<in> u" "cmod (x' - w) < \<delta>" "cmod (x' - w) < \<eta>"  for x'
   1.578 +                if "x' \<in> U" "cmod (x' - w) < \<delta>" "cmod (x' - w) < \<eta>"  for x'
   1.579      proof -
   1.580 -      have "cmod (contour_integral (linepath a b) (\<lambda>x. F x' x - F w x)) \<le> \<epsilon>/norm(b - a) * norm(b - a)"
   1.581 +      have "(\<lambda>x. F x' x - F w x) contour_integrable_on linepath a b"
   1.582 +        by (simp add: \<open>w \<in> U\<close> cont_dw contour_integrable_diff that)
   1.583 +      then have "cmod (contour_integral (linepath a b) (\<lambda>x. F x' x - F w x)) \<le> \<epsilon>/norm(b - a) * norm(b - a)"
   1.584          apply (rule has_contour_integral_bound_linepath [OF has_contour_integral_integral _ \<eta>])
   1.585 -        apply (rule contour_integrable_diff [OF cont_dw cont_dw])
   1.586 -        using \<open>0 < \<epsilon>\<close> \<open>a \<noteq> b\<close> \<open>0 < \<delta>\<close> \<open>w \<in> u\<close> that
   1.587 -        apply (auto simp: norm_minus_commute)
   1.588 +        using \<open>0 < \<epsilon>\<close> \<open>0 < \<delta>\<close> that apply (auto simp: norm_minus_commute)
   1.589          done
   1.590        also have "\<dots> = \<epsilon>" using \<open>a \<noteq> b\<close> by simp
   1.591        finally show ?thesis .
   1.592 @@ -7054,22 +7062,26 @@
   1.593      show ?thesis
   1.594        apply (rule_tac x="min \<delta> \<eta>" in exI)
   1.595        using \<open>0 < \<delta>\<close> \<open>0 < \<eta>\<close>
   1.596 -      apply (auto simp: dist_norm contour_integral_diff [OF cont_dw cont_dw, symmetric] \<open>w \<in> u\<close> intro: le_ee)
   1.597 +      apply (auto simp: dist_norm contour_integral_diff [OF cont_dw cont_dw, symmetric] \<open>w \<in> U\<close> intro: le_ee)
   1.598        done
   1.599    qed
   1.600    show ?thesis
   1.601 -    apply (rule continuous_onI)
   1.602 -    apply (cases "a=b")
   1.603 -    apply (auto intro: *)
   1.604 -    done
   1.605 +  proof (cases "a=b")
   1.606 +    case True
   1.607 +    then show ?thesis by simp
   1.608 +  next
   1.609 +    case False
   1.610 +    show ?thesis
   1.611 +      by (rule continuous_onI) (use False in \<open>auto intro: *\<close>)
   1.612 +  qed
   1.613  qed
   1.614  
   1.615  text\<open>This version has @{term"polynomial_function \<gamma>"} as an additional assumption.\<close>
   1.616  lemma Cauchy_integral_formula_global_weak:
   1.617 -    assumes u: "open u" and holf: "f holomorphic_on u"
   1.618 -        and z: "z \<in> u" and \<gamma>: "polynomial_function \<gamma>"
   1.619 -        and pasz: "path_image \<gamma> \<subseteq> u - {z}" and loop: "pathfinish \<gamma> = pathstart \<gamma>"
   1.620 -        and zero: "\<And>w. w \<notin> u \<Longrightarrow> winding_number \<gamma> w = 0"
   1.621 +  assumes "open U" and holf: "f holomorphic_on U"
   1.622 +        and z: "z \<in> U" and \<gamma>: "polynomial_function \<gamma>"
   1.623 +        and pasz: "path_image \<gamma> \<subseteq> U - {z}" and loop: "pathfinish \<gamma> = pathstart \<gamma>"
   1.624 +        and zero: "\<And>w. w \<notin> U \<Longrightarrow> winding_number \<gamma> w = 0"
   1.625        shows "((\<lambda>w. f w / (w - z)) has_contour_integral (2*pi * \<i> * winding_number \<gamma> z * f z)) \<gamma>"
   1.626  proof -
   1.627    obtain \<gamma>' where pf\<gamma>': "polynomial_function \<gamma>'" and \<gamma>': "\<And>x. (\<gamma> has_vector_derivative (\<gamma>' x)) (at x)"
   1.628 @@ -7084,46 +7096,50 @@
   1.629      by (auto simp: path_polynomial_function valid_path_polynomial_function)
   1.630    then have ov: "open v"
   1.631      by (simp add: v_def open_winding_number_levelsets loop)
   1.632 -  have uv_Un: "u \<union> v = UNIV"
   1.633 +  have uv_Un: "U \<union> v = UNIV"
   1.634      using pasz zero by (auto simp: v_def)
   1.635 -  have conf: "continuous_on u f"
   1.636 +  have conf: "continuous_on U f"
   1.637      by (metis holf holomorphic_on_imp_continuous_on)
   1.638 -  have hol_d: "(d y) holomorphic_on u" if "y \<in> u" for y
   1.639 +  have hol_d: "(d y) holomorphic_on U" if "y \<in> U" for y
   1.640    proof -
   1.641 -    have *: "(\<lambda>c. if c = y then deriv f y else (f c - f y) / (c - y)) holomorphic_on u"
   1.642 -      by (simp add: holf pole_lemma_open u)
   1.643 +    have *: "(\<lambda>c. if c = y then deriv f y else (f c - f y) / (c - y)) holomorphic_on U"
   1.644 +      by (simp add: holf pole_lemma_open \<open>open U\<close>)
   1.645      then have "isCont (\<lambda>x. if x = y then deriv f y else (f x - f y) / (x - y)) y"
   1.646 -      using at_within_open field_differentiable_imp_continuous_at holomorphic_on_def that u by fastforce
   1.647 -    then have "continuous_on u (d y)"
   1.648 -      apply (simp add: d_def continuous_on_eq_continuous_at u, clarify)
   1.649 +      using at_within_open field_differentiable_imp_continuous_at holomorphic_on_def that \<open>open U\<close> by fastforce
   1.650 +    then have "continuous_on U (d y)"
   1.651 +      apply (simp add: d_def continuous_on_eq_continuous_at \<open>open U\<close>, clarify)
   1.652        using * holomorphic_on_def
   1.653 -      by (meson field_differentiable_within_open field_differentiable_imp_continuous_at u)
   1.654 -    moreover have "d y holomorphic_on u - {y}"
   1.655 -      apply (simp add: d_def holomorphic_on_open u open_delete field_differentiable_def [symmetric])
   1.656 -      apply (intro ballI)
   1.657 -      apply (rename_tac w)
   1.658 -      apply (rule_tac d="dist w y" and f = "\<lambda>w. (f w - f y)/(w - y)" in field_differentiable_transform_within)
   1.659 -      apply (auto simp: dist_pos_lt dist_commute intro!: derivative_intros)
   1.660 -      using analytic_on_imp_differentiable_at analytic_on_open holf u apply blast
   1.661 -      done
   1.662 +      by (meson field_differentiable_within_open field_differentiable_imp_continuous_at \<open>open U\<close>)
   1.663 +    moreover have "d y holomorphic_on U - {y}"
   1.664 +    proof -
   1.665 +      have "\<And>w. w \<in> U - {y} \<Longrightarrow>
   1.666 +                 (\<lambda>w. if w = y then deriv f y else (f w - f y) / (w - y)) field_differentiable at w"
   1.667 +        apply (rule_tac d="dist w y" and f = "\<lambda>w. (f w - f y)/(w - y)" in field_differentiable_transform_within)
   1.668 +           apply (auto simp: dist_pos_lt dist_commute intro!: derivative_intros)
   1.669 +        using \<open>open U\<close> holf holomorphic_on_imp_differentiable_at by blast
   1.670 +      then show ?thesis
   1.671 +        unfolding field_differentiable_def by (simp add: d_def holomorphic_on_open \<open>open U\<close> open_delete)
   1.672 +    qed
   1.673      ultimately show ?thesis
   1.674 -      by (rule no_isolated_singularity) (auto simp: u)
   1.675 +      by (rule no_isolated_singularity) (auto simp: \<open>open U\<close>)
   1.676    qed
   1.677    have cint_fxy: "(\<lambda>x. (f x - f y) / (x - y)) contour_integrable_on \<gamma>" if "y \<notin> path_image \<gamma>" for y
   1.678 -    apply (rule contour_integrable_holomorphic_simple [where S = "u-{y}"])
   1.679 -    using \<open>valid_path \<gamma>\<close> pasz
   1.680 -    apply (auto simp: u open_delete)
   1.681 -    apply (rule continuous_intros holomorphic_intros continuous_on_subset [OF conf] holomorphic_on_subset [OF holf] |
   1.682 -                force simp: that)+
   1.683 -    done
   1.684 +  proof (rule contour_integrable_holomorphic_simple [where S = "U-{y}"])
   1.685 +    show "(\<lambda>x. (f x - f y) / (x - y)) holomorphic_on U - {y}"
   1.686 +      by (force intro: holomorphic_intros holomorphic_on_subset [OF holf])
   1.687 +    show "path_image \<gamma> \<subseteq> U - {y}"
   1.688 +      using pasz that by blast
   1.689 +  qed (auto simp: \<open>open U\<close> open_delete \<open>valid_path \<gamma>\<close>)
   1.690    define h where
   1.691 -    "h z = (if z \<in> u then contour_integral \<gamma> (d z) else contour_integral \<gamma> (\<lambda>w. f w/(w - z)))" for z
   1.692 -  have U: "\<And>z. z \<in> u \<Longrightarrow> ((d z) has_contour_integral h z) \<gamma>"
   1.693 +    "h z = (if z \<in> U then contour_integral \<gamma> (d z) else contour_integral \<gamma> (\<lambda>w. f w/(w - z)))" for z
   1.694 +  have U: "((d z) has_contour_integral h z) \<gamma>" if "z \<in> U" for z
   1.695 +  proof -
   1.696 +    have "d z holomorphic_on U"
   1.697 +      by (simp add: hol_d that)
   1.698 +    with that show ?thesis
   1.699      apply (simp add: h_def)
   1.700 -    apply (rule has_contour_integral_integral [OF contour_integrable_holomorphic_simple [where S=u]])
   1.701 -    using u pasz \<open>valid_path \<gamma>\<close>
   1.702 -    apply (auto intro: holomorphic_on_imp_continuous_on hol_d)
   1.703 -    done
   1.704 +      by (meson Diff_subset \<open>open U\<close> \<open>valid_path \<gamma>\<close> contour_integrable_holomorphic_simple has_contour_integral_integral pasz subset_trans)
   1.705 +  qed
   1.706    have V: "((\<lambda>w. f w / (w - z)) has_contour_integral h z) \<gamma>" if z: "z \<in> v" for z
   1.707    proof -
   1.708      have 0: "0 = (f z) * 2 * of_real (2 * pi) * \<i> * winding_number \<gamma> z"
   1.709 @@ -7142,24 +7158,24 @@
   1.710      ultimately have *: "((\<lambda>x. f z / (x - z) + (f x - f z) / (x - z)) has_contour_integral (0 + contour_integral \<gamma> (d z))) \<gamma>"
   1.711        by (rule has_contour_integral_add)
   1.712      have "((\<lambda>w. f w / (w - z)) has_contour_integral contour_integral \<gamma> (d z)) \<gamma>"
   1.713 -            if  "z \<in> u"
   1.714 +            if  "z \<in> U"
   1.715        using * by (auto simp: divide_simps has_contour_integral_eq)
   1.716      moreover have "((\<lambda>w. f w / (w - z)) has_contour_integral contour_integral \<gamma> (\<lambda>w. f w / (w - z))) \<gamma>"
   1.717 -            if "z \<notin> u"
   1.718 -      apply (rule has_contour_integral_integral [OF contour_integrable_holomorphic_simple [where S=u]])
   1.719 -      using u pasz \<open>valid_path \<gamma>\<close> that
   1.720 +            if "z \<notin> U"
   1.721 +      apply (rule has_contour_integral_integral [OF contour_integrable_holomorphic_simple [where S=U]])
   1.722 +      using U pasz \<open>valid_path \<gamma>\<close> that
   1.723        apply (auto intro: holomorphic_on_imp_continuous_on hol_d)
   1.724 -      apply (rule continuous_intros conf holomorphic_intros holf | force)+
   1.725 +       apply (rule continuous_intros conf holomorphic_intros holf assms | force)+
   1.726        done
   1.727      ultimately show ?thesis
   1.728        using z by (simp add: h_def)
   1.729    qed
   1.730    have znot: "z \<notin> path_image \<gamma>"
   1.731      using pasz by blast
   1.732 -  obtain d0 where "d0>0" and d0: "\<And>x y. x \<in> path_image \<gamma> \<Longrightarrow> y \<in> - u \<Longrightarrow> d0 \<le> dist x y"
   1.733 -    using separate_compact_closed [of "path_image \<gamma>" "-u"] pasz u
   1.734 +  obtain d0 where "d0>0" and d0: "\<And>x y. x \<in> path_image \<gamma> \<Longrightarrow> y \<in> - U \<Longrightarrow> d0 \<le> dist x y"
   1.735 +    using separate_compact_closed [of "path_image \<gamma>" "-U"] pasz \<open>open U\<close>
   1.736      by (fastforce simp add: \<open>path \<gamma>\<close> compact_path_image)
   1.737 -  obtain dd where "0 < dd" and dd: "{y + k | y k. y \<in> path_image \<gamma> \<and> k \<in> ball 0 dd} \<subseteq> u"
   1.738 +  obtain dd where "0 < dd" and dd: "{y + k | y k. y \<in> path_image \<gamma> \<and> k \<in> ball 0 dd} \<subseteq> U"
   1.739      apply (rule that [of "d0/2"])
   1.740      using \<open>0 < d0\<close>
   1.741      apply (auto simp: dist_norm dest: d0)
   1.742 @@ -7174,27 +7190,27 @@
   1.743      using \<open>0 < dd\<close>
   1.744      apply (rule_tac x="dd/2" in exI, auto)
   1.745      done
   1.746 -  obtain t where "compact t" and subt: "path_image \<gamma> \<subseteq> interior t" and t: "t \<subseteq> u"
   1.747 +  obtain T where "compact T" and subt: "path_image \<gamma> \<subseteq> interior T" and T: "T \<subseteq> U"
   1.748      apply (rule that [OF _ 1])
   1.749      apply (fastforce simp add: \<open>valid_path \<gamma>\<close> compact_valid_path_image intro!: compact_sums)
   1.750      apply (rule order_trans [OF _ dd])
   1.751      using \<open>0 < dd\<close> by fastforce
   1.752    obtain L where "L>0"
   1.753 -           and L: "\<And>f B. \<lbrakk>f holomorphic_on interior t; \<And>z. z\<in>interior t \<Longrightarrow> cmod (f z) \<le> B\<rbrakk> \<Longrightarrow>
   1.754 +           and L: "\<And>f B. \<lbrakk>f holomorphic_on interior T; \<And>z. z\<in>interior T \<Longrightarrow> cmod (f z) \<le> B\<rbrakk> \<Longrightarrow>
   1.755                           cmod (contour_integral \<gamma> f) \<le> L * B"
   1.756        using contour_integral_bound_exists [OF open_interior \<open>valid_path \<gamma>\<close> subt]
   1.757        by blast
   1.758 -  have "bounded(f ` t)"
   1.759 -    by (meson \<open>compact t\<close> compact_continuous_image compact_imp_bounded conf continuous_on_subset t)
   1.760 -  then obtain D where "D>0" and D: "\<And>x. x \<in> t \<Longrightarrow> norm (f x) \<le> D"
   1.761 +  have "bounded(f ` T)"
   1.762 +    by (meson \<open>compact T\<close> compact_continuous_image compact_imp_bounded conf continuous_on_subset T)
   1.763 +  then obtain D where "D>0" and D: "\<And>x. x \<in> T \<Longrightarrow> norm (f x) \<le> D"
   1.764      by (auto simp: bounded_pos)
   1.765 -  obtain C where "C>0" and C: "\<And>x. x \<in> t \<Longrightarrow> norm x \<le> C"
   1.766 -    using \<open>compact t\<close> bounded_pos compact_imp_bounded by force
   1.767 +  obtain C where "C>0" and C: "\<And>x. x \<in> T \<Longrightarrow> norm x \<le> C"
   1.768 +    using \<open>compact T\<close> bounded_pos compact_imp_bounded by force
   1.769    have "dist (h y) 0 \<le> e" if "0 < e" and le: "D * L / e + C \<le> cmod y" for e y
   1.770    proof -
   1.771      have "D * L / e > 0"  using \<open>D>0\<close> \<open>L>0\<close> \<open>e>0\<close> by simp
   1.772      with le have ybig: "norm y > C" by force
   1.773 -    with C have "y \<notin> t"  by force
   1.774 +    with C have "y \<notin> T"  by force
   1.775      then have ynot: "y \<notin> path_image \<gamma>"
   1.776        using subt interior_subset by blast
   1.777      have [simp]: "winding_number \<gamma> y = 0"
   1.778 @@ -7204,12 +7220,12 @@
   1.779        done
   1.780      have [simp]: "h y = contour_integral \<gamma> (\<lambda>w. f w/(w - y))"
   1.781        by (rule contour_integral_unique [symmetric]) (simp add: v_def ynot V)
   1.782 -    have holint: "(\<lambda>w. f w / (w - y)) holomorphic_on interior t"
   1.783 +    have holint: "(\<lambda>w. f w / (w - y)) holomorphic_on interior T"
   1.784        apply (rule holomorphic_on_divide)
   1.785 -      using holf holomorphic_on_subset interior_subset t apply blast
   1.786 +      using holf holomorphic_on_subset interior_subset T apply blast
   1.787        apply (rule holomorphic_intros)+
   1.788 -      using \<open>y \<notin> t\<close> interior_subset by auto
   1.789 -    have leD: "cmod (f z / (z - y)) \<le> D * (e / L / D)" if z: "z \<in> interior t" for z
   1.790 +      using \<open>y \<notin> T\<close> interior_subset by auto
   1.791 +    have leD: "cmod (f z / (z - y)) \<le> D * (e / L / D)" if z: "z \<in> interior T" for z
   1.792      proof -
   1.793        have "D * L / e + cmod z \<le> cmod y"
   1.794          using le C [of z] z using interior_subset by force
   1.795 @@ -7238,32 +7254,33 @@
   1.796    moreover have "h holomorphic_on UNIV"
   1.797    proof -
   1.798      have con_ff: "continuous (at (x,z)) (\<lambda>(x,y). (f y - f x) / (y - x))"
   1.799 -                 if "x \<in> u" "z \<in> u" "x \<noteq> z" for x z
   1.800 +                 if "x \<in> U" "z \<in> U" "x \<noteq> z" for x z
   1.801        using that conf
   1.802 -      apply (simp add: split_def continuous_on_eq_continuous_at u)
   1.803 +      apply (simp add: split_def continuous_on_eq_continuous_at \<open>open U\<close>)
   1.804        apply (simp | rule continuous_intros continuous_within_compose2 [where g=f])+
   1.805        done
   1.806      have con_fstsnd: "continuous_on UNIV (\<lambda>x. (fst x - snd x) ::complex)"
   1.807        by (rule continuous_intros)+
   1.808 -    have open_uu_Id: "open (u \<times> u - Id)"
   1.809 +    have open_uu_Id: "open (U \<times> U - Id)"
   1.810        apply (rule open_Diff)
   1.811 -      apply (simp add: open_Times u)
   1.812 +      apply (simp add: open_Times \<open>open U\<close>)
   1.813        using continuous_closed_preimage_constant [OF con_fstsnd closed_UNIV, of 0]
   1.814        apply (auto simp: Id_fstsnd_eq algebra_simps)
   1.815        done
   1.816 -    have con_derf: "continuous (at z) (deriv f)" if "z \<in> u" for z
   1.817 -      apply (rule continuous_on_interior [of u])
   1.818 -      apply (simp add: holf holomorphic_deriv holomorphic_on_imp_continuous_on u)
   1.819 -      by (simp add: interior_open that u)
   1.820 +    have con_derf: "continuous (at z) (deriv f)" if "z \<in> U" for z
   1.821 +      apply (rule continuous_on_interior [of U])
   1.822 +      apply (simp add: holf holomorphic_deriv holomorphic_on_imp_continuous_on \<open>open U\<close>)
   1.823 +      by (simp add: interior_open that \<open>open U\<close>)
   1.824      have tendsto_f': "((\<lambda>(x,y). if y = x then deriv f (x)
   1.825                                  else (f (y) - f (x)) / (y - x)) \<longlongrightarrow> deriv f x)
   1.826 -                      (at (x, x) within u \<times> u)" if "x \<in> u" for x
   1.827 +                      (at (x, x) within U \<times> U)" if "x \<in> U" for x
   1.828      proof (rule Lim_withinI)
   1.829        fix e::real assume "0 < e"
   1.830        obtain k1 where "k1>0" and k1: "\<And>x'. norm (x' - x) \<le> k1 \<Longrightarrow> norm (deriv f x' - deriv f x) < e"
   1.831 -        using \<open>0 < e\<close> continuous_within_E [OF con_derf [OF \<open>x \<in> u\<close>]]
   1.832 +        using \<open>0 < e\<close> continuous_within_E [OF con_derf [OF \<open>x \<in> U\<close>]]
   1.833          by (metis UNIV_I dist_norm)
   1.834 -      obtain k2 where "k2>0" and k2: "ball x k2 \<subseteq> u" by (blast intro: openE [OF u] \<open>x \<in> u\<close>)
   1.835 +      obtain k2 where "k2>0" and k2: "ball x k2 \<subseteq> U" 
   1.836 +        by (blast intro: openE [OF \<open>open U\<close>] \<open>x \<in> U\<close>)
   1.837        have neq: "norm ((f z' - f x') / (z' - x') - deriv f x) \<le> e"
   1.838                      if "z' \<noteq> x'" and less_k1: "norm (x'-x, z'-x) < k1" and less_k2: "norm (x'-x, z'-x) < k2"
   1.839                   for x' z'
   1.840 @@ -7273,9 +7290,9 @@
   1.841            by (metis (no_types) dist_commute dist_norm norm_fst_le norm_snd_le order_trans)
   1.842          have derf_le: "w \<in> closed_segment x' z' \<Longrightarrow> z' \<noteq> x' \<Longrightarrow> cmod (deriv f w - deriv f x) \<le> e" for w
   1.843            by (blast intro: cs_less less_k1 k1 [unfolded divide_const_simps dist_norm] less_imp_le le_less_trans)
   1.844 -        have f_has_der: "\<And>x. x \<in> u \<Longrightarrow> (f has_field_derivative deriv f x) (at x within u)"
   1.845 -          by (metis DERIV_deriv_iff_field_differentiable at_within_open holf holomorphic_on_def u)
   1.846 -        have "closed_segment x' z' \<subseteq> u"
   1.847 +        have f_has_der: "\<And>x. x \<in> U \<Longrightarrow> (f has_field_derivative deriv f x) (at x within U)"
   1.848 +          by (metis DERIV_deriv_iff_field_differentiable at_within_open holf holomorphic_on_def \<open>open U\<close>)
   1.849 +        have "closed_segment x' z' \<subseteq> U"
   1.850            by (rule order_trans [OF _ k2]) (simp add: cs_less  le_less_trans [OF _ less_k2] dist_complex_def norm_minus_commute subset_iff)
   1.851          then have cint_derf: "(deriv f has_contour_integral f z' - f x') (linepath x' z')"
   1.852            using contour_integral_primitive [OF f_has_der valid_path_linepath] pasz  by simp
   1.853 @@ -7290,7 +7307,7 @@
   1.854          also have "\<dots> \<le> e" using \<open>0 < e\<close> by simp
   1.855          finally show ?thesis .
   1.856        qed
   1.857 -      show "\<exists>d>0. \<forall>xa\<in>u \<times> u.
   1.858 +      show "\<exists>d>0. \<forall>xa\<in>U \<times> U.
   1.859                    0 < dist xa (x, x) \<and> dist xa (x, x) < d \<longrightarrow>
   1.860                    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"
   1.861          apply (rule_tac x="min k1 k2" in exI)
   1.862 @@ -7299,49 +7316,51 @@
   1.863          done
   1.864      qed
   1.865      have con_pa_f: "continuous_on (path_image \<gamma>) f"
   1.866 -      by (meson holf holomorphic_on_imp_continuous_on holomorphic_on_subset interior_subset subt t)
   1.867 -    have le_B: "\<And>t. t \<in> {0..1} \<Longrightarrow> cmod (vector_derivative \<gamma> (at t)) \<le> B"
   1.868 +      by (meson holf holomorphic_on_imp_continuous_on holomorphic_on_subset interior_subset subt T)
   1.869 +    have le_B: "\<And>T. T \<in> {0..1} \<Longrightarrow> cmod (vector_derivative \<gamma> (at T)) \<le> B"
   1.870        apply (rule B)
   1.871        using \<gamma>' using path_image_def vector_derivative_at by fastforce
   1.872      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>"
   1.873        by (simp add: V)
   1.874 -    have cond_uu: "continuous_on (u \<times> u) (\<lambda>(x,y). d x y)"
   1.875 +    have cond_uu: "continuous_on (U \<times> U) (\<lambda>(x,y). d x y)"
   1.876        apply (simp add: continuous_on_eq_continuous_within d_def continuous_within tendsto_f')
   1.877 -      apply (simp add: tendsto_within_open_NO_MATCH open_Times u, clarify)
   1.878 +      apply (simp add: tendsto_within_open_NO_MATCH open_Times \<open>open U\<close>, clarify)
   1.879        apply (rule Lim_transform_within_open [OF _ open_uu_Id, where f = "(\<lambda>(x,y). (f y - f x) / (y - x))"])
   1.880        using con_ff
   1.881        apply (auto simp: continuous_within)
   1.882        done
   1.883 -    have hol_dw: "(\<lambda>z. d z w) holomorphic_on u" if "w \<in> u" for w
   1.884 +    have hol_dw: "(\<lambda>z. d z w) holomorphic_on U" if "w \<in> U" for w
   1.885      proof -
   1.886 -      have "continuous_on u ((\<lambda>(x,y). d x y) \<circ> (\<lambda>z. (w,z)))"
   1.887 +      have "continuous_on U ((\<lambda>(x,y). d x y) \<circ> (\<lambda>z. (w,z)))"
   1.888          by (rule continuous_on_compose continuous_intros continuous_on_subset [OF cond_uu] | force intro: that)+
   1.889 -      then have *: "continuous_on u (\<lambda>z. if w = z then deriv f z else (f w - f z) / (w - z))"
   1.890 +      then have *: "continuous_on U (\<lambda>z. if w = z then deriv f z else (f w - f z) / (w - z))"
   1.891          by (rule rev_iffD1 [OF _ continuous_on_cong [OF refl]]) (simp add: d_def field_simps)
   1.892 -      have **: "\<And>x. \<lbrakk>x \<in> u; x \<noteq> w\<rbrakk> \<Longrightarrow> (\<lambda>z. if w = z then deriv f z else (f w - f z) / (w - z)) field_differentiable at x"
   1.893 +      have **: "\<And>x. \<lbrakk>x \<in> U; x \<noteq> w\<rbrakk> \<Longrightarrow> (\<lambda>z. if w = z then deriv f z else (f w - f z) / (w - z)) field_differentiable at x"
   1.894          apply (rule_tac f = "\<lambda>x. (f w - f x)/(w - x)" and d = "dist x w" in field_differentiable_transform_within)
   1.895 -        apply (rule u derivative_intros holomorphic_on_imp_differentiable_at [OF holf] | force simp: dist_commute)+
   1.896 +        apply (rule \<open>open U\<close> derivative_intros holomorphic_on_imp_differentiable_at [OF holf] | force simp: dist_commute)+
   1.897          done
   1.898        show ?thesis
   1.899          unfolding d_def
   1.900 -        apply (rule no_isolated_singularity [OF * _ u, where K = "{w}"])
   1.901 -        apply (auto simp: field_differentiable_def [symmetric] holomorphic_on_open open_Diff u **)
   1.902 +        apply (rule no_isolated_singularity [OF * _ \<open>open U\<close>, where K = "{w}"])
   1.903 +        apply (auto simp: field_differentiable_def [symmetric] holomorphic_on_open open_Diff \<open>open U\<close> **)
   1.904          done
   1.905      qed
   1.906      { fix a b
   1.907 -      assume abu: "closed_segment a b \<subseteq> u"
   1.908 -      then have "\<And>w. w \<in> u \<Longrightarrow> (\<lambda>z. d z w) contour_integrable_on (linepath a b)"
   1.909 +      assume abu: "closed_segment a b \<subseteq> U"
   1.910 +      then have "\<And>w. w \<in> U \<Longrightarrow> (\<lambda>z. d z w) contour_integrable_on (linepath a b)"
   1.911          by (metis hol_dw continuous_on_subset contour_integrable_continuous_linepath holomorphic_on_imp_continuous_on)
   1.912 -      then have cont_cint_d: "continuous_on u (\<lambda>w. contour_integral (linepath a b) (\<lambda>z. d z w))"
   1.913 -        apply (rule contour_integral_continuous_on_linepath_2D [OF \<open>open u\<close> _ _ abu])
   1.914 +      then have cont_cint_d: "continuous_on U (\<lambda>w. contour_integral (linepath a b) (\<lambda>z. d z w))"
   1.915 +        apply (rule contour_integral_continuous_on_linepath_2D [OF \<open>open U\<close> _ _ abu])
   1.916          apply (auto intro: continuous_on_swap_args cond_uu)
   1.917          done
   1.918        have cont_cint_d\<gamma>: "continuous_on {0..1} ((\<lambda>w. contour_integral (linepath a b) (\<lambda>z. d z w)) \<circ> \<gamma>)"
   1.919 -        apply (rule continuous_on_compose)
   1.920 -        using \<open>path \<gamma>\<close> path_def pasz
   1.921 -        apply (auto intro!: continuous_on_subset [OF cont_cint_d])
   1.922 -        apply (force simp: path_image_def)
   1.923 -        done
   1.924 +      proof (rule continuous_on_compose)
   1.925 +        show "continuous_on {0..1} \<gamma>"
   1.926 +          using \<open>path \<gamma>\<close> path_def by blast
   1.927 +        show "continuous_on (\<gamma> ` {0..1}) (\<lambda>w. contour_integral (linepath a b) (\<lambda>z. d z w))"
   1.928 +          using pasz unfolding path_image_def
   1.929 +          by (auto intro!: continuous_on_subset [OF cont_cint_d])
   1.930 +      qed
   1.931        have cint_cint: "(\<lambda>w. contour_integral (linepath a b) (\<lambda>z. d z w)) contour_integrable_on \<gamma>"
   1.932          apply (simp add: contour_integrable_on)
   1.933          apply (rule integrable_continuous_real)
   1.934 @@ -7361,13 +7380,13 @@
   1.935                      contour_integral \<gamma> (\<lambda>w. contour_integral (linepath a b) (\<lambda>z. d z w))" .
   1.936        note cint_cint cint_h_eq
   1.937      } note cint_h = this
   1.938 -    have conthu: "continuous_on u h"
   1.939 +    have conthu: "continuous_on U h"
   1.940      proof (simp add: continuous_on_sequentially, clarify)
   1.941        fix a x
   1.942 -      assume x: "x \<in> u" and au: "\<forall>n. a n \<in> u" and ax: "a \<longlonglongrightarrow> x"
   1.943 +      assume x: "x \<in> U" and au: "\<forall>n. a n \<in> U" and ax: "a \<longlonglongrightarrow> x"
   1.944        then have A1: "\<forall>\<^sub>F n in sequentially. d (a n) contour_integrable_on \<gamma>"
   1.945          by (meson U contour_integrable_on_def eventuallyI)
   1.946 -      obtain dd where "dd>0" and dd: "cball x dd \<subseteq> u" using open_contains_cball u x by force
   1.947 +      obtain dd where "dd>0" and dd: "cball x dd \<subseteq> U" using open_contains_cball \<open>open U\<close> x by force
   1.948        have A2: "uniform_limit (path_image \<gamma>) (\<lambda>n. d (a n)) (d x) sequentially"
   1.949          unfolding uniform_limit_iff dist_norm
   1.950        proof clarify
   1.951 @@ -7382,10 +7401,9 @@
   1.952               apply (auto simp: compact_Times compact_valid_path_image simp del: mem_cball)
   1.953              done
   1.954            then obtain kk where "kk>0"
   1.955 -            and kk: "\<And>x x'. \<lbrakk>x\<in>?ddpa; x'\<in>?ddpa; dist x' x < kk\<rbrakk> \<Longrightarrow>
   1.956 +            and kk: "\<And>x x'. \<lbrakk>x \<in> ?ddpa; x' \<in> ?ddpa; dist x' x < kk\<rbrakk> \<Longrightarrow>
   1.957                               dist ((\<lambda>(x,y). d x y) x') ((\<lambda>(x,y). d x y) x) < ee"
   1.958 -            apply (rule uniformly_continuous_onE [where e = ee])
   1.959 -            using \<open>0 < ee\<close> by auto
   1.960 +            by (rule uniformly_continuous_onE [where e = ee]) (use \<open>0 < ee\<close> in auto)
   1.961            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"
   1.962              for  w z
   1.963              using \<open>dd>0\<close> kk [of "(x,z)" "(w,z)"] by (force simp: norm_minus_commute dist_norm)
   1.964 @@ -7397,35 +7415,34 @@
   1.965              done
   1.966          qed
   1.967        qed
   1.968 -      have tendsto_hx: "(\<lambda>n. contour_integral \<gamma> (d (a n))) \<longlonglongrightarrow> h x"
   1.969 -        apply (simp add: contour_integral_unique [OF U, symmetric] x)
   1.970 -        apply (rule contour_integral_uniform_limit [OF A1 A2 le_B])
   1.971 -        apply (auto simp: \<open>valid_path \<gamma>\<close>)
   1.972 -        done
   1.973 +      have "(\<lambda>n. contour_integral \<gamma> (d (a n))) \<longlonglongrightarrow> contour_integral \<gamma> (d x)"
   1.974 +        by (rule contour_integral_uniform_limit [OF A1 A2 le_B]) (auto simp: \<open>valid_path \<gamma>\<close>)
   1.975 +      then have tendsto_hx: "(\<lambda>n. contour_integral \<gamma> (d (a n))) \<longlonglongrightarrow> h x"
   1.976 +        by (simp add: h_def x)
   1.977        then show "(h \<circ> a) \<longlonglongrightarrow> h x"
   1.978          by (simp add: h_def x au o_def)
   1.979      qed
   1.980      show ?thesis
   1.981      proof (simp add: holomorphic_on_open field_differentiable_def [symmetric], clarify)
   1.982        fix z0
   1.983 -      consider "z0 \<in> v" | "z0 \<in> u" using uv_Un by blast
   1.984 +      consider "z0 \<in> v" | "z0 \<in> U" using uv_Un by blast
   1.985        then show "h field_differentiable at z0"
   1.986        proof cases
   1.987          assume "z0 \<in> v" then show ?thesis
   1.988            using Cauchy_next_derivative [OF con_pa_f le_B f_has_cint _ ov] V f_has_cint \<open>valid_path \<gamma>\<close>
   1.989            by (auto simp: field_differentiable_def v_def)
   1.990        next
   1.991 -        assume "z0 \<in> u" then
   1.992 -        obtain e where "e>0" and e: "ball z0 e \<subseteq> u" by (blast intro: openE [OF u])
   1.993 +        assume "z0 \<in> U" then
   1.994 +        obtain e where "e>0" and e: "ball z0 e \<subseteq> U" by (blast intro: openE [OF \<open>open U\<close>])
   1.995          have *: "contour_integral (linepath a b) h + contour_integral (linepath b c) h + contour_integral (linepath c a) h = 0"
   1.996                  if abc_subset: "convex hull {a, b, c} \<subseteq> ball z0 e"  for a b c
   1.997          proof -
   1.998 -          have *: "\<And>x1 x2 z. z \<in> u \<Longrightarrow> closed_segment x1 x2 \<subseteq> u \<Longrightarrow> (\<lambda>w. d w z) contour_integrable_on linepath x1 x2"
   1.999 -            using  hol_dw holomorphic_on_imp_continuous_on u
  1.1000 +          have *: "\<And>x1 x2 z. z \<in> U \<Longrightarrow> closed_segment x1 x2 \<subseteq> U \<Longrightarrow> (\<lambda>w. d w z) contour_integrable_on linepath x1 x2"
  1.1001 +            using  hol_dw holomorphic_on_imp_continuous_on \<open>open U\<close>
  1.1002              by (auto intro!: contour_integrable_holomorphic_simple)
  1.1003 -          have abc: "closed_segment a b \<subseteq> u"  "closed_segment b c \<subseteq> u"  "closed_segment c a \<subseteq> u"
  1.1004 +          have abc: "closed_segment a b \<subseteq> U"  "closed_segment b c \<subseteq> U"  "closed_segment c a \<subseteq> U"
  1.1005              using that e segments_subset_convex_hull by fastforce+
  1.1006 -          have eq0: "\<And>w. w \<in> u \<Longrightarrow> contour_integral (linepath a b +++ linepath b c +++ linepath c a) (\<lambda>z. d z w) = 0"
  1.1007 +          have eq0: "\<And>w. w \<in> U \<Longrightarrow> contour_integral (linepath a b +++ linepath b c +++ linepath c a) (\<lambda>z. d z w) = 0"
  1.1008              apply (rule contour_integral_unique [OF Cauchy_theorem_triangle])
  1.1009              apply (rule holomorphic_on_subset [OF hol_dw])
  1.1010              using e abc_subset by auto
  1.1011 @@ -7434,7 +7451,7 @@
  1.1012                          (contour_integral (linepath b c) (\<lambda>z. d z x) +
  1.1013                           contour_integral (linepath c a) (\<lambda>z. d z x)))  =  0"
  1.1014              apply (rule contour_integral_eq_0)
  1.1015 -            using abc pasz u
  1.1016 +            using abc pasz U
  1.1017              apply (subst contour_integral_join [symmetric], auto intro: eq0 *)+
  1.1018              done
  1.1019            then show ?thesis
  1.1020 @@ -7540,13 +7557,12 @@
  1.1021             "path_image g \<subseteq> S" "pathfinish g = pathstart g" "z \<notin> S"
  1.1022      shows "winding_number g z = 0"
  1.1023  proof -
  1.1024 -  have "winding_number g z = winding_number(linepath (pathstart g) (pathstart g)) z"
  1.1025 -    apply (rule winding_number_homotopic_paths)
  1.1026 -    apply (rule homotopic_loops_imp_homotopic_paths_null [where a = "pathstart g"])
  1.1027 -    apply (rule homotopic_loops_subset [of S])
  1.1028 -    using assms
  1.1029 -    apply (auto simp: homotopic_paths_imp_homotopic_loops path_defs simply_connected_eq_contractible_path)
  1.1030 -    done
  1.1031 +  have hom: "homotopic_loops S g (linepath (pathstart g) (pathstart g))"
  1.1032 +    by (meson assms homotopic_paths_imp_homotopic_loops pathfinish_linepath simply_connected_eq_contractible_path)
  1.1033 +  then have "homotopic_paths (- {z}) g (linepath (pathstart g) (pathstart g))"
  1.1034 +    by (meson \<open>z \<notin> S\<close> homotopic_loops_imp_homotopic_paths_null homotopic_paths_subset subset_Compl_singleton)
  1.1035 +  then have "winding_number g z = winding_number(linepath (pathstart g) (pathstart g)) z"
  1.1036 +    by (rule winding_number_homotopic_paths)
  1.1037    also have "\<dots> = 0"
  1.1038      using assms by (force intro: winding_number_trivial)
  1.1039    finally show ?thesis .
  1.1040 @@ -7562,7 +7578,7 @@
  1.1041                           homotopic_paths_imp_homotopic_loops)
  1.1042  using valid_path_imp_path by blast
  1.1043  
  1.1044 -lemma holomorphic_logarithm_exists:
  1.1045 +proposition holomorphic_logarithm_exists:
  1.1046    assumes A: "convex A" "open A" 
  1.1047        and f: "f holomorphic_on A" "\<And>x. x \<in> A \<Longrightarrow> f x \<noteq> 0"
  1.1048        and z0: "z0 \<in> A"
  1.1049 @@ -7586,7 +7602,6 @@
  1.1050      from 2 and z0 and f show ?case
  1.1051        by (auto simp: h_def exp_diff field_simps intro!: derivative_eq_intros g f')
  1.1052    qed fact+
  1.1053 -
  1.1054    then obtain c where c: "\<And>x. x \<in> A \<Longrightarrow> f x / exp (h x) - 1 = c"
  1.1055      by blast
  1.1056    from c[OF z0] and z0 and f have "c = 0"