author paulson Sat Jun 02 22:57:18 2018 +0100 (14 months ago) changeset 68359 8cd3d0305269 parent 68341 b58e7131de0d child 68360 0f19c98fa7be
tidied more Cauchy proofs
```     1.1 --- a/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Fri Jun 01 09:57:33 2018 +0100
1.2 +++ b/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Sat Jun 02 22:57:18 2018 +0100
1.3 @@ -3370,7 +3370,7 @@
1.4        fix e::real
1.5        assume e: "e>0"
1.6        obtain p where p: "polynomial_function p \<and>
1.7 -            pathstart p = pathstart \<gamma> \<and> pathfinish p = pathfinish \<gamma> \<and> (\<forall>t\<in>{0..1}. cmod (p t - \<gamma> t) < min e (d / 2))"
1.8 +            pathstart p = pathstart \<gamma> \<and> pathfinish p = pathfinish \<gamma> \<and> (\<forall>t\<in>{0..1}. cmod (p t - \<gamma> t) < min e (d/2))"
1.9          using path_approx_polynomial_function [OF \<open>path \<gamma>\<close>, of "min e (d/2)"] d \<open>0<e\<close> by auto
1.10        have "(\<lambda>w. 1 / (w - z)) holomorphic_on UNIV - {z}"
1.11          by (auto simp: intro!: holomorphic_intros)
1.12 @@ -4650,17 +4650,19 @@
1.13      have lpa: "linked_paths atends g p"
1.14        by (metis (mono_tags, lifting) N01(1) ksf linked_paths_def pathfinish_def pathstart_def psf)
1.15      show ?case
1.16 -      apply (rule_tac x="min d1 d2" in exI)
1.17 -      apply (simp add: \<open>0 < d1\<close> \<open>0 < d2\<close>, clarify)
1.18 -      apply (rule_tac s="contour_integral p f" in trans)
1.19 -      using pk_le N01(1) ksf pathfinish_def pathstart_def
1.20 -      apply (force intro!: vpp d1 simp add: linked_paths_def psf ksf)
1.21 -      using pk_le N01 apply (force intro!: vpp d2 lpa simp add: linked_paths_def psf ksf)
1.22 -      done
1.23 +    proof (intro exI; safe)
1.24 +      fix j
1.25 +      assume "valid_path j" "linked_paths atends g j"
1.26 +        and "\<forall>u\<in>{0..1}. cmod (j u - k (real (Suc n) / real N, u)) < min d1 d2"
1.27 +      then have "contour_integral j f = contour_integral p f"
1.28 +        using pk_le N01(1) ksf by (force intro!: vpp d1 simp add: linked_paths_def psf)
1.29 +      also have "... = contour_integral g f"
1.30 +        using pk_le by (force intro!: vpp d2 lpa)
1.31 +      finally show "contour_integral j f = contour_integral g f" .
1.32 +    qed (simp add: \<open>0 < d1\<close> \<open>0 < d2\<close>)
1.33    qed
1.34    then obtain d where "0 < d"
1.35 -                       "\<And>j. valid_path j \<and> (\<forall>u \<in> {0..1}. norm(j u - k (1,u)) < d) \<and>
1.36 -                            linked_paths atends g j
1.37 +                       "\<And>j. valid_path j \<and> (\<forall>u \<in> {0..1}. norm(j u - k (1,u)) < d) \<and> linked_paths atends g j
1.38                              \<Longrightarrow> contour_integral j f = contour_integral g f"
1.39      using \<open>N>0\<close> by auto
1.40    then have "linked_paths atends g h \<Longrightarrow> contour_integral h f = contour_integral g f"
1.41 @@ -4726,15 +4728,14 @@
1.42         and hq_less: "\<forall>t\<in>{0..1}. cmod (h t - q t) < e"
1.43         and paq:  "contour_integral q (\<lambda>w. 1 / (w - z)) = complex_of_real (2 * pi) * \<i> * winding_number h z"
1.44      using winding_number [OF \<open>path h\<close> pah \<open>0 < e\<close>] unfolding winding_number_prop_def by blast
1.45 -  have gp: "homotopic_paths (- {z}) g p"
1.46 +  have "homotopic_paths (- {z}) g p"
1.47      by (simp add: d p valid_path_imp_path norm_minus_commute gp_less)
1.48 -  have hq: "homotopic_paths (- {z}) h q"
1.49 +  moreover have "homotopic_paths (- {z}) h q"
1.50      by (simp add: e q valid_path_imp_path norm_minus_commute hq_less)
1.51 -  have "contour_integral p (\<lambda>w. 1/(w - z)) = contour_integral q (\<lambda>w. 1/(w - z))"
1.52 -    apply (rule Cauchy_theorem_homotopic_paths [of "-{z}"])
1.53 -    apply (blast intro: homotopic_paths_trans homotopic_paths_sym gp hq assms)
1.54 -    apply (auto intro!: holomorphic_intros simp: p q)
1.55 -    done
1.56 +  ultimately have "homotopic_paths (- {z}) p q"
1.57 +    by (blast intro: homotopic_paths_trans homotopic_paths_sym assms)
1.58 +  then have "contour_integral p (\<lambda>w. 1/(w - z)) = contour_integral q (\<lambda>w. 1/(w - z))"
1.59 +    by (rule Cauchy_theorem_homotopic_paths) (auto intro!: holomorphic_intros simp: p q)
1.60    then show ?thesis
1.61      by (simp add: pap paq)
1.62  qed
1.63 @@ -4792,16 +4793,13 @@
1.64    by (blast intro: sym homotopic_loops_linear winding_number_homotopic_loops)
1.65
1.66  lemma winding_number_nearby_paths_eq:
1.67 -     "\<lbrakk>path g; path h;
1.68 -      pathstart h = pathstart g; pathfinish h = pathfinish g;
1.69 +     "\<lbrakk>path g; path h; pathstart h = pathstart g; pathfinish h = pathfinish g;
1.70        \<And>t. t \<in> {0..1} \<Longrightarrow> norm(h t - g t) < norm(g t - z)\<rbrakk>
1.71        \<Longrightarrow> winding_number h z = winding_number g z"
1.72    by (metis segment_bound(2) norm_minus_commute not_le winding_number_paths_linear_eq)
1.73
1.74  lemma winding_number_nearby_loops_eq:
1.75 -     "\<lbrakk>path g; path h;
1.76 -      pathfinish g = pathstart g;
1.77 -        pathfinish h = pathstart h;
1.78 +     "\<lbrakk>path g; path h; pathfinish g = pathstart g; pathfinish h = pathstart h;
1.79        \<And>t. t \<in> {0..1} \<Longrightarrow> norm(h t - g t) < norm(g t - z)\<rbrakk>
1.80        \<Longrightarrow> winding_number h z = winding_number g z"
1.81    by (metis segment_bound(2) norm_minus_commute not_le winding_number_loops_linear_eq)
1.82 @@ -4968,12 +4966,7 @@
1.83      have **: "((\<lambda>x. if (part_circlepath z r s t x) \<in> k then 0
1.84                      else f(part_circlepath z r s t x) *
1.85                         vector_derivative (part_circlepath z r s t) (at x)) has_integral i)  {0..1}"
1.86 -      apply (rule has_integral_spike
1.87 -              [where f = "\<lambda>x. f(part_circlepath z r s t x) * vector_derivative (part_circlepath z r s t) (at x)"])
1.88 -      apply (rule negligible_finite [OF fin01])
1.89 -      using fi has_contour_integral
1.90 -      apply auto
1.91 -      done
1.92 +      by (rule has_integral_spike [OF negligible_finite [OF fin01]])  (use fi has_contour_integral in auto)
1.93      have *: "\<And>x. \<lbrakk>0 \<le> x; x \<le> 1; part_circlepath z r s t x \<notin> k\<rbrakk> \<Longrightarrow> cmod (f (part_circlepath z r s t x)) \<le> B"
1.94        by (auto intro!: B [unfolded path_image_def image_def, simplified])
1.95      show ?thesis
1.96 @@ -5023,9 +5016,8 @@
1.97  proof (cases "r = 0 \<or> s = t")
1.98    case True
1.99    then show ?thesis
1.100 -    apply (rule disjE)
1.101 -    apply (force simp: part_circlepath_def simple_path_def intro: bexI [where x = "1/4"] bexI [where x = "1/3"])+
1.102 -    done
1.103 +    unfolding part_circlepath_def simple_path_def
1.104 +    by (rule disjE) (force intro: bexI [where x = "1/4"] bexI [where x = "1/3"])+
1.105  next
1.106    case False then have "r \<noteq> 0" "s \<noteq> t" by auto
1.107    have *: "\<And>x y z s t. \<i>*((1 - x) * s + x * t) = \<i>*(((1 - y) * s + y * t)) + z  \<longleftrightarrow> \<i>*(x - y) * (t - s) = z"
1.108 @@ -5033,28 +5025,29 @@
1.109    have abs01: "\<And>x y::real. 0 \<le> x \<and> x \<le> 1 \<and> 0 \<le> y \<and> y \<le> 1
1.110                        \<Longrightarrow> (x = y \<or> x = 0 \<and> y = 1 \<or> x = 1 \<and> y = 0 \<longleftrightarrow> \<bar>x - y\<bar> \<in> {0,1})"
1.111      by auto
1.112 -  have abs_away: "\<And>P. (\<forall>x\<in>{0..1}. \<forall>y\<in>{0..1}. P \<bar>x - y\<bar>) \<longleftrightarrow> (\<forall>x::real. 0 \<le> x \<and> x \<le> 1 \<longrightarrow> P x)"
1.113 -    by force
1.114    have **: "\<And>x y. (\<exists>n. (complex_of_real x - of_real y) * (of_real t - of_real s) = 2 * (of_int n * of_real pi)) \<longleftrightarrow>
1.115                    (\<exists>n. \<bar>x - y\<bar> * (t - s) = 2 * (of_int n * pi))"
1.116      by (force simp: algebra_simps abs_if dest: arg_cong [where f=Re] arg_cong [where f=complex_of_real]
1.117                      intro: exI [where x = "-n" for n])
1.118 -  have 1: "\<forall>x. 0 \<le> x \<and> x \<le> 1 \<longrightarrow> (\<exists>n. x * (t - s) = 2 * (real_of_int n * pi)) \<longrightarrow> x = 0 \<or> x = 1 \<Longrightarrow> \<bar>s - t\<bar> \<le> 2 * pi"
1.119 -    apply (rule ccontr)
1.120 -    apply (drule_tac x="2*pi / \<bar>t - s\<bar>" in spec)
1.121 -    using False
1.122 -    apply (simp add: abs_minus_commute divide_simps)
1.123 -    apply (frule_tac x=1 in spec)
1.124 -    apply (drule_tac x="-1" in spec, simp)
1.125 -    done
1.126 +  have 1: "\<bar>s - t\<bar> \<le> 2 * pi"
1.127 +    if "\<And>x. 0 \<le> x \<and> x \<le> 1 \<Longrightarrow> (\<exists>n. x * (t - s) = 2 * (real_of_int n * pi)) \<longrightarrow> x = 0 \<or> x = 1"
1.128 +  proof (rule ccontr)
1.129 +    assume "\<not> \<bar>s - t\<bar> \<le> 2 * pi"
1.130 +    then have *: "\<And>n. t - s \<noteq> of_int n * \<bar>s - t\<bar>"
1.131 +      using False that [of "2*pi / \<bar>t - s\<bar>"] by (simp add: abs_minus_commute divide_simps)
1.132 +    show False
1.133 +      using * [of 1] * [of "-1"] by auto
1.134 +  qed
1.135    have 2: "\<bar>s - t\<bar> = \<bar>2 * (real_of_int n * pi) / x\<bar>" if "x \<noteq> 0" "x * (t - s) = 2 * (real_of_int n * pi)" for x n
1.136    proof -
1.137      have "t-s = 2 * (real_of_int n * pi)/x"
1.138        using that by (simp add: field_simps)
1.139      then show ?thesis by (metis abs_minus_commute)
1.140    qed
1.141 +  have abs_away: "\<And>P. (\<forall>x\<in>{0..1}. \<forall>y\<in>{0..1}. P \<bar>x - y\<bar>) \<longleftrightarrow> (\<forall>x::real. 0 \<le> x \<and> x \<le> 1 \<longrightarrow> P x)"
1.142 +    by force
1.143    show ?thesis using False
1.144 -    apply (simp add: simple_path_def path_part_circlepath)
1.145 +    apply (simp add: simple_path_def)
1.146      apply (simp add: part_circlepath_def linepath_def exp_eq  * ** abs01  del: Set.insert_iff)
1.147      apply (subst abs_away)
1.148      apply (auto simp: 1)
1.149 @@ -5068,22 +5061,20 @@
1.150      shows "arc (part_circlepath z r s t)"
1.151  proof -
1.152    have *: "x = y" if eq: "\<i> * (linepath s t x) = \<i> * (linepath s t y) + 2 * of_int n * complex_of_real pi * \<i>"
1.153 -                  and x: "x \<in> {0..1}" and y: "y \<in> {0..1}" for x y n
1.154 -    proof -
1.155 -      have "(linepath s t x) = (linepath s t y) + 2 * of_int n * complex_of_real pi"
1.156 -        by (metis add_divide_eq_iff complex_i_not_zero mult.commute nonzero_mult_div_cancel_left eq)
1.157 -      then have "s*y + t*x = s*x + (t*y + of_int n * (pi * 2))"
1.158 -        by (force simp: algebra_simps linepath_def dest: arg_cong [where f=Re])
1.159 -      then have st: "x \<noteq> y \<Longrightarrow> (s-t) = (of_int n * (pi * 2) / (y-x))"
1.160 -        by (force simp: field_simps)
1.161 -      show ?thesis
1.162 -        apply (rule ccontr)
1.163 -        using assms x y
1.164 -        apply (simp add: st abs_mult field_simps)
1.165 -        using st
1.166 -        apply (auto simp: dest: of_int_lessD)
1.167 -        done
1.168 -    qed
1.169 +    and x: "x \<in> {0..1}" and y: "y \<in> {0..1}" for x y n
1.170 +  proof (rule ccontr)
1.171 +    assume "x \<noteq> y"
1.172 +    have "(linepath s t x) = (linepath s t y) + 2 * of_int n * complex_of_real pi"
1.173 +      by (metis add_divide_eq_iff complex_i_not_zero mult.commute nonzero_mult_div_cancel_left eq)
1.174 +    then have "s*y + t*x = s*x + (t*y + of_int n * (pi * 2))"
1.175 +      by (force simp: algebra_simps linepath_def dest: arg_cong [where f=Re])
1.176 +    with \<open>x \<noteq> y\<close> have st: "s-t = (of_int n * (pi * 2) / (y-x))"
1.177 +      by (force simp: field_simps)
1.178 +    have "\<bar>real_of_int n\<bar> < \<bar>y - x\<bar>"
1.179 +      using assms \<open>x \<noteq> y\<close> by (simp add: st abs_mult field_simps)
1.180 +    then show False
1.181 +      using assms x y st by (auto dest: of_int_lessD)
1.182 +  qed
1.183    show ?thesis
1.184      using assms
1.185      apply (simp add: arc_def)
1.186 @@ -5219,14 +5210,16 @@
1.187    by (simp add: sphere_def dist_norm norm_minus_commute)
1.188
1.189  proposition contour_integral_circlepath:
1.190 -     "0 < r \<Longrightarrow> contour_integral (circlepath z r) (\<lambda>w. 1 / (w - z)) = 2 * complex_of_real pi * \<i>"
1.191 -  apply (rule contour_integral_unique)
1.192 -  apply (simp add: has_contour_integral_def)
1.193 -  apply (subst has_integral_cong)
1.194 -  apply (simp add: vector_derivative_circlepath01)
1.195 -  using has_integral_const_real [of _ 0 1]
1.196 -  apply (force simp: circlepath)
1.197 -  done
1.198 +  assumes "r > 0"
1.199 +  shows "contour_integral (circlepath z r) (\<lambda>w. 1 / (w - z)) = 2 * complex_of_real pi * \<i>"
1.200 +proof (rule contour_integral_unique)
1.201 +  show "((\<lambda>w. 1 / (w - z)) has_contour_integral 2 * complex_of_real pi * \<i>) (circlepath z r)"
1.202 +    unfolding has_contour_integral_def using assms
1.203 +    apply (subst has_integral_cong)
1.204 +     apply (simp add: vector_derivative_circlepath01)
1.205 +    using has_integral_const_real [of _ 0 1] apply (force simp: circlepath)
1.206 +    done
1.207 +qed
1.208
1.209  lemma winding_number_circlepath_centre: "0 < r \<Longrightarrow> winding_number (circlepath z r) z = 1"
1.210    apply (rule winding_number_unique_loop)
1.211 @@ -5250,10 +5243,12 @@
1.212    have disjo: "cball z r' \<inter> sphere z r = {}"
1.213      using \<open>r' < r\<close> by (force simp: cball_def sphere_def)
1.214    have "winding_number(circlepath z r) w = winding_number(circlepath z r) z"
1.215 -    apply (rule winding_number_around_inside [where s = "cball z r'"])
1.216 -    apply (simp_all add: disjo order.strict_implies_order winding_number_circlepath_centre)
1.217 -    apply (simp_all add: False r'_def dist_norm norm_minus_commute)
1.218 -    done
1.219 +  proof (rule winding_number_around_inside [where s = "cball z r'"])
1.220 +    show "winding_number (circlepath z r) z \<noteq> 0"
1.221 +      by (simp add: winding_number_circlepath_centre)
1.222 +    show "cball z r' \<inter> path_image (circlepath z r) = {}"
1.223 +      by (simp add: disjo less_eq_real_def)
1.224 +  qed (auto simp: r'_def dist_norm norm_minus_commute)
1.225    also have "\<dots> = 1"
1.226      by (simp add: winding_number_circlepath_centre)
1.227    finally show ?thesis .
1.228 @@ -5263,7 +5258,7 @@
1.229  text\<open> Hence the Cauchy formula for points inside a circle.\<close>
1.230
1.231  theorem Cauchy_integral_circlepath:
1.232 -  assumes "continuous_on (cball z r) f" "f holomorphic_on (ball z r)" "norm(w - z) < r"
1.233 +  assumes contf: "continuous_on (cball z r) f" and holf: "f holomorphic_on (ball z r)" and wz: "norm(w - z) < r"
1.234    shows "((\<lambda>u. f u/(u - w)) has_contour_integral (2 * of_real pi * \<i> * f w))
1.235           (circlepath z r)"
1.236  proof -
1.237 @@ -5271,12 +5266,15 @@
1.238      using assms le_less_trans norm_ge_zero by blast
1.239    have "((\<lambda>u. f u / (u - w)) has_contour_integral (2 * pi) * \<i> * winding_number (circlepath z r) w * f w)
1.240          (circlepath z r)"
1.241 -    apply (rule Cauchy_integral_formula_weak [where s = "cball z r" and k = "{}"])
1.242 -    using assms  \<open>r > 0\<close>
1.243 -    apply (simp_all add: dist_norm norm_minus_commute)
1.244 -    apply (metis at_within_interior dist_norm holomorphic_on_def interior_ball mem_ball norm_minus_commute)
1.245 -    apply (simp add: cball_def sphere_def dist_norm, clarify, simp)
1.246 -    by (metis dist_commute dist_norm less_irrefl)
1.247 +  proof (rule Cauchy_integral_formula_weak [where s = "cball z r" and k = "{}"])
1.248 +    show "\<And>x. x \<in> interior (cball z r) - {} \<Longrightarrow>
1.249 +         f field_differentiable at x"
1.250 +      using holf holomorphic_on_imp_differentiable_at by auto
1.251 +    have "w \<notin> sphere z r"
1.252 +      by simp (metis dist_commute dist_norm not_le order_refl wz)
1.253 +    then show "path_image (circlepath z r) \<subseteq> cball z r - {w}"
1.254 +      using \<open>r > 0\<close> by (auto simp add: cball_def sphere_def)
1.255 +  qed (use wz in \<open>simp_all add: dist_norm norm_minus_commute contf\<close>)
1.256    then show ?thesis
1.257      by (simp add: winding_number_circlepath assms)
1.258  qed
1.259 @@ -5330,20 +5328,18 @@
1.260      have Ble: "B * e / (\<bar>B\<bar> + 1) \<le> e"
1.261        using \<open>0 \<le> B\<close>  \<open>0 < e\<close> by (simp add: divide_simps)
1.262      have "\<exists>h. (\<forall>x\<in>{0..1}. cmod (l (\<gamma> x) * vector_derivative \<gamma> (at x) - h x) \<le> e) \<and> h integrable_on {0..1}"
1.263 -      apply (rule_tac x="\<lambda>x. f (a::'a) (\<gamma> x) * vector_derivative \<gamma> (at x)" in exI)
1.264 -      apply (intro inta conjI ballI)
1.265 -      apply (rule order_trans [OF _ Ble])
1.266 -      apply (frule noleB)
1.267 -      apply (frule fga)
1.268 -      using \<open>0 \<le> B\<close>  \<open>0 < e\<close>
1.269 -      apply (simp add: norm_mult left_diff_distrib [symmetric] norm_minus_commute divide_simps)
1.270 -      apply (drule (1) mult_mono [OF less_imp_le])
1.271 -      apply (simp_all add: mult_ac)
1.272 -      done
1.273 +    proof (intro exI conjI ballI)
1.274 +      show "cmod (l (\<gamma> x) * vector_derivative \<gamma> (at x) - f a (\<gamma> x) * vector_derivative \<gamma> (at x)) \<le> e"
1.275 +        if "x \<in> {0..1}" for x
1.276 +        apply (rule order_trans [OF _ Ble])
1.277 +        using noleB [OF that] fga [OF that] \<open>0 \<le> B\<close> \<open>0 < e\<close>
1.278 +        apply (simp add: norm_mult left_diff_distrib [symmetric] norm_minus_commute divide_simps)
1.279 +        apply (fastforce simp: mult_ac dest: mult_mono [OF less_imp_le])
1.280 +        done
1.281 +    qed (rule inta)
1.282    }
1.283    then show lintg: "l contour_integrable_on \<gamma>"
1.284 -    apply (simp add: contour_integrable_on)
1.285 -    by (metis (mono_tags, lifting)integrable_uniform_limit_real)
1.286 +    unfolding contour_integrable_on by (metis (mono_tags, lifting)integrable_uniform_limit_real)
1.287    { fix e::real
1.288      define B' where "B' = B + 1"
1.289      have B': "B' > 0" "B' > B" using  \<open>0 \<le> B\<close> by (auto simp: B'_def)
1.290 @@ -5363,13 +5359,17 @@
1.291        then show ?thesis
1.292          by (simp add: left_diff_distrib [symmetric] norm_mult)
1.293      qed
1.294 +    have le_e: "\<And>x. \<lbrakk>\<forall>xa\<in>{0..1}. 2 * cmod (f x (\<gamma> xa) - l (\<gamma> xa)) < e / B'; f x contour_integrable_on \<gamma>\<rbrakk>
1.295 +         \<Longrightarrow> cmod (integral {0..1}
1.296 +                    (\<lambda>u. f x (\<gamma> u) * vector_derivative \<gamma> (at u) - l (\<gamma> u) * vector_derivative \<gamma> (at u))) < e"
1.297 +      apply (rule le_less_trans [OF integral_norm_bound_integral ie])
1.298 +        apply (simp add: lintg integrable_diff contour_integrable_on [symmetric])
1.299 +       apply (blast intro: *)+
1.300 +      done
1.301      have "\<forall>\<^sub>F x in F. dist (contour_integral \<gamma> (f x)) (contour_integral \<gamma> l) < e"
1.302        apply (rule eventually_mono [OF eventually_conj [OF ev_no' ev_fint]])
1.303        apply (simp add: dist_norm contour_integrable_on path_image_def contour_integral_integral)
1.304 -      apply (simp add: lintg integral_diff [symmetric] contour_integrable_on [symmetric], clarify)
1.305 -      apply (rule le_less_trans [OF integral_norm_bound_integral ie])
1.306 -      apply (simp add: lintg integrable_diff contour_integrable_on [symmetric])
1.307 -      apply (blast intro: *)+
1.308 +      apply (simp add: lintg integral_diff [symmetric] contour_integrable_on [symmetric] le_e)
1.309        done
1.310    }
1.311    then show "((\<lambda>n. contour_integral \<gamma> (f n)) \<longlongrightarrow> contour_integral \<gamma> l) F"
1.312 @@ -5404,14 +5404,16 @@
1.313      using open_contains_ball by blast
1.314    have [simp]: "\<And>n. cmod (1 + of_nat n) = 1 + of_nat n"
1.315      by (metis norm_of_nat of_nat_Suc)
1.316 +  have cint: "\<And>x. \<lbrakk>x \<noteq> w; cmod (x - w) < d\<rbrakk>
1.317 +         \<Longrightarrow> (\<lambda>z. (f' z / (z - x) ^ k - f' z / (z - w) ^ k) / (x * k - w * k)) contour_integrable_on \<gamma>"
1.318 +    apply (rule contour_integrable_div [OF contour_integrable_diff])
1.319 +    using int w d
1.320 +    by (force simp: dist_norm norm_minus_commute intro!: has_contour_integral_integrable)+
1.321    have 1: "\<forall>\<^sub>F n in at w. (\<lambda>x. f' x * (inverse (x - n) ^ k - inverse (x - w) ^ k) / (n - w) / of_nat k)
1.322                           contour_integrable_on \<gamma>"
1.323 -    apply (simp add: eventually_at)
1.324 +    unfolding eventually_at
1.325      apply (rule_tac x=d in exI)
1.326 -    apply (simp add: \<open>d > 0\<close> dist_norm field_simps, clarify)
1.327 -    apply (rule contour_integrable_div [OF contour_integrable_diff])
1.328 -    using int w d
1.329 -    apply (force simp:  dist_norm norm_minus_commute intro!: has_contour_integral_integrable)+
1.330 +    apply (simp add: \<open>d > 0\<close> dist_norm field_simps cint)
1.331      done
1.332    have bim_g: "bounded (image f' (path_image \<gamma>))"
1.333      by (simp add: compact_imp_bounded compact_continuous_image compact_valid_path_image assms)
1.334 @@ -5424,7 +5426,7 @@
1.335    proof -
1.336      have *: "cmod ((inverse (x - u) ^ k - inverse (x - w) ^ k) / ((u - w) * k) - inverse (x - w) ^ Suc k)   < e"
1.337              if x: "x \<in> path_image \<gamma>" and "u \<noteq> w" and uwd: "cmod (u - w) < d/2"
1.338 -                and uw_less: "cmod (u - w) < e * (d / 2) ^ (k+2) / (1 + real k)"
1.339 +                and uw_less: "cmod (u - w) < e * (d/2) ^ (k+2) / (1 + real k)"
1.340              for u x
1.341      proof -
1.342        define ff where [abs_def]:
1.343 @@ -5434,8 +5436,8 @@
1.344             else (k * of_real(Suc k)) / (x - w)^(k + 2))" for n :: nat and w
1.345        have km1: "\<And>z::complex. z \<noteq> 0 \<Longrightarrow> z ^ (k - Suc 0) = z ^ k / z"
1.346          by (simp add: field_simps) (metis Suc_pred \<open>k \<noteq> 0\<close> neq0_conv power_Suc)
1.347 -      have ff1: "(ff i has_field_derivative ff (Suc i) z) (at z within ball w (d / 2))"
1.348 -              if "z \<in> ball w (d / 2)" "i \<le> 1" for i z
1.349 +      have ff1: "(ff i has_field_derivative ff (Suc i) z) (at z within ball w (d/2))"
1.350 +              if "z \<in> ball w (d/2)" "i \<le> 1" for i z
1.351        proof -
1.352          have "z \<notin> path_image \<gamma>"
1.353            using \<open>x \<in> path_image \<gamma>\<close> d that ball_divide_subset_numeral by blast
1.354 @@ -5452,22 +5454,18 @@
1.355        qed
1.356        { fix a::real and b::real assume ab: "a > 0" "b > 0"
1.357          then have "k * (1 + real k) * (1 / a) \<le> k * (1 + real k) * (4 / b) \<longleftrightarrow> b \<le> 4 * a"
1.358 -          apply (subst mult_le_cancel_left_pos)
1.359 -          using \<open>k \<noteq> 0\<close>
1.360 -          apply (auto simp: divide_simps)
1.361 -          done
1.362 +          by (subst mult_le_cancel_left_pos) (use \<open>k \<noteq> 0\<close> in \<open>auto simp: divide_simps\<close>)
1.363          with ab have "real k * (1 + real k) / a \<le> (real k * 4 + real k * real k * 4) / b \<longleftrightarrow> b \<le> 4 * a"
1.364            by (simp add: field_simps)
1.365        } note canc = this
1.366 -      have ff2: "cmod (ff (Suc 1) v) \<le> real (k * (k + 1)) / (d / 2) ^ (k + 2)"
1.367 -                if "v \<in> ball w (d / 2)" for v
1.368 +      have ff2: "cmod (ff (Suc 1) v) \<le> real (k * (k + 1)) / (d/2) ^ (k + 2)"
1.369 +                if "v \<in> ball w (d/2)" for v
1.370        proof -
1.371 +        have lessd: "\<And>z. cmod (\<gamma> z - v) < d/2 \<Longrightarrow> cmod (w - \<gamma> z) < d"
1.372 +          by (metis that norm_minus_commute norm_triangle_half_r dist_norm mem_ball)
1.373          have "d/2 \<le> cmod (x - v)" using d x that
1.374 -          apply (simp add: dist_norm path_image_def ball_def not_less [symmetric] del: divide_const_simps, clarify)
1.375 -          apply (drule subsetD)
1.376 -           prefer 2 apply blast
1.377 -          apply (metis norm_minus_commute norm_triangle_half_r CollectI)
1.378 -          done
1.379 +          using lessd d x
1.380 +          by (auto simp add: dist_norm path_image_def ball_def not_less [symmetric] del: divide_const_simps)
1.381          then have "d \<le> cmod (x - v) * 2"
1.382            by (simp add: divide_simps)
1.383          then have dpow_le: "d ^ (k+2) \<le> (cmod (x - v) * 2) ^ (k+2)"
1.384 @@ -5475,24 +5473,22 @@
1.385          have "x \<noteq> v" using that
1.386            using \<open>x \<in> path_image \<gamma>\<close> ball_divide_subset_numeral d by fastforce
1.387          then show ?thesis
1.388 -        using \<open>d > 0\<close>
1.389 -        apply (simp add: ff_def norm_mult norm_divide norm_power dist_norm canc)
1.390 -        using dpow_le
1.391 -        apply (simp add: algebra_simps divide_simps mult_less_0_iff)
1.392 +        using \<open>d > 0\<close> apply (simp add: ff_def norm_mult norm_divide norm_power dist_norm canc)
1.393 +        using dpow_le apply (simp add: algebra_simps divide_simps mult_less_0_iff)
1.394          done
1.395        qed
1.396 -      have ub: "u \<in> ball w (d / 2)"
1.397 +      have ub: "u \<in> ball w (d/2)"
1.398          using uwd by (simp add: dist_commute dist_norm)
1.399        have "cmod (inverse (x - u) ^ k - (inverse (x - w) ^ k + of_nat k * (u - w) / ((x - w) * (x - w) ^ k)))
1.400 -                  \<le> (real k * 4 + real k * real k * 4) * (cmod (u - w) * cmod (u - w)) / (d * (d * (d / 2) ^ k))"
1.401 +                  \<le> (real k * 4 + real k * real k * 4) * (cmod (u - w) * cmod (u - w)) / (d * (d * (d/2) ^ k))"
1.402          using complex_taylor [OF _ ff1 ff2 _ ub, of w, simplified]
1.403          by (simp add: ff_def \<open>0 < d\<close>)
1.404        then have "cmod (inverse (x - u) ^ k - (inverse (x - w) ^ k + of_nat k * (u - w) / ((x - w) * (x - w) ^ k)))
1.405 -                  \<le> (cmod (u - w) * real k) * (1 + real k) * cmod (u - w) / (d / 2) ^ (k+2)"
1.406 +                  \<le> (cmod (u - w) * real k) * (1 + real k) * cmod (u - w) / (d/2) ^ (k+2)"
1.407          by (simp add: field_simps)
1.408        then have "cmod (inverse (x - u) ^ k - (inverse (x - w) ^ k + of_nat k * (u - w) / ((x - w) * (x - w) ^ k)))
1.409                   / (cmod (u - w) * real k)
1.410 -                  \<le> (1 + real k) * cmod (u - w) / (d / 2) ^ (k+2)"
1.411 +                  \<le> (1 + real k) * cmod (u - w) / (d/2) ^ (k+2)"
1.412          using \<open>k \<noteq> 0\<close> \<open>u \<noteq> w\<close> by (simp add: mult_ac zero_less_mult_iff pos_divide_le_eq)
1.413        also have "\<dots> < e"
1.414          using uw_less \<open>0 < d\<close> by (simp add: mult_ac divide_simps)
1.415 @@ -5503,7 +5499,7 @@
1.416          using uwd \<open>0 < d\<close> x d by (force simp: dist_norm ball_def norm_minus_commute)
1.417        show ?thesis
1.418          apply (rule le_less_trans [OF _ e])
1.419 -        using \<open>k \<noteq> 0\<close> \<open>x \<noteq> u\<close>  \<open>u \<noteq> w\<close>
1.420 +        using \<open>k \<noteq> 0\<close> \<open>x \<noteq> u\<close> \<open>u \<noteq> w\<close>
1.421          apply (simp add: field_simps norm_divide [symmetric])
1.422          done
1.423      qed
1.424 @@ -5538,8 +5534,7 @@
1.425                               inverse (\<gamma> x - w) * inverse (\<gamma> x - w) ^ k)"
1.426          by (simp add: norm_mult)
1.427        also have "\<dots> < cmod (f' (\<gamma> x)) * (e/C)"
1.428 -        apply (rule mult_strict_left_mono [OF ec])
1.429 -        using False by simp
1.430 +        using False mult_strict_left_mono [OF ec] by force
1.431        also have "\<dots> \<le> e" using C
1.432          by (metis False \<open>0 < e\<close> frac_le less_eq_real_def mult.commute pos_le_divide_eq x zero_less_norm_iff)
1.433        finally show ?thesis .
1.434 @@ -5557,13 +5552,17 @@
1.435      by (rule contour_integral_uniform_limit [OF 1 2 leB \<gamma>]) auto
1.436    have **: "contour_integral \<gamma> (\<lambda>x. f' x * (inverse (x - u) ^ k - inverse (x - w) ^ k) / ((u - w) * k)) =
1.437                (f u - f w) / (u - w) / k"
1.438 -           if "dist u w < d" for u
1.439 -    apply (rule contour_integral_unique)
1.440 -    apply (simp add: diff_divide_distrib algebra_simps)
1.441 -    apply (rule has_contour_integral_diff; rule has_contour_integral_div; simp add: field_simps; rule int)
1.442 -    apply (metis contra_subsetD d dist_commute mem_ball that)
1.443 -    apply (rule w)
1.444 -    done
1.445 +    if "dist u w < d" for u
1.446 +  proof -
1.447 +    have u: "u \<in> s - path_image \<gamma>"
1.448 +      by (metis subsetD d dist_commute mem_ball that)
1.449 +    show ?thesis
1.450 +      apply (rule contour_integral_unique)
1.451 +      apply (simp add: diff_divide_distrib algebra_simps)
1.452 +      apply (intro has_contour_integral_diff has_contour_integral_div)
1.453 +      using u w apply (simp_all add: field_simps int)
1.454 +      done
1.455 +  qed
1.456    show ?thes2
1.457      apply (simp add: has_field_derivative_iff del: power_Suc)
1.458      apply (rule Lim_transform_within [OF tendsto_mult_left [OF *] \<open>0 < d\<close> ])
1.459 @@ -5628,14 +5627,14 @@
1.460  subsection\<open>Existence of all higher derivatives\<close>
1.461
1.462  proposition derivative_is_holomorphic:
1.463 -  assumes "open s"
1.464 -      and fder: "\<And>z. z \<in> s \<Longrightarrow> (f has_field_derivative f' z) (at z)"
1.465 -    shows "f' holomorphic_on s"
1.466 +  assumes "open S"
1.467 +      and fder: "\<And>z. z \<in> S \<Longrightarrow> (f has_field_derivative f' z) (at z)"
1.468 +    shows "f' holomorphic_on S"
1.469  proof -
1.470 -  have *: "\<exists>h. (f' has_field_derivative h) (at z)" if "z \<in> s" for z
1.471 +  have *: "\<exists>h. (f' has_field_derivative h) (at z)" if "z \<in> S" for z
1.472    proof -
1.473 -    obtain r where "r > 0" and r: "cball z r \<subseteq> s"
1.474 -      using open_contains_cball \<open>z \<in> s\<close> \<open>open s\<close> by blast
1.475 +    obtain r where "r > 0" and r: "cball z r \<subseteq> S"
1.476 +      using open_contains_cball \<open>z \<in> S\<close> \<open>open S\<close> by blast
1.477      then have holf_cball: "f holomorphic_on cball z r"
1.478        apply (simp add: holomorphic_on_def)
1.479        using field_differentiable_at_within field_differentiable_def fder by blast
1.480 @@ -5673,38 +5672,38 @@
1.481        done
1.482    qed
1.483    show ?thesis
1.484 -    by (simp add: holomorphic_on_open [OF \<open>open s\<close>] *)
1.485 +    by (simp add: holomorphic_on_open [OF \<open>open S\<close>] *)
1.486  qed
1.487
1.488  lemma holomorphic_deriv [holomorphic_intros]:
1.489 -    "\<lbrakk>f holomorphic_on s; open s\<rbrakk> \<Longrightarrow> (deriv f) holomorphic_on s"
1.490 +    "\<lbrakk>f holomorphic_on S; open S\<rbrakk> \<Longrightarrow> (deriv f) holomorphic_on S"
1.491  by (metis DERIV_deriv_iff_field_differentiable at_within_open derivative_is_holomorphic holomorphic_on_def)
1.492
1.493 -lemma analytic_deriv [analytic_intros]: "f analytic_on s \<Longrightarrow> (deriv f) analytic_on s"
1.494 +lemma analytic_deriv [analytic_intros]: "f analytic_on S \<Longrightarrow> (deriv f) analytic_on S"
1.495    using analytic_on_holomorphic holomorphic_deriv by auto
1.496
1.497 -lemma holomorphic_higher_deriv [holomorphic_intros]: "\<lbrakk>f holomorphic_on s; open s\<rbrakk> \<Longrightarrow> (deriv ^^ n) f holomorphic_on s"
1.498 +lemma holomorphic_higher_deriv [holomorphic_intros]: "\<lbrakk>f holomorphic_on S; open S\<rbrakk> \<Longrightarrow> (deriv ^^ n) f holomorphic_on S"
1.499    by (induction n) (auto simp: holomorphic_deriv)
1.500
1.501 -lemma analytic_higher_deriv [analytic_intros]: "f analytic_on s \<Longrightarrow> (deriv ^^ n) f analytic_on s"
1.502 +lemma analytic_higher_deriv [analytic_intros]: "f analytic_on S \<Longrightarrow> (deriv ^^ n) f analytic_on S"
1.503    unfolding analytic_on_def using holomorphic_higher_deriv by blast
1.504
1.505  lemma has_field_derivative_higher_deriv:
1.506 -     "\<lbrakk>f holomorphic_on s; open s; x \<in> s\<rbrakk>
1.507 +     "\<lbrakk>f holomorphic_on S; open S; x \<in> S\<rbrakk>
1.508        \<Longrightarrow> ((deriv ^^ n) f has_field_derivative (deriv ^^ (Suc n)) f x) (at x)"
1.509  by (metis (no_types, hide_lams) DERIV_deriv_iff_field_differentiable at_within_open comp_apply
1.510           funpow.simps(2) holomorphic_higher_deriv holomorphic_on_def)
1.511
1.512  lemma valid_path_compose_holomorphic:
1.513 -  assumes "valid_path g" and holo:"f holomorphic_on s" and "open s" "path_image g \<subseteq> s"
1.514 +  assumes "valid_path g" and holo:"f holomorphic_on S" and "open S" "path_image g \<subseteq> S"
1.515    shows "valid_path (f \<circ> g)"
1.516  proof (rule valid_path_compose[OF \<open>valid_path g\<close>])
1.517    fix x assume "x \<in> path_image g"
1.518    then show "f field_differentiable at x"
1.519      using analytic_on_imp_differentiable_at analytic_on_open assms holo by blast
1.520  next
1.521 -  have "deriv f holomorphic_on s"
1.522 -    using holomorphic_deriv holo \<open>open s\<close> by auto
1.523 +  have "deriv f holomorphic_on S"
1.524 +    using holomorphic_deriv holo \<open>open S\<close> by auto
1.525    then show "continuous_on (path_image g) (deriv f)"
1.526      using assms(4) holomorphic_on_imp_continuous_on holomorphic_on_subset by auto
1.527  qed
1.528 @@ -5713,15 +5712,15 @@
1.529  subsection\<open>Morera's theorem\<close>
1.530
1.531  lemma Morera_local_triangle_ball:
1.532 -  assumes "\<And>z. z \<in> s
1.533 +  assumes "\<And>z. z \<in> S
1.534            \<Longrightarrow> \<exists>e a. 0 < e \<and> z \<in> ball a e \<and> continuous_on (ball a e) f \<and>
1.535                      (\<forall>b c. closed_segment b c \<subseteq> ball a e
1.536                             \<longrightarrow> contour_integral (linepath a b) f +
1.537                                 contour_integral (linepath b c) f +
1.538                                 contour_integral (linepath c a) f = 0)"
1.539 -  shows "f analytic_on s"
1.540 +  shows "f analytic_on S"
1.541  proof -
1.542 -  { fix z  assume "z \<in> s"
1.543 +  { fix z  assume "z \<in> S"
1.544      with assms obtain e a where
1.545              "0 < e" and z: "z \<in> ball a e" and contf: "continuous_on (ball a e) f"
1.546          and 0: "\<And>b c. closed_segment b c \<subseteq> ball a e
1.547 @@ -5733,29 +5732,31 @@
1.548      have sb_ball: "ball z (e - dist a z) \<subseteq> ball a e"
1.549        by (simp add: dist_commute ball_subset_ball_iff)
1.550      have "\<exists>e>0. f holomorphic_on ball z e"
1.551 -      apply (rule_tac x="e - dist a z" in exI)
1.552 -      apply (simp add: az)
1.553 -      apply (rule holomorphic_on_subset [OF _ sb_ball])
1.554 -      apply (rule derivative_is_holomorphic[OF open_ball])
1.555 -      apply (rule triangle_contour_integrals_starlike_primitive [OF contf _ open_ball, of a])
1.556 -         apply (simp_all add: 0 \<open>0 < e\<close>)
1.557 -      apply (meson \<open>0 < e\<close> centre_in_ball convex_ball convex_contains_segment mem_ball)
1.558 -      done
1.559 +    proof (intro exI conjI)
1.560 +      have sub_ball: "\<And>y. dist a y < e \<Longrightarrow> closed_segment a y \<subseteq> ball a e"
1.561 +        by (meson \<open>0 < e\<close> centre_in_ball convex_ball convex_contains_segment mem_ball)
1.562 +      show "f holomorphic_on ball z (e - dist a z)"
1.563 +        apply (rule holomorphic_on_subset [OF _ sb_ball])
1.564 +        apply (rule derivative_is_holomorphic[OF open_ball])
1.565 +        apply (rule triangle_contour_integrals_starlike_primitive [OF contf _ open_ball, of a])
1.566 +           apply (simp_all add: 0 \<open>0 < e\<close> sub_ball)
1.567 +        done
1.568 +    qed (simp add: az)
1.569    }
1.570    then show ?thesis
1.571      by (simp add: analytic_on_def)
1.572  qed
1.573
1.574  lemma Morera_local_triangle:
1.575 -  assumes "\<And>z. z \<in> s
1.576 +  assumes "\<And>z. z \<in> S
1.577            \<Longrightarrow> \<exists>t. open t \<and> z \<in> t \<and> continuous_on t f \<and>
1.578                    (\<forall>a b c. convex hull {a,b,c} \<subseteq> t
1.579                                \<longrightarrow> contour_integral (linepath a b) f +
1.580                                    contour_integral (linepath b c) f +
1.581                                    contour_integral (linepath c a) f = 0)"
1.582 -  shows "f analytic_on s"
1.583 +  shows "f analytic_on S"
1.584  proof -
1.585 -  { fix z  assume "z \<in> s"
1.586 +  { fix z  assume "z \<in> S"
1.587      with assms obtain t where
1.588              "open t" and z: "z \<in> t" and contf: "continuous_on t f"
1.589          and 0: "\<And>a b c. convex hull {a,b,c} \<subseteq> t
1.590 @@ -5767,29 +5768,27 @@
1.591        using open_contains_ball by blast
1.592      have [simp]: "continuous_on (ball z e) f" using contf
1.593        using continuous_on_subset e by blast
1.594 -    have "\<exists>e a. 0 < e \<and>
1.595 -               z \<in> ball a e \<and>
1.596 -               continuous_on (ball a e) f \<and>
1.597 -               (\<forall>b c. closed_segment b c \<subseteq> ball a e \<longrightarrow>
1.598 -                      contour_integral (linepath a b) f + contour_integral (linepath b c) f + contour_integral (linepath c a) f = 0)"
1.599 -      apply (rule_tac x=e in exI)
1.600 -      apply (rule_tac x=z in exI)
1.601 -      apply (simp add: \<open>e > 0\<close>, clarify)
1.602 -      apply (rule 0)
1.603 -      apply (meson z \<open>0 < e\<close> centre_in_ball closed_segment_subset convex_ball dual_order.trans e starlike_convex_subset)
1.604 -      done
1.605 +    have eq0: "\<And>b c. closed_segment b c \<subseteq> ball z e \<Longrightarrow>
1.606 +                         contour_integral (linepath z b) f +
1.607 +                         contour_integral (linepath b c) f +
1.608 +                         contour_integral (linepath c z) f = 0"
1.609 +      by (meson 0 z \<open>0 < e\<close> centre_in_ball closed_segment_subset convex_ball dual_order.trans e starlike_convex_subset)
1.610 +    have "\<exists>e a. 0 < e \<and> z \<in> ball a e \<and> continuous_on (ball a e) f \<and>
1.611 +                (\<forall>b c. closed_segment b c \<subseteq> ball a e \<longrightarrow>
1.612 +                       contour_integral (linepath a b) f + contour_integral (linepath b c) f + contour_integral (linepath c a) f = 0)"
1.613 +      using \<open>e > 0\<close> eq0 by force
1.614    }
1.615    then show ?thesis
1.616      by (simp add: Morera_local_triangle_ball)
1.617  qed
1.618
1.619  proposition Morera_triangle:
1.620 -    "\<lbrakk>continuous_on s f; open s;
1.621 -      \<And>a b c. convex hull {a,b,c} \<subseteq> s
1.622 +    "\<lbrakk>continuous_on S f; open S;
1.623 +      \<And>a b c. convex hull {a,b,c} \<subseteq> S
1.624                \<longrightarrow> contour_integral (linepath a b) f +
1.625                    contour_integral (linepath b c) f +
1.626                    contour_integral (linepath c a) f = 0\<rbrakk>
1.627 -     \<Longrightarrow> f analytic_on s"
1.628 +     \<Longrightarrow> f analytic_on S"
1.629    using Morera_local_triangle by blast
1.630
1.631
1.632 @@ -5798,10 +5797,10 @@
1.633
1.634  lemma higher_deriv_linear [simp]:
1.635      "(deriv ^^ n) (\<lambda>w. c*w) = (\<lambda>z. if n = 0 then c*z else if n = 1 then c else 0)"
1.636 -  by (induction n) (auto simp: deriv_const deriv_linear)
1.637 +  by (induction n) auto
1.638
1.639  lemma higher_deriv_const [simp]: "(deriv ^^ n) (\<lambda>w. c) = (\<lambda>w. if n=0 then c else 0)"
1.640 -  by (induction n) (auto simp: deriv_const)
1.641 +  by (induction n) auto
1.642
1.643  lemma higher_deriv_ident [simp]:
1.644       "(deriv ^^ n) (\<lambda>w. w) z = (if n = 0 then z else if n = 1 then 1 else 0)"
1.645 @@ -5820,7 +5819,7 @@
1.646    by (metis DERIV_chain comp_funpow comp_id funpow_swap1 mult.right_neutral)
1.647
1.648  proposition higher_deriv_uminus:
1.649 -  assumes "f holomorphic_on s" "open s" and z: "z \<in> s"
1.650 +  assumes "f holomorphic_on S" "open S" and z: "z \<in> S"
1.651      shows "(deriv ^^ n) (\<lambda>w. -(f w)) z = - ((deriv ^^ n) f z)"
1.652  using z
1.653  proof (induction n arbitrary: z)
1.654 @@ -5829,18 +5828,18 @@
1.655    case (Suc n z)
1.656    have *: "((deriv ^^ n) f has_field_derivative deriv ((deriv ^^ n) f) z) (at z)"
1.657      using Suc.prems assms has_field_derivative_higher_deriv by auto
1.658 -  show ?case
1.659 -    apply simp
1.660 -    apply (rule DERIV_imp_deriv)
1.661 +  have "((deriv ^^ n) (\<lambda>w. - f w) has_field_derivative - deriv ((deriv ^^ n) f) z) (at z)"
1.662      apply (rule DERIV_transform_within_open [of "\<lambda>w. -((deriv ^^ n) f w)"])
1.663 -    apply (rule derivative_eq_intros | rule * refl assms Suc)+
1.664 -    apply (simp add: Suc)
1.665 +       apply (rule derivative_eq_intros | rule * refl assms)+
1.666 +     apply (auto simp add: Suc)
1.667      done
1.668 +  then show ?case
1.669 +    by (simp add: DERIV_imp_deriv)
1.670  qed
1.671
1.672  proposition higher_deriv_add:
1.673    fixes z::complex
1.674 -  assumes "f holomorphic_on s" "g holomorphic_on s" "open s" and z: "z \<in> s"
1.675 +  assumes "f holomorphic_on S" "g holomorphic_on S" "open S" and z: "z \<in> S"
1.676      shows "(deriv ^^ n) (\<lambda>w. f w + g w) z = (deriv ^^ n) f z + (deriv ^^ n) g z"
1.677  using z
1.678  proof (induction n arbitrary: z)
1.679 @@ -5850,18 +5849,19 @@
1.680    have *: "((deriv ^^ n) f has_field_derivative deriv ((deriv ^^ n) f) z) (at z)"
1.681            "((deriv ^^ n) g has_field_derivative deriv ((deriv ^^ n) g) z) (at z)"
1.682      using Suc.prems assms has_field_derivative_higher_deriv by auto
1.683 -  show ?case
1.684 -    apply simp
1.685 -    apply (rule DERIV_imp_deriv)
1.686 +  have "((deriv ^^ n) (\<lambda>w. f w + g w) has_field_derivative
1.687 +        deriv ((deriv ^^ n) f) z + deriv ((deriv ^^ n) g) z) (at z)"
1.688      apply (rule DERIV_transform_within_open [of "\<lambda>w. (deriv ^^ n) f w + (deriv ^^ n) g w"])
1.689 -    apply (rule derivative_eq_intros | rule * refl assms Suc)+
1.690 -    apply (simp add: Suc)
1.691 +       apply (rule derivative_eq_intros | rule * refl assms)+
1.692 +     apply (auto simp add: Suc)
1.693      done
1.694 +  then show ?case
1.695 +    by (simp add: DERIV_imp_deriv)
1.696  qed
1.697
1.698  corollary higher_deriv_diff:
1.699    fixes z::complex
1.700 -  assumes "f holomorphic_on s" "g holomorphic_on s" "open s" and z: "z \<in> s"
1.701 +  assumes "f holomorphic_on S" "g holomorphic_on S" "open S" and z: "z \<in> S"
1.702      shows "(deriv ^^ n) (\<lambda>w. f w - g w) z = (deriv ^^ n) f z - (deriv ^^ n) g z"
1.703    apply (simp only: Groups.group_add_class.diff_conv_add_uminus higher_deriv_add)
1.704    apply (subst higher_deriv_add)
1.705 @@ -5874,7 +5874,7 @@
1.706
1.707  proposition higher_deriv_mult:
1.708    fixes z::complex
1.709 -  assumes "f holomorphic_on s" "g holomorphic_on s" "open s" and z: "z \<in> s"
1.710 +  assumes "f holomorphic_on S" "g holomorphic_on S" "open S" and z: "z \<in> S"
1.711      shows "(deriv ^^ n) (\<lambda>w. f w * g w) z =
1.712             (\<Sum>i = 0..n. of_nat (n choose i) * (deriv ^^ i) f z * (deriv ^^ (n - i)) g z)"
1.713  using z
1.714 @@ -5892,23 +5892,26 @@
1.715      apply (subst (4) sum_Suc_reindex)
1.716      apply (auto simp: algebra_simps Suc_diff_le intro: sum.cong)
1.717      done
1.718 -  show ?case
1.719 -    apply (simp only: funpow.simps o_apply)
1.720 -    apply (rule DERIV_imp_deriv)
1.721 +  have "((deriv ^^ n) (\<lambda>w. f w * g w) has_field_derivative
1.722 +         (\<Sum>i = 0..Suc n. (Suc n choose i) * (deriv ^^ i) f z * (deriv ^^ (Suc n - i)) g z))
1.723 +        (at z)"
1.724      apply (rule DERIV_transform_within_open
1.725 -             [of "\<lambda>w. (\<Sum>i = 0..n. of_nat (n choose i) * (deriv ^^ i) f w * (deriv ^^ (n - i)) g w)"])
1.726 -    apply (simp add: algebra_simps)
1.727 -    apply (rule DERIV_cong [OF DERIV_sum])
1.728 -    apply (rule DERIV_cmult)
1.729 -    apply (auto intro: DERIV_mult * sumeq \<open>open s\<close> Suc.prems Suc.IH [symmetric])
1.730 +        [of "\<lambda>w. (\<Sum>i = 0..n. of_nat (n choose i) * (deriv ^^ i) f w * (deriv ^^ (n - i)) g w)"])
1.731 +       apply (simp add: algebra_simps)
1.732 +       apply (rule DERIV_cong [OF DERIV_sum])
1.733 +        apply (rule DERIV_cmult)
1.734 +        apply (auto intro: DERIV_mult * sumeq \<open>open S\<close> Suc.prems Suc.IH [symmetric])
1.735      done
1.736 +  then show ?case
1.737 +    unfolding funpow.simps o_apply
1.738 +    by (simp add: DERIV_imp_deriv)
1.739  qed
1.740
1.741
1.742  proposition higher_deriv_transform_within_open:
1.743    fixes z::complex
1.744 -  assumes "f holomorphic_on s" "g holomorphic_on s" "open s" and z: "z \<in> s"
1.745 -      and fg: "\<And>w. w \<in> s \<Longrightarrow> f w = g w"
1.746 +  assumes "f holomorphic_on S" "g holomorphic_on S" "open S" and z: "z \<in> S"
1.747 +      and fg: "\<And>w. w \<in> S \<Longrightarrow> f w = g w"
1.748      shows "(deriv ^^ i) f z = (deriv ^^ i) g z"
1.749  using z
1.750  by (induction i arbitrary: z)
1.751 @@ -5916,45 +5919,41 @@
1.752
1.753  proposition higher_deriv_compose_linear:
1.754    fixes z::complex
1.755 -  assumes f: "f holomorphic_on t" and s: "open s" and t: "open t" and z: "z \<in> s"
1.756 -      and fg: "\<And>w. w \<in> s \<Longrightarrow> u * w \<in> t"
1.757 +  assumes f: "f holomorphic_on T" and S: "open S" and T: "open T" and z: "z \<in> S"
1.758 +      and fg: "\<And>w. w \<in> S \<Longrightarrow> u * w \<in> T"
1.759      shows "(deriv ^^ n) (\<lambda>w. f (u * w)) z = u^n * (deriv ^^ n) f (u * z)"
1.760  using z
1.761  proof (induction n arbitrary: z)
1.762    case 0 then show ?case by simp
1.763  next
1.764    case (Suc n z)
1.765 -  have holo0: "f holomorphic_on ( *) u ` s"
1.766 +  have holo0: "f holomorphic_on ( *) u ` S"
1.767      by (meson fg f holomorphic_on_subset image_subset_iff)
1.768 -  have holo1: "(\<lambda>w. f (u * w)) holomorphic_on s"
1.769 +  have holo2: "(deriv ^^ n) f holomorphic_on ( * ) u ` S"
1.770 +    by (meson f fg holomorphic_higher_deriv holomorphic_on_subset image_subset_iff T)
1.771 +  have holo3: "(\<lambda>z. u ^ n * (deriv ^^ n) f (u * z)) holomorphic_on S"
1.772 +    by (intro holo2 holomorphic_on_compose [where g="(deriv ^^ n) f", unfolded o_def] holomorphic_intros)
1.773 +  have holo1: "(\<lambda>w. f (u * w)) holomorphic_on S"
1.774      apply (rule holomorphic_on_compose [where g=f, unfolded o_def])
1.775      apply (rule holo0 holomorphic_intros)+
1.776      done
1.777 -  have holo2: "(\<lambda>z. u ^ n * (deriv ^^ n) f (u * z)) holomorphic_on s"
1.778 -    apply (rule holomorphic_intros)+
1.779 -    apply (rule holomorphic_on_compose [where g="(deriv ^^ n) f", unfolded o_def])
1.780 -    apply (rule holomorphic_intros)
1.781 -    apply (rule holomorphic_on_subset [where s=t])
1.782 -    apply (rule holomorphic_intros assms)+
1.783 -    apply (blast intro: fg)
1.784 -    done
1.785    have "deriv ((deriv ^^ n) (\<lambda>w. f (u * w))) z = deriv (\<lambda>z. u^n * (deriv ^^ n) f (u*z)) z"
1.786 -    apply (rule complex_derivative_transform_within_open [OF _ holo2 s Suc.prems])
1.787 -    apply (rule holomorphic_higher_deriv [OF holo1 s])
1.788 +    apply (rule complex_derivative_transform_within_open [OF _ holo3 S Suc.prems])
1.789 +    apply (rule holomorphic_higher_deriv [OF holo1 S])
1.790      apply (simp add: Suc.IH)
1.791      done
1.792    also have "\<dots> = u^n * deriv (\<lambda>z. (deriv ^^ n) f (u * z)) z"
1.793      apply (rule deriv_cmult)
1.794      apply (rule analytic_on_imp_differentiable_at [OF _ Suc.prems])
1.795 -    apply (rule analytic_on_compose_gen [where g="(deriv ^^ n) f" and T=t, unfolded o_def])
1.796 +    apply (rule analytic_on_compose_gen [where g="(deriv ^^ n) f" and T=T, unfolded o_def])
1.797        apply (simp add: analytic_on_linear)
1.798 -     apply (simp add: analytic_on_open f holomorphic_higher_deriv t)
1.799 +     apply (simp add: analytic_on_open f holomorphic_higher_deriv T)
1.800      apply (blast intro: fg)
1.801      done
1.802    also have "\<dots> = u * u ^ n * deriv ((deriv ^^ n) f) (u * z)"
1.803        apply (subst complex_derivative_chain [where g = "(deriv ^^ n) f" and f = "( *) u", unfolded o_def])
1.804        apply (rule derivative_intros)
1.805 -      using Suc.prems field_differentiable_def f fg has_field_derivative_higher_deriv t apply blast
1.806 +      using Suc.prems field_differentiable_def f fg has_field_derivative_higher_deriv T apply blast
1.807        apply (simp add: deriv_linear)
1.808        done
1.809    finally show ?case
1.810 @@ -6002,26 +6001,26 @@
1.811
1.812  proposition no_isolated_singularity:
1.813    fixes z::complex
1.814 -  assumes f: "continuous_on s f" and holf: "f holomorphic_on (s - k)" and s: "open s" and k: "finite k"
1.815 -    shows "f holomorphic_on s"
1.816 +  assumes f: "continuous_on S f" and holf: "f holomorphic_on (S - K)" and S: "open S" and K: "finite K"
1.817 +    shows "f holomorphic_on S"
1.818  proof -
1.819    { fix z
1.820 -    assume "z \<in> s" and cdf: "\<And>x. x\<in>s - k \<Longrightarrow> f field_differentiable at x"
1.821 +    assume "z \<in> S" and cdf: "\<And>x. x\<in>S - K \<Longrightarrow> f field_differentiable at x"
1.822      have "f field_differentiable at z"
1.823 -    proof (cases "z \<in> k")
1.824 -      case False then show ?thesis by (blast intro: cdf \<open>z \<in> s\<close>)
1.825 +    proof (cases "z \<in> K")
1.826 +      case False then show ?thesis by (blast intro: cdf \<open>z \<in> S\<close>)
1.827      next
1.828        case True
1.829 -      with finite_set_avoid [OF k, of z]
1.830 -      obtain d where "d>0" and d: "\<And>x. \<lbrakk>x\<in>k; x \<noteq> z\<rbrakk> \<Longrightarrow> d \<le> dist z x"
1.831 +      with finite_set_avoid [OF K, of z]
1.832 +      obtain d where "d>0" and d: "\<And>x. \<lbrakk>x\<in>K; x \<noteq> z\<rbrakk> \<Longrightarrow> d \<le> dist z x"
1.833          by blast
1.834 -      obtain e where "e>0" and e: "ball z e \<subseteq> s"
1.835 -        using  s \<open>z \<in> s\<close> by (force simp: open_contains_ball)
1.836 +      obtain e where "e>0" and e: "ball z e \<subseteq> S"
1.837 +        using  S \<open>z \<in> S\<close> by (force simp: open_contains_ball)
1.838        have fde: "continuous_on (ball z (min d e)) f"
1.839          by (metis Int_iff ball_min_Int continuous_on_subset e f subsetI)
1.840        obtain g where "\<And>w. w \<in> ball z (min d e) \<Longrightarrow> (g has_field_derivative f w) (at w within ball z (min d e))"
1.841          apply (rule contour_integral_convex_primitive [OF convex_ball fde])
1.842 -        apply (rule Cauchy_theorem_triangle_cofinite [OF _ k])
1.843 +        apply (rule Cauchy_theorem_triangle_cofinite [OF _ K])
1.844           apply (metis continuous_on_subset [OF fde] closed_segment_subset convex_ball starlike_convex_subset)
1.845          apply (rule cdf)
1.846          apply (metis Diff_iff Int_iff ball_min_Int bot_least contra_subsetD convex_ball e insert_subset
1.847 @@ -6034,43 +6033,43 @@
1.848          by (metis open_ball \<open>0 < d\<close> \<open>0 < e\<close> at_within_open centre_in_ball min_less_iff_conj)
1.849      qed
1.850    }
1.851 -  with holf s k show ?thesis
1.852 +  with holf S K show ?thesis
1.853      by (simp add: holomorphic_on_open open_Diff finite_imp_closed field_differentiable_def [symmetric])
1.854  qed
1.855
1.856  lemma no_isolated_singularity':
1.857    fixes z::complex
1.858 -  assumes f: "\<And>z. z \<in> k \<Longrightarrow> (f \<longlongrightarrow> f z) (at z within s)"
1.859 -      and holf: "f holomorphic_on (s - k)" and s: "open s" and k: "finite k"
1.860 -    shows "f holomorphic_on s"
1.861 +  assumes f: "\<And>z. z \<in> K \<Longrightarrow> (f \<longlongrightarrow> f z) (at z within S)"
1.862 +      and holf: "f holomorphic_on (S - K)" and S: "open S" and K: "finite K"
1.863 +    shows "f holomorphic_on S"
1.864  proof (rule no_isolated_singularity[OF _ assms(2-)])
1.865 -  show "continuous_on s f" unfolding continuous_on_def
1.866 +  show "continuous_on S f" unfolding continuous_on_def
1.867    proof
1.868 -    fix z assume z: "z \<in> s"
1.869 -    show "(f \<longlongrightarrow> f z) (at z within s)"
1.870 -    proof (cases "z \<in> k")
1.871 +    fix z assume z: "z \<in> S"
1.872 +    show "(f \<longlongrightarrow> f z) (at z within S)"
1.873 +    proof (cases "z \<in> K")
1.874        case False
1.875 -      from holf have "continuous_on (s - k) f"
1.876 +      from holf have "continuous_on (S - K) f"
1.877          by (rule holomorphic_on_imp_continuous_on)
1.878 -      with z False have "(f \<longlongrightarrow> f z) (at z within (s - k))"
1.879 +      with z False have "(f \<longlongrightarrow> f z) (at z within (S - K))"
1.880          by (simp add: continuous_on_def)
1.881 -      also from z k s False have "at z within (s - k) = at z within s"
1.882 +      also from z K S False have "at z within (S - K) = at z within S"
1.883          by (subst (1 2) at_within_open) (auto intro: finite_imp_closed)
1.884 -      finally show "(f \<longlongrightarrow> f z) (at z within s)" .
1.885 +      finally show "(f \<longlongrightarrow> f z) (at z within S)" .
1.886      qed (insert assms z, simp_all)
1.887    qed
1.888  qed
1.889
1.890  proposition Cauchy_integral_formula_convex:
1.891 -    assumes s: "convex s" and k: "finite k" and contf: "continuous_on s f"
1.892 -        and fcd: "(\<And>x. x \<in> interior s - k \<Longrightarrow> f field_differentiable at x)"
1.893 -        and z: "z \<in> interior s" and vpg: "valid_path \<gamma>"
1.894 -        and pasz: "path_image \<gamma> \<subseteq> s - {z}" and loop: "pathfinish \<gamma> = pathstart \<gamma>"
1.895 +    assumes S: "convex S" and K: "finite K" and contf: "continuous_on S f"
1.896 +        and fcd: "(\<And>x. x \<in> interior S - K \<Longrightarrow> f field_differentiable at x)"
1.897 +        and z: "z \<in> interior S" and vpg: "valid_path \<gamma>"
1.898 +        and pasz: "path_image \<gamma> \<subseteq> S - {z}" and loop: "pathfinish \<gamma> = pathstart \<gamma>"
1.899        shows "((\<lambda>w. f w / (w - z)) has_contour_integral (2*pi * \<i> * winding_number \<gamma> z * f z)) \<gamma>"
1.900 -  apply (rule Cauchy_integral_formula_weak [OF s finite.emptyI contf])
1.901 +  apply (rule Cauchy_integral_formula_weak [OF S finite.emptyI contf])
1.902    apply (simp add: holomorphic_on_open [symmetric] field_differentiable_def)
1.903 -  using no_isolated_singularity [where s = "interior s"]
1.904 -  apply (metis k contf fcd holomorphic_on_open field_differentiable_def continuous_on_subset
1.905 +  using no_isolated_singularity [where S = "interior S"]
1.906 +  apply (metis K contf fcd holomorphic_on_open field_differentiable_def continuous_on_subset
1.907                 has_field_derivative_at_within holomorphic_on_def interior_subset open_interior)
1.908    using assms
1.909    apply auto
1.910 @@ -7330,7 +7329,7 @@
1.911          done
1.912        show ?thesis
1.913          unfolding d_def
1.914 -        apply (rule no_isolated_singularity [OF * _ u, where k = "{w}"])
1.915 +        apply (rule no_isolated_singularity [OF * _ u, where K = "{w}"])
1.916          apply (auto simp: field_differentiable_def [symmetric] holomorphic_on_open open_Diff u **)
1.917          done
1.918      qed
```
```     2.1 --- a/src/HOL/Analysis/Conformal_Mappings.thy	Fri Jun 01 09:57:33 2018 +0100
2.2 +++ b/src/HOL/Analysis/Conformal_Mappings.thy	Sat Jun 02 22:57:18 2018 +0100
2.3 @@ -2489,7 +2489,7 @@
2.4    finally have **: "g \<midarrow>z\<rightarrow> g z" .
2.5
2.6    have g_holo: "g holomorphic_on s"
2.7 -    by (rule no_isolated_singularity'[where k = "{z}"])
2.8 +    by (rule no_isolated_singularity'[where K = "{z}"])
2.9         (insert assms * **, simp_all add: at_within_open_NO_MATCH)
2.10    from s and this have "residue (\<lambda>w. g w / (w - z)) z = g z"
2.11      by (rule residue_simple)
```