merged
authorpaulson
Sat Jun 02 22:57:44 2018 +0100 (13 months ago)
changeset 683600f19c98fa7be
parent 68358 e761afd35baa
parent 68359 8cd3d0305269
child 68361 20375f232f3b
merged
     1.1 --- a/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Sat Jun 02 22:40:03 2018 +0200
     1.2 +++ b/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Sat Jun 02 22:57:44 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	Sat Jun 02 22:40:03 2018 +0200
     2.2 +++ b/src/HOL/Analysis/Conformal_Mappings.thy	Sat Jun 02 22:57:44 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)