Wenda Li's new material: residue theorem, argument_principle, Rouche_theorem

--- a/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy	Mon Mar 07 23:20:11 2016 +0100
+++ b/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy	Wed Mar 09 17:16:08 2016 +0000
@@ -567,17 +567,17 @@
 lemma closed_valid_path_image: "valid_path g \<Longrightarrow> closed(path_image g)"
   by (metis closed_path_image valid_path_imp_path)
 
-lemma valid_path_compose:
-  assumes "valid_path g"
-      and der:"\<And>x. x \<in> path_image g \<Longrightarrow> \<exists>f'. (f has_field_derivative f') (at x)"
-      and con: "continuous_on {0..1} (\<lambda>x. deriv f (g x))"
+proposition valid_path_compose:
+  assumes "valid_path g" 
+      and der: "\<And>x. x \<in> path_image g \<Longrightarrow> \<exists>f'. (f has_field_derivative f') (at x)"
+      and con: "continuous_on (path_image g) (deriv f)"
     shows "valid_path (f o g)"
 proof -
   obtain s where "finite s" and g_diff: "g C1_differentiable_on {0..1} - s"
     using `valid_path g` unfolding valid_path_def piecewise_C1_differentiable_on_def by auto
-  have "f \<circ> g differentiable at t" if "t \<in> {0..1} - s" for t
+  have "f \<circ> g differentiable at t" when "t\<in>{0..1} - s" for t
     proof (rule differentiable_chain_at)
-      show "g differentiable at t" using `valid_path g`
+      show "g differentiable at t" using `valid_path g` 
         by (meson C1_differentiable_on_eq \<open>g C1_differentiable_on {0..1} - s\<close> that)
     next
       have "g t\<in>path_image g" using that DiffD1 image_eqI path_image_def by metis
@@ -588,38 +588,42 @@
       then show "f differentiable at (g t)" using differentiableI by auto
     qed
   moreover have "continuous_on ({0..1} - s) (\<lambda>x. vector_derivative (f \<circ> g) (at x))"
-  proof (rule continuous_on_eq [where f = "\<lambda>x. vector_derivative g (at x) * deriv f (g x)"],
-      rule continuous_intros)
-    show "continuous_on ({0..1} - s) (\<lambda>x. vector_derivative g (at x))"
-      using g_diff C1_differentiable_on_eq by auto
-  next
-    show "continuous_on ({0..1} - s) (\<lambda>x. deriv f (g x))"
-      using con continuous_on_subset by blast
-  next
-    show "vector_derivative g (at t) * deriv f (g t) = vector_derivative (f \<circ> g) (at t)"
-         if "t \<in> {0..1} - s" for t
-    proof (rule vector_derivative_chain_at_general[symmetric])
-      show "g differentiable at t" by (meson C1_differentiable_on_eq g_diff that)
+    proof (rule continuous_on_eq [where f = "\<lambda>x. vector_derivative g (at x) * deriv f (g x)"],
+        rule continuous_intros)
+      show "continuous_on ({0..1} - s) (\<lambda>x. vector_derivative g (at x))"
+        using g_diff C1_differentiable_on_eq by auto
+    next
+      have "continuous_on {0..1} (\<lambda>x. deriv f (g x))" 
+        using continuous_on_compose[OF _ con[unfolded path_image_def],unfolded comp_def] 
+          `valid_path g` piecewise_C1_differentiable_on_def valid_path_def 
+        by blast
+      then show "continuous_on ({0..1} - s) (\<lambda>x. deriv f (g x))" 
+        using continuous_on_subset by blast
     next
-      have "g t\<in>path_image g" using that DiffD1 image_eqI path_image_def by metis
-      then obtain f' where "(f has_field_derivative f') (at (g t))"
-        using der by auto
-      then show "\<exists>g'. (f has_field_derivative g') (at (g t))" by auto
+      show "vector_derivative g (at t) * deriv f (g t) = vector_derivative (f \<circ> g) (at t)"
+          when "t \<in> {0..1} - s" for t
+        proof (rule vector_derivative_chain_at_general[symmetric])
+          show "g differentiable at t" by (meson C1_differentiable_on_eq g_diff that)
+        next
+          have "g t\<in>path_image g" using that DiffD1 image_eqI path_image_def by metis
+          then obtain f' where "(f has_field_derivative f') (at (g t))"
+            using der by auto
+          then show "\<exists>g'. (f has_field_derivative g') (at (g t))" by auto
+        qed
     qed
-  qed
   ultimately have "f o g C1_differentiable_on {0..1} - s"
     using C1_differentiable_on_eq by blast
-  moreover have "path (f o g)"
-  proof -
-    have "isCont f x" if "x \<in> path_image g" for x
-      proof -
-        obtain f' where "(f has_field_derivative f') (at x)"
-          using der `x\<in>path_image g` by auto
-        thus ?thesis using DERIV_isCont by auto
-      qed
-    then have "continuous_on (path_image g) f" using continuous_at_imp_continuous_on by auto
-    then show ?thesis using path_continuous_image `valid_path g` valid_path_imp_path by auto
-  qed
+  moreover have "path (f o g)" 
+    proof -
+      have "isCont f x" when "x\<in>path_image g" for x 
+        proof -
+          obtain f' where "(f has_field_derivative f') (at x)" 
+            using der[rule_format] `x\<in>path_image g` by auto
+          thus ?thesis using DERIV_isCont by auto
+        qed
+      then have "continuous_on (path_image g) f" using continuous_at_imp_continuous_on by auto
+      then show ?thesis using path_continuous_image `valid_path g` valid_path_imp_path by auto
+    qed
   ultimately show ?thesis unfolding valid_path_def piecewise_C1_differentiable_on_def path_def
     using `finite s` by auto
 qed
@@ -725,7 +729,7 @@
     by (auto simp: valid_path_def piecewise_C1_differentiable_on_def path_def [symmetric])
 qed
 
-lemma valid_path_reversepath: "valid_path(reversepath g) \<longleftrightarrow> valid_path g"
+lemma valid_path_reversepath [simp]: "valid_path(reversepath g) \<longleftrightarrow> valid_path g"
   using valid_path_imp_reverse by force
 
 lemma has_contour_integral_reversepath:
@@ -5732,6 +5736,20 @@
 by (metis (no_types, hide_lams) DERIV_deriv_iff_field_differentiable at_within_open comp_apply
          funpow.simps(2) holomorphic_higher_deriv holomorphic_on_def)
 
+lemma valid_path_compose_holomorphic:
+  assumes "valid_path g" and holo:"f holomorphic_on s" and "open s" "path_image g \<subseteq> s"
+  shows "valid_path (f o g)"
+proof (rule valid_path_compose[OF `valid_path g`])
+  fix x assume "x \<in> path_image g"
+  then show "\<exists>f'. (f has_field_derivative f') (at x)"
+    using holo holomorphic_on_open[OF `open s`] `path_image g \<subseteq> s` by auto 
+next
+  have "deriv f holomorphic_on s"
+    using holomorphic_deriv holo `open s` by auto
+  then show "continuous_on (path_image g) (deriv f)" 
+    using assms(4) holomorphic_on_imp_continuous_on holomorphic_on_subset by auto
+qed
+
 
 subsection\<open> Morera's theorem.\<close>
 

--- a/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy	Mon Mar 07 23:20:11 2016 +0100
+++ b/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy	Wed Mar 09 17:16:08 2016 +0000
@@ -443,7 +443,7 @@
     "f holomorphic_on s \<Longrightarrow> continuous_on s f"
   by (metis field_differentiable_imp_continuous_at continuous_on_eq_continuous_within holomorphic_on_def)
 
-lemma holomorphic_on_subset:
+lemma holomorphic_on_subset [elim]:
     "f holomorphic_on s \<Longrightarrow> t \<subseteq> s \<Longrightarrow> f holomorphic_on t"
   unfolding holomorphic_on_def
   by (metis field_differentiable_within_subset subsetD)

--- a/src/HOL/Multivariate_Analysis/Conformal_Mappings.thy	Mon Mar 07 23:20:11 2016 +0100
+++ b/src/HOL/Multivariate_Analysis/Conformal_Mappings.thy	Wed Mar 09 17:16:08 2016 +0000
@@ -2,6 +2,8 @@
 
 text\<open>By John Harrison et al.  Ported from HOL Light by L C Paulson (2016)\<close>
 
+text\<open>Also Cauchy's residue theorem by Wenda Li (2016)\<close>
+
 theory Conformal_Mappings
 imports "~~/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm"
 
@@ -2130,4 +2132,1336 @@
   qed
 qed
 
+subsection \<open>Cauchy's residue theorem\<close>
+
+text\<open>Wenda Li (2016)\<close>
+
+declare valid_path_imp_path [simp] 
+
+lemma holomorphic_factor_zero_unique: 
+  fixes f::"complex \<Rightarrow> complex" and z::complex and r::real    
+  assumes "r>0"
+    and asm:"\<forall>w\<in>ball z r. f w = (w-z)^n * g w \<and> g w\<noteq>0 \<and> f w = (w - z)^m * h w \<and> h w\<noteq>0"
+    and g_holo:"g holomorphic_on ball z r" and h_holo:"h holomorphic_on ball z r"
+  shows "n=m" 
+proof -
+  have "n>m \<Longrightarrow> False"
+    proof -
+      assume "n>m"
+      have "(h \<longlongrightarrow> 0) (at z within ball z r)" 
+        proof (rule Lim_transform_within[OF _ `r>0`, where f="\<lambda>w. (w - z) ^ (n - m) * g w"]) 
+          have "\<forall>w\<in>ball z r. w\<noteq>z \<longrightarrow> h w = (w-z)^(n-m) * g w" using `n>m` asm
+            by (auto simp add:field_simps power_diff)
+          then show "\<lbrakk>x' \<in> ball z r; 0 < dist x' z;dist x' z < r\<rbrakk> 
+            \<Longrightarrow> (x' - z) ^ (n - m) * g x' = h x'" for x' by auto
+        next
+          def F\<equiv>"at z within ball z r"
+            and f'\<equiv>"\<lambda>x. (x - z) ^ (n-m)"
+          have "f' z=0" using `n>m` unfolding f'_def by auto
+          moreover have "continuous F f'" unfolding f'_def F_def
+            by (intro continuous_intros)
+          ultimately have "(f' \<longlongrightarrow> 0) F" unfolding F_def
+            by (simp add: continuous_within)            
+          moreover have "(g \<longlongrightarrow> g z) F"
+            using holomorphic_on_imp_continuous_on[OF g_holo,unfolded continuous_on_def] `r>0`
+            unfolding F_def by auto
+          ultimately show " ((\<lambda>w. f' w * g w) \<longlongrightarrow> 0) F" using tendsto_mult by fastforce
+        qed
+      moreover have "(h \<longlongrightarrow> h z) (at z within ball z r)" 
+        using holomorphic_on_imp_continuous_on[OF h_holo] 
+        by (auto simp add:continuous_on_def `r>0`) 
+      moreover have "at z within ball z r \<noteq> bot" using `r>0` 
+        by (auto simp add:trivial_limit_within islimpt_ball)
+      ultimately have "h z=0" by (auto intro: tendsto_unique)
+      thus False using asm `r>0` by auto
+    qed
+  moreover have "m>n \<Longrightarrow> False"
+    proof -
+      assume "m>n"
+      have "(g \<longlongrightarrow> 0) (at z within ball z r)" 
+        proof (rule Lim_transform_within[OF _ `r>0`, where f="\<lambda>w. (w - z) ^ (m - n) * h w"]) 
+          have "\<forall>w\<in>ball z r. w\<noteq>z \<longrightarrow> g w = (w-z)^(m-n) * h w" using `m>n` asm
+            by (auto simp add:field_simps power_diff)
+          then show "\<lbrakk>x' \<in> ball z r; 0 < dist x' z;dist x' z < r\<rbrakk> 
+            \<Longrightarrow> (x' - z) ^ (m - n) * h x' = g x'" for x' by auto
+        next
+          def F\<equiv>"at z within ball z r"
+            and f'\<equiv>"\<lambda>x. (x - z) ^ (m-n)"
+          have "f' z=0" using `m>n` unfolding f'_def by auto
+          moreover have "continuous F f'" unfolding f'_def F_def
+            by (intro continuous_intros)
+          ultimately have "(f' \<longlongrightarrow> 0) F" unfolding F_def
+            by (simp add: continuous_within)            
+          moreover have "(h \<longlongrightarrow> h z) F"
+            using holomorphic_on_imp_continuous_on[OF h_holo,unfolded continuous_on_def] `r>0`
+            unfolding F_def by auto
+          ultimately show " ((\<lambda>w. f' w * h w) \<longlongrightarrow> 0) F" using tendsto_mult by fastforce
+        qed
+      moreover have "(g \<longlongrightarrow> g z) (at z within ball z r)" 
+        using holomorphic_on_imp_continuous_on[OF g_holo] 
+        by (auto simp add:continuous_on_def `r>0`) 
+      moreover have "at z within ball z r \<noteq> bot" using `r>0` 
+        by (auto simp add:trivial_limit_within islimpt_ball)
+      ultimately have "g z=0" by (auto intro: tendsto_unique)
+      thus False using asm `r>0` by auto
+    qed
+  ultimately show "n=m" by fastforce
+qed
+
+lemma holomorphic_factor_zero_Ex1:
+  assumes "open s" "connected s" "z \<in> s" and
+        holo:"f holomorphic_on s" 
+        and "f z = 0" and "\<exists>w\<in>s. f w \<noteq> 0"
+  shows "\<exists>!n. \<exists>g r. 0 < n \<and> 0 < r \<and>
+                g holomorphic_on cball z r 
+                \<and> (\<forall>w\<in>cball z r. f w = (w-z)^n * g w \<and> g w\<noteq>0)"
+proof (rule ex_ex1I)
+  obtain g r n where "0 < n" "0 < r" "ball z r \<subseteq> s" and 
+          g:"g holomorphic_on ball z r"
+          "\<And>w. w \<in> ball z r \<Longrightarrow> f w = (w - z) ^ n * g w" 
+          "\<And>w. w \<in> ball z r \<Longrightarrow> g w \<noteq> 0"
+    using holomorphic_factor_zero_nonconstant[OF holo `open s` `connected s` `z\<in>s` `f z=0`]
+    by (metis assms(3) assms(5) assms(6))
+  def r'\<equiv>"r/2"
+  have "cball z r' \<subseteq> ball z r" unfolding r'_def by (simp add: \<open>0 < r\<close> cball_subset_ball_iff)
+  hence "cball z r' \<subseteq> s" "g holomorphic_on cball z r'" 
+      "(\<forall>w\<in>cball z r'. f w = (w - z) ^ n * g w \<and> g w \<noteq> 0)"
+    using g `ball z r \<subseteq> s` by auto
+  moreover have "r'>0" unfolding r'_def using `0<r` by auto
+  ultimately show "\<exists>n g r. 0 < n \<and> 0 < r  \<and> g holomorphic_on cball z r 
+          \<and> (\<forall>w\<in>cball z r. f w = (w - z) ^ n * g w \<and> g w \<noteq> 0)"
+    apply (intro exI[of _ n] exI[of _ g] exI[of _ r'])
+    by (simp add:`0 < n`)
+next
+  fix m n 
+  def fac\<equiv>"\<lambda>n g r. \<forall>w\<in>cball z r. f w = (w - z) ^ n * g w \<and> g w \<noteq> 0"  
+  assume n_asm:"\<exists>g r1. 0 < n \<and> 0 < r1 \<and> g holomorphic_on cball z r1 \<and> fac n g r1"
+     and m_asm:"\<exists>h r2. 0 < m \<and> 0 < r2  \<and> h holomorphic_on cball z r2 \<and> fac m h r2"
+  obtain g r1 where "0 < n" "0 < r1" and g_holo: "g holomorphic_on cball z r1" 
+    and "fac n g r1" using n_asm by auto
+  obtain h r2 where "0 < m" "0 < r2" and h_holo: "h holomorphic_on cball z r2"  
+    and "fac m h r2" using m_asm by auto
+  def r\<equiv>"min r1 r2"
+  have "r>0" using `r1>0` `r2>0` unfolding r_def by auto
+  moreover have "\<forall>w\<in>ball z r. f w = (w-z)^n * g w \<and> g w\<noteq>0 \<and> f w = (w - z)^m * h w \<and> h w\<noteq>0" 
+    using \<open>fac m h r2\<close> \<open>fac n g r1\<close>   unfolding fac_def r_def
+    by fastforce
+  ultimately show "m=n" using g_holo h_holo 
+    apply (elim holomorphic_factor_zero_unique[of r z f n g m h,symmetric,rotated])
+    by (auto simp add:r_def)
+qed
+
+lemma finite_ball_avoid:
+  assumes "open s" "finite pts"
+  shows "\<forall>p\<in>s. \<exists>e>0. \<forall>w\<in>ball p e. w\<in>s \<and> (w\<noteq>p \<longrightarrow> w\<notin>pts)"
+proof
+  fix p assume "p\<in>s"
+  then obtain e1 where "0 < e1" and e1_b:"ball p e1 \<subseteq> s" 
+    using open_contains_ball_eq[OF `open s`] by auto
+  obtain e2 where "0<e2" and "\<forall>x\<in>pts. x \<noteq> p \<longrightarrow> e2 \<le> dist p x" 
+    using finite_set_avoid[OF `finite pts`,of p] by auto
+  hence "\<forall>w\<in>ball p (min e1 e2). w\<in>s \<and> (w\<noteq>p \<longrightarrow> w\<notin>pts)" using e1_b by auto
+  thus "\<exists>e>0. \<forall>w\<in>ball p e. w \<in> s \<and> (w \<noteq> p \<longrightarrow> w \<notin> pts)" using `e2>0` `e1>0` 
+    apply (rule_tac x="min e1 e2" in exI)
+    by auto
+qed
+
+lemma finite_cball_avoid:
+  fixes s :: "'a :: euclidean_space set"
+  assumes "open s" "finite pts"
+  shows "\<forall>p\<in>s. \<exists>e>0. \<forall>w\<in>cball p e. w\<in>s \<and> (w\<noteq>p \<longrightarrow> w\<notin>pts)"
+proof 
+  fix p assume "p\<in>s"
+  then obtain e1 where "e1>0" and e1: "\<forall>w\<in>ball p e1. w\<in>s \<and> (w\<noteq>p \<longrightarrow> w\<notin>pts)" 
+    using finite_ball_avoid[OF assms] by auto
+  def e2\<equiv>"e1/2"
+  have "e2>0" and "e2<e1" unfolding e2_def using `e1>0` by auto
+  then have "cball p e2 \<subseteq> ball p e1" by (subst cball_subset_ball_iff,auto)
+  then show "\<exists>e>0. \<forall>w\<in>cball p e. w \<in> s \<and> (w \<noteq> p \<longrightarrow> w \<notin> pts)" using `e2>0` e1 by auto
+qed
+
+lemma get_integrable_path:
+  assumes "open s" "connected (s-pts)" "finite pts" "f holomorphic_on (s-pts) " "a\<in>s-pts" "b\<in>s-pts"
+  obtains g where "valid_path g" "pathstart g = a" "pathfinish g = b" 
+    "path_image g \<subseteq> s-pts" "f contour_integrable_on g" using assms
+proof (induct arbitrary:s thesis a rule:finite_induct[OF `finite pts`]) print_cases
+  case 1
+  obtain g where "valid_path g" "path_image g \<subseteq> s" "pathstart g = a" "pathfinish g = b"
+    using connected_open_polynomial_connected[OF `open s`,of a b ] `connected (s - {})`
+      valid_path_polynomial_function "1.prems"(6) "1.prems"(7) by auto
+  moreover have "f contour_integrable_on g" 
+    using contour_integrable_holomorphic_simple[OF _ `open s` `valid_path g` `path_image g \<subseteq> s`,of f]
+      `f holomorphic_on s - {}`
+    by auto
+  ultimately show ?case using "1"(1)[of g] by auto
+next
+  case idt:(2 p pts) 
+  obtain e where "e>0" and e:"\<forall>w\<in>ball a e. w \<in> s \<and> (w \<noteq> a \<longrightarrow> w \<notin> insert p pts)"
+    using finite_ball_avoid[OF `open s` `finite (insert p pts)`,rule_format,of a]  
+      `a \<in> s - insert p pts`
+    by auto
+  def a'\<equiv>"a+e/2"
+  have "a'\<in>s-{p} -pts"  using e[rule_format,of "a+e/2"] `e>0`  
+    by (auto simp add:dist_complex_def a'_def)
+  then obtain g' where g'[simp]:"valid_path g'" "pathstart g' = a'" "pathfinish g' = b" 
+    "path_image g' \<subseteq> s - {p} - pts" "f contour_integrable_on g'"    
+    using idt.hyps(3)[of a' "s-{p}"] idt.prems idt.hyps(1) 
+    by (metis Diff_insert2 open_delete)
+  def g\<equiv>"linepath a a' +++ g'"
+  have "valid_path g" unfolding g_def by (auto intro: valid_path_join)
+  moreover have "pathstart g = a" and  "pathfinish g = b" unfolding g_def by auto 
+  moreover have "path_image g \<subseteq> s - insert p pts" unfolding g_def 
+    proof (rule subset_path_image_join)
+      have "closed_segment a a' \<subseteq> ball a e" using `e>0` 
+        by (auto dest!:segment_bound1 simp:a'_def dist_complex_def norm_minus_commute)
+      then show "path_image (linepath a a') \<subseteq> s - insert p pts" using e idt(9)
+        by auto
+    next
+      show "path_image g' \<subseteq> s - insert p pts" using g'(4) by blast
+    qed
+  moreover have "f contour_integrable_on g"  
+    proof -
+      have "closed_segment a a' \<subseteq> ball a e" using `e>0` 
+        by (auto dest!:segment_bound1 simp:a'_def dist_complex_def norm_minus_commute)
+      then have "continuous_on (closed_segment a a') f" 
+        using e idt.prems(6) holomorphic_on_imp_continuous_on[OF idt.prems(5)]
+        apply (elim continuous_on_subset)
+        by auto
+      then have "f contour_integrable_on linepath a a'" 
+        using contour_integrable_continuous_linepath by auto
+      then show ?thesis unfolding g_def
+        apply (rule contour_integrable_joinI)
+        by (auto simp add: `e>0`)
+    qed
+  ultimately show ?case using idt.prems(1)[of g] by auto
+qed
+
+lemma Cauchy_theorem_aux:
+  assumes "open s" "connected (s-pts)" "finite pts" "pts \<subseteq> s" "f holomorphic_on s-pts"
+          "valid_path g" "pathfinish g = pathstart g" "path_image g \<subseteq> s-pts" 
+          "\<forall>z. (z \<notin> s) \<longrightarrow> winding_number g z  = 0" 
+          "\<forall>p\<in>s. h p>0 \<and> (\<forall>w\<in>cball p (h p). w\<in>s \<and> (w\<noteq>p \<longrightarrow> w \<notin> pts))"
+  shows "contour_integral g f = (\<Sum>p\<in>pts. winding_number g p * contour_integral (circlepath p (h p)) f)"
+    using assms
+proof (induct arbitrary:s g rule:finite_induct[OF `finite pts`]) 
+  case 1
+  then show ?case by (simp add: Cauchy_theorem_global contour_integral_unique)
+next
+  case (2 p pts) 
+  note fin[simp] = `finite (insert p pts)`
+    and connected = `connected (s - insert p pts)`
+    and valid[simp] = `valid_path g`
+    and g_loop[simp] = `pathfinish g = pathstart g`
+    and holo[simp]= `f holomorphic_on s - insert p pts`
+    and path_img = `path_image g \<subseteq> s - insert p pts`
+    and winding = `\<forall>z. z \<notin> s \<longrightarrow> winding_number g z = 0`
+    and h = `\<forall>pa\<in>s. 0 < h pa \<and> (\<forall>w\<in>cball pa (h pa). w \<in> s \<and> (w \<noteq> pa \<longrightarrow> w \<notin> insert p pts))`
+  have "h p>0" and "p\<in>s"
+    and h_p: "\<forall>w\<in>cball p (h p). w \<in> s \<and> (w \<noteq> p \<longrightarrow> w \<notin> insert p pts)"
+    using h `insert p pts \<subseteq> s` by auto
+  obtain pg where pg[simp]: "valid_path pg" "pathstart pg = pathstart g" "pathfinish pg=p+h p" 
+      "path_image pg \<subseteq> s-insert p pts" "f contour_integrable_on pg" 
+    proof -
+      have "p + h p\<in>cball p (h p)" using h[rule_format,of p] 
+        by (simp add: \<open>p \<in> s\<close> dist_norm)
+      then have "p + h p \<in> s - insert p pts" using h[rule_format,of p] `insert p pts \<subseteq> s` 
+        by fastforce
+      moreover have "pathstart g \<in> s - insert p pts " using path_img by auto
+      ultimately show ?thesis
+        using get_integrable_path[OF `open s` connected fin holo,of "pathstart g" "p+h p"] that
+        by blast
+    qed
+  obtain n::int where "n=winding_number g p"
+    using integer_winding_number[OF _ g_loop,of p] valid path_img 
+    by (metis DiffD2 Ints_cases insertI1 subset_eq valid_path_imp_path)
+  def p_circ\<equiv>"circlepath p (h p)" and p_circ_pt\<equiv>"linepath (p+h p) (p+h p)"
+  def n_circ\<equiv>"\<lambda>n. (op +++ p_circ ^^ n) p_circ_pt"
+  def cp\<equiv>"if n\<ge>0 then reversepath (n_circ (nat n)) else n_circ (nat (- n))"
+  have n_circ:"valid_path (n_circ k)"    
+      "winding_number (n_circ k) p = k"
+      "pathstart (n_circ k) = p + h p" "pathfinish (n_circ k) = p + h p" 
+      "path_image (n_circ k) =  (if k=0 then {p + h p} else sphere p (h p))"
+      "p \<notin> path_image (n_circ k)"
+      "\<And>p'. p'\<notin>s - pts \<Longrightarrow> winding_number (n_circ k) p'=0 \<and> p'\<notin>path_image (n_circ k)"
+      "f contour_integrable_on (n_circ k)"
+      "contour_integral (n_circ k) f = k *  contour_integral p_circ f"
+      for k 
+    proof (induct k) 
+      case 0 
+      show "valid_path (n_circ 0)" 
+        and "path_image (n_circ 0) =  (if 0=0 then {p + h p} else sphere p (h p))"
+        and "winding_number (n_circ 0) p = of_nat 0" 
+        and "pathstart (n_circ 0) = p + h p"
+        and "pathfinish (n_circ 0) = p + h p"
+        and "p \<notin> path_image (n_circ 0)"
+        unfolding n_circ_def p_circ_pt_def using `h p > 0`
+        by (auto simp add: dist_norm)
+      show "winding_number (n_circ 0) p'=0 \<and> p'\<notin>path_image (n_circ 0)" when "p'\<notin>s- pts" for p' 
+        unfolding n_circ_def p_circ_pt_def
+        apply (auto intro!:winding_number_trivial)
+        by (metis Diff_iff pathfinish_in_path_image pg(3) pg(4) subsetCE subset_insertI that)+
+      show "f contour_integrable_on (n_circ 0)"
+        unfolding n_circ_def p_circ_pt_def
+        by (auto intro!:contour_integrable_continuous_linepath simp add:continuous_on_sing)
+      show "contour_integral (n_circ 0) f = of_nat 0  *  contour_integral p_circ f"
+        unfolding n_circ_def p_circ_pt_def by auto
+    next
+      case (Suc k)
+      have n_Suc:"n_circ (Suc k) = p_circ +++ n_circ k" unfolding n_circ_def by auto
+      have pcirc:"p \<notin> path_image p_circ" "valid_path p_circ" "pathfinish p_circ = pathstart (n_circ k)" 
+        using Suc(3) unfolding p_circ_def using `h p > 0` by (auto simp add: p_circ_def)
+      have pcirc_image:"path_image p_circ \<subseteq> s - insert p pts" 
+        proof -
+          have "path_image p_circ \<subseteq> cball p (h p)" using \<open>0 < h p\<close> p_circ_def by auto
+          then show ?thesis using h_p pcirc(1) by auto
+        qed
+      have pcirc_integrable:"f contour_integrable_on p_circ"
+        by (auto simp add:p_circ_def intro!: pcirc_image[unfolded p_circ_def] 
+          contour_integrable_continuous_circlepath holomorphic_on_imp_continuous_on 
+          holomorphic_on_subset[OF holo])
+      show "valid_path (n_circ (Suc k))"   
+        using valid_path_join[OF pcirc(2) Suc(1) pcirc(3)] unfolding n_circ_def by auto
+      show "path_image (n_circ (Suc k)) 
+          = (if Suc k = 0 then {p + complex_of_real (h p)} else sphere p (h p))" 
+        proof -
+          have "path_image p_circ = sphere p (h p)" 
+            unfolding p_circ_def using \<open>0 < h p\<close> by auto
+          then show ?thesis unfolding n_Suc  using Suc.hyps(5)  `h p>0`
+            by (auto simp add:  path_image_join[OF pcirc(3)]  dist_norm)
+        qed
+      then show "p \<notin> path_image (n_circ (Suc k))" using `h p>0` by auto
+      show "winding_number (n_circ (Suc k)) p = of_nat (Suc k)" 
+        proof -
+          have "winding_number p_circ p = 1" 
+            by (simp add: `h p > 0` p_circ_def winding_number_circlepath_centre)
+          moreover have "p \<notin> path_image (n_circ k)" using Suc(5) `h p>0` by auto
+          then have "winding_number (p_circ +++ n_circ k) p 
+              = winding_number p_circ p + winding_number (n_circ k) p"
+            using  valid_path_imp_path Suc.hyps(1) Suc.hyps(2) pcirc 
+            apply (intro winding_number_join)
+            by auto
+          ultimately show ?thesis using Suc(2) unfolding n_circ_def 
+            by auto
+        qed 
+      show "pathstart (n_circ (Suc k)) = p + h p"
+        by (simp add: n_circ_def p_circ_def)
+      show "pathfinish (n_circ (Suc k)) = p + h p"
+        using Suc(4) unfolding n_circ_def by auto      
+      show "winding_number (n_circ (Suc k)) p'=0 \<and>  p'\<notin>path_image (n_circ (Suc k))" when "p'\<notin>s-pts" for p'
+        proof -
+          have " p' \<notin> path_image p_circ" using \<open>p \<in> s\<close> h p_circ_def that using pcirc_image by blast
+          moreover have "p' \<notin> path_image (n_circ k)" 
+            using Suc.hyps(7) that by blast
+          moreover have "winding_number p_circ p' = 0" 
+            proof -
+              have "path_image p_circ \<subseteq> cball p (h p)"
+                using h unfolding p_circ_def using \<open>p \<in> s\<close> by fastforce
+              moreover have "p'\<notin>cball p (h p)" using \<open>p \<in> s\<close> h that "2.hyps"(2) by fastforce
+              ultimately show ?thesis unfolding p_circ_def
+                apply (intro winding_number_zero_outside)
+                by auto
+            qed
+          ultimately show ?thesis
+            unfolding n_Suc
+            apply (subst winding_number_join)
+            by (auto simp: pcirc Suc that not_in_path_image_join Suc.hyps(7)[OF that])
+        qed
+      show "f contour_integrable_on (n_circ (Suc k))"
+        unfolding n_Suc
+        by (rule contour_integrable_joinI[OF pcirc_integrable Suc(8) pcirc(2) Suc(1)])
+      show "contour_integral (n_circ (Suc k)) f = (Suc k) *  contour_integral p_circ f"
+        unfolding n_Suc
+        by (auto simp add:contour_integral_join[OF pcirc_integrable Suc(8) pcirc(2) Suc(1)] 
+          Suc(9) algebra_simps)
+    qed
+  have cp[simp]:"pathstart cp = p + h p"  "pathfinish cp = p + h p"
+         "valid_path cp" "path_image cp \<subseteq> s - insert p pts" 
+         "winding_number cp p = - n"
+         "\<And>p'. p'\<notin>s - pts \<Longrightarrow> winding_number cp p'=0 \<and> p' \<notin> path_image cp"
+         "f contour_integrable_on cp"
+         "contour_integral cp f = - n * contour_integral p_circ f"
+    proof - 
+      show "pathstart cp = p + h p" and "pathfinish cp = p + h p" and "valid_path cp"
+        using n_circ unfolding cp_def by auto
+    next
+      have "sphere p (h p) \<subseteq>  s - insert p pts" 
+        using h[rule_format,of p] `insert p pts \<subseteq> s` by force
+      moreover  have "p + complex_of_real (h p) \<in> s - insert p pts" 
+        using pg(3) pg(4) by (metis pathfinish_in_path_image subsetCE)
+      ultimately show "path_image cp \<subseteq>  s - insert p pts" unfolding cp_def
+        using n_circ(5)  by auto
+    next
+      show "winding_number cp p = - n" 
+        unfolding cp_def using winding_number_reversepath n_circ `h p>0` by auto
+    next
+      show "winding_number cp p'=0 \<and> p' \<notin> path_image cp" when "p'\<notin>s - pts" for p'
+        unfolding cp_def
+        apply (auto)
+        apply (subst winding_number_reversepath)
+        by (auto simp add: n_circ(7)[OF that] n_circ(1))
+    next
+      show "f contour_integrable_on cp" unfolding cp_def
+        using contour_integrable_reversepath_eq n_circ(1,8) by auto
+    next
+      show "contour_integral cp f = - n * contour_integral p_circ f"
+        unfolding cp_def using contour_integral_reversepath[OF n_circ(1)] n_circ(9)
+        by auto
+    qed
+  def g'\<equiv>"g +++ pg +++ cp +++ (reversepath pg)"
+  have "contour_integral g' f = (\<Sum>p\<in>pts. winding_number g' p * contour_integral (circlepath p (h p)) f)"
+    proof (rule "2.hyps"(3)[of "s-{p}" "g'",OF _ _ `finite pts` ]) 
+      show "connected (s - {p} - pts)" using connected by (metis Diff_insert2)
+      show "open (s - {p})" using `open s` by auto
+      show " pts \<subseteq> s - {p}" using `insert p pts \<subseteq> s` ` p \<notin> pts`  by blast 
+      show "f holomorphic_on s - {p} - pts" using holo `p \<notin> pts` by (metis Diff_insert2)
+      show "valid_path g'" 
+        unfolding g'_def cp_def using n_circ valid pg g_loop
+        by (auto intro!:valid_path_join )
+      show "pathfinish g' = pathstart g'"
+        unfolding g'_def cp_def using pg(2) by simp
+      show "path_image g' \<subseteq> s - {p} - pts" 
+        proof -
+          def s'\<equiv>"s - {p} - pts"
+          have s':"s' = s-insert p pts " unfolding s'_def by auto
+          then show ?thesis using path_img pg(4) cp(4)      
+            unfolding g'_def 
+            apply (fold s'_def s')           
+            apply (intro subset_path_image_join)
+            by auto
+        qed
+      note path_join_imp[simp]
+      show "\<forall>z. z \<notin> s - {p} \<longrightarrow> winding_number g' z = 0"
+        proof clarify
+          fix z assume z:"z\<notin>s - {p}"
+          have "winding_number (g +++ pg +++ cp +++ reversepath pg) z = winding_number g z 
+              + winding_number (pg +++ cp +++ (reversepath pg)) z"
+            proof (rule winding_number_join)
+              show "path g" using `valid_path g` by simp
+              show "z \<notin> path_image g" using z path_img by auto
+              show "path (pg +++ cp +++ reversepath pg)" using pg(3) cp by auto
+            next
+              have "path_image (pg +++ cp +++ reversepath pg) \<subseteq> s - insert p pts"
+                using pg(4) cp(4) by (auto simp:subset_path_image_join)
+              then show "z \<notin> path_image (pg +++ cp +++ reversepath pg)" using z by auto
+            next
+              show "pathfinish g = pathstart (pg +++ cp +++ reversepath pg)" using g_loop by auto
+            qed
+          also have "... = winding_number g z + (winding_number pg z 
+              + winding_number (cp +++ (reversepath pg)) z)"
+            proof (subst add_left_cancel,rule winding_number_join)
+              show "path pg" and "path (cp +++ reversepath pg)" 
+                and "pathfinish pg = pathstart (cp +++ reversepath pg)" by auto
+              show "z \<notin> path_image pg" using pg(4) z by blast
+              show "z \<notin> path_image (cp +++ reversepath pg)" using z 
+                by (metis Diff_iff \<open>z \<notin> path_image pg\<close> contra_subsetD cp(4) insertI1 
+                  not_in_path_image_join path_image_reversepath singletonD)
+            qed
+          also have "... = winding_number g z + (winding_number pg z 
+              + (winding_number cp z + winding_number (reversepath pg) z))" 
+            apply (auto intro!:winding_number_join )
+            apply (metis Diff_iff contra_subsetD cp(4) insertI1 singletonD z)
+            by (metis Diff_insert2 Diff_subset contra_subsetD pg(4) z)            
+          also have "... = winding_number g z + winding_number cp z"
+            apply (subst winding_number_reversepath)
+            apply auto
+            by (metis Diff_iff contra_subsetD insertI1 pg(4) singletonD z)
+          finally have "winding_number g' z = winding_number g z + winding_number cp z" 
+            unfolding g'_def .
+          moreover have "winding_number g z + winding_number cp z = 0" 
+            using winding z `n=winding_number g p` by auto
+          ultimately show "winding_number g' z = 0" unfolding g'_def by auto
+        qed
+      show "\<forall>pa\<in>s - {p}. 0 < h pa \<and> (\<forall>w\<in>cball pa (h pa). w \<in> s - {p} \<and> (w \<noteq> pa \<longrightarrow> w \<notin> pts))"
+        using h by fastforce
+    qed
+  moreover have "contour_integral g' f = contour_integral g f 
+      - winding_number g p * contour_integral p_circ f" 
+    proof -
+      have "contour_integral g' f =  contour_integral g f 
+        + contour_integral (pg +++ cp +++ reversepath pg) f"
+        unfolding g'_def
+        apply (subst Cauchy_Integral_Thm.contour_integral_join) 
+        by (auto simp add:open_Diff[OF `open s`,OF finite_imp_closed[OF fin]]
+          intro!: contour_integrable_holomorphic_simple[OF holo _ _ path_img]  
+          contour_integrable_reversepath)
+      also have "... = contour_integral g f + contour_integral pg f 
+          + contour_integral (cp +++ reversepath pg) f"
+        apply (subst Cauchy_Integral_Thm.contour_integral_join)
+        by (auto simp add:contour_integrable_reversepath)
+      also have "... = contour_integral g f + contour_integral pg f 
+          + contour_integral cp f + contour_integral (reversepath pg) f"
+        apply (subst Cauchy_Integral_Thm.contour_integral_join)
+        by (auto simp add:contour_integrable_reversepath)
+      also have "... = contour_integral g f + contour_integral cp f"
+        using contour_integral_reversepath
+        by (auto simp add:contour_integrable_reversepath)
+      also have "... = contour_integral g f - winding_number g p * contour_integral p_circ f"
+        using `n=winding_number g p` by auto
+      finally show ?thesis .
+    qed
+  moreover have "winding_number g' p' = winding_number g p'" when "p'\<in>pts" for p' 
+    proof -
+      have [simp]: "p' \<notin> path_image g" "p' \<notin> path_image pg" "p'\<notin>path_image cp" 
+        using "2.prems"(8) that 
+        apply blast
+        apply (metis Diff_iff Diff_insert2 contra_subsetD pg(4) that)
+        by (meson DiffD2 cp(4) set_rev_mp subset_insertI that)
+      have "winding_number g' p' = winding_number g p' 
+          + winding_number (pg +++ cp +++ reversepath pg) p'" unfolding g'_def 
+        apply (subst winding_number_join)
+        apply simp_all
+        apply (intro not_in_path_image_join)
+        by auto
+      also have "... = winding_number g p' + winding_number pg p'
+          + winding_number (cp +++ reversepath pg) p'" 
+        apply (subst winding_number_join)
+        apply simp_all
+        apply (intro not_in_path_image_join)
+        by auto
+      also have "... = winding_number g p' + winding_number pg p'+ winding_number cp p'
+          + winding_number (reversepath pg) p'"
+        apply (subst winding_number_join)
+        by simp_all
+      also have "... = winding_number g p' + winding_number cp p'"
+        apply (subst winding_number_reversepath)
+        by auto
+      also have "... = winding_number g p'" using that by auto
+      finally show ?thesis .
+    qed
+  ultimately show ?case unfolding p_circ_def 
+    apply (subst (asm) setsum.cong[OF refl, 
+        of pts _ "\<lambda>p. winding_number g p * contour_integral (circlepath p (h p)) f"])
+    by (auto simp add:setsum.insert[OF `finite pts` `p\<notin>pts`] algebra_simps)         
+qed  
+
+
+lemma Cauchy_theorem_singularities:
+  assumes "open s" "connected (s-pts)" "finite pts" and 
+          holo:"f holomorphic_on s-pts" and
+          "valid_path g" and 
+          loop:"pathfinish g = pathstart g" and
+          "path_image g \<subseteq> s-pts" and
+          homo:"\<forall>z. (z \<notin> s) \<longrightarrow> winding_number g z  = 0" and
+          avoid:"\<forall>p\<in>s. h p>0 \<and> (\<forall>w\<in>cball p (h p). w\<in>s \<and> (w\<noteq>p \<longrightarrow> w \<notin> pts))"
+  shows "contour_integral g f = (\<Sum>p\<in>pts. winding_number g p * contour_integral (circlepath p (h p)) f)"
+    (is "?L=?R")
+proof -
+  def circ\<equiv>"\<lambda>p. winding_number g p * contour_integral (circlepath p (h p)) f"
+  def pts1\<equiv>"pts \<inter> s" 
+  def pts2\<equiv>"pts - pts1"
+  have "pts=pts1 \<union> pts2" "pts1 \<inter> pts2 = {}" "pts2 \<inter> s={}" "pts1\<subseteq>s" 
+    unfolding pts1_def pts2_def by auto
+  have "contour_integral g f =  (\<Sum>p\<in>pts1. circ p)" unfolding circ_def
+    proof (rule Cauchy_theorem_aux[OF `open s` _ _ `pts1\<subseteq>s` _ `valid_path g` loop _ homo])
+      show "connected (s - pts1)" by (metis Diff_Int2 Int_absorb assms(2) pts1_def)
+      show "finite pts1" using \<open>pts = pts1 \<union> pts2\<close> assms(3) by auto
+      show "f holomorphic_on s - pts1" by (metis Diff_Int2 Int_absorb holo pts1_def)
+      show "path_image g \<subseteq> s - pts1" using assms(7) pts1_def by auto 
+      show "\<forall>p\<in>s. 0 < h p \<and> (\<forall>w\<in>cball p (h p). w \<in> s \<and> (w \<noteq> p \<longrightarrow> w \<notin> pts1))"
+        by (simp add: avoid pts1_def)
+    qed
+  moreover have "setsum circ pts2=0"
+    proof -
+      have "winding_number g p=0" when "p\<in>pts2" for p 
+        using  `pts2 \<inter> s={}` that homo[rule_format,of p] by auto
+      thus ?thesis unfolding circ_def
+        apply (intro setsum.neutral)
+        by auto
+    qed
+  moreover have "?R=setsum circ pts1 + setsum circ pts2"
+    unfolding circ_def 
+    using setsum.union_disjoint[OF _ _ `pts1 \<inter> pts2 = {}`] `finite pts` `pts=pts1 \<union> pts2`
+    by blast
+  ultimately show ?thesis
+    apply (fold circ_def)
+    by auto
+qed
+
+
+
+
+(*order of the zero of f at z*)
+definition zorder::"(complex \<Rightarrow> complex) \<Rightarrow> complex \<Rightarrow> nat" where
+  "zorder f z = (THE n. n>0 \<and> (\<exists>h r. r>0 \<and> h holomorphic_on cball z r 
+                    \<and> (\<forall>w\<in>cball z r. f w =  h w * (w-z)^n \<and> h w \<noteq>0)))"
+
+definition zer_poly::"[complex \<Rightarrow> complex,complex]\<Rightarrow>complex \<Rightarrow> complex" where
+  "zer_poly f z = (SOME h. \<exists>r . r>0 \<and> h holomorphic_on cball z r 
+                    \<and> (\<forall>w\<in>cball z r. f w =  h w * (w-z)^(zorder f z) \<and> h w \<noteq>0))"
+
+(*order of the pole of f at z*)
+definition porder::"(complex \<Rightarrow> complex) \<Rightarrow> complex \<Rightarrow> nat" where
+  "porder f z = zorder (inverse o f) z"
+
+definition pol_poly::"[complex \<Rightarrow> complex,complex]\<Rightarrow>complex \<Rightarrow> complex" where
+  "pol_poly f z = inverse o zer_poly (inverse o f) z"
+
+definition residue::"(complex \<Rightarrow> complex) \<Rightarrow> complex \<Rightarrow> complex" where
+  "residue f z = (let n=porder f z;h=pol_poly f z in (deriv ^^ (n - 1)) h z / fact (n-1))"
+
+definition is_pole:: "(complex \<Rightarrow> complex) \<Rightarrow> complex \<Rightarrow>bool" where
+  "is_pole f p \<equiv> isCont (inverse o f) p \<and> f p = 0"
+
+
+lemma zorder_exist:  
+  fixes f::"complex \<Rightarrow> complex" and z::complex
+  defines "n\<equiv>zorder f z" and "h\<equiv>zer_poly f z"
+  assumes  "open s" "connected s" "z\<in>s" 
+    and holo: "f holomorphic_on s"
+    and  "f z=0" "\<exists>w\<in>s. f w\<noteq>0"
+  shows "\<exists>r. n>0 \<and> r>0 \<and> cball z r \<subseteq> s \<and> h holomorphic_on cball z r 
+    \<and> (\<forall>w\<in>cball z r. f w  = h w * (w-z)^n \<and> h w \<noteq>0) "
+proof -
+  def P\<equiv>"\<lambda>h r n. r>0 \<and> h holomorphic_on cball z r 
+    \<and> (\<forall>w\<in>cball z r. ( f w  = h w * (w-z)^n) \<and> h w \<noteq>0)"
+  have "(\<exists>!n. n>0 \<and> (\<exists> h r. P h r n))"
+    proof -
+      have "\<exists>!n. \<exists>h r. n>0 \<and> P h r n"
+        using holomorphic_factor_zero_Ex1[OF `open s` `connected s` `z\<in>s` holo `f z=0` 
+          `\<exists>w\<in>s. f w\<noteq>0`] unfolding P_def
+        apply (subst mult.commute)
+        by auto
+      thus ?thesis by auto
+    qed
+  moreover have n:"n=(THE n. n>0 \<and> (\<exists>h r. P h r n))"
+    unfolding n_def zorder_def P_def by simp
+  ultimately have "n>0 \<and> (\<exists>h r. P h r n)"  
+    apply (drule_tac theI')
+    by simp
+  then have "n>0" and "\<exists>h r. P h r n" by auto
+  moreover have "h=(SOME h. \<exists>r. P h r n)"
+    unfolding h_def P_def zer_poly_def[of f z,folded n_def P_def] by simp
+  ultimately have "\<exists>r. P h r n" 
+    apply (drule_tac someI_ex)
+    by simp
+  then obtain r1 where "P h r1 n" by auto
+  obtain r2 where "r2>0" "cball z r2 \<subseteq> s" 
+    using assms(3) assms(5) open_contains_cball_eq by blast
+  def r3\<equiv>"min r1 r2"
+  have "P h r3 n" using `P h r1 n` `r2>0` unfolding P_def r3_def
+    by auto
+  moreover have "cball z r3 \<subseteq> s" using `cball z r2 \<subseteq> s` unfolding r3_def by auto
+  ultimately show ?thesis using `n>0` unfolding P_def by auto
+qed    
+
+lemma porder_exist:  
+  fixes f::"complex \<Rightarrow> complex" and z::complex
+  defines "n\<equiv>porder f z" and "h\<equiv>pol_poly f z"
+  assumes  "open s" "connected s" "z\<in>s" 
+    and holo:"(inverse o f) holomorphic_on s"
+    and  "f z=0" "\<exists>w\<in>s. f w\<noteq>0"
+  shows "\<exists>r. n>0 \<and> r>0 \<and> cball z r \<subseteq> s \<and> h holomorphic_on cball z r 
+    \<and> (\<forall>w\<in>cball z r. f w  = h w / (w-z)^n \<and> h w \<noteq>0)"
+proof -
+  def zo\<equiv>"zorder (inverse \<circ> f) z" and zp\<equiv>"zer_poly (inverse \<circ> f) z"
+  obtain r where "0 < zo" "0 < r" "cball z r \<subseteq> s" and zp_holo: "zp holomorphic_on cball z r" and
+      zp_fac: "\<forall>w\<in>cball z r. (inverse \<circ> f) w = zp w * (w - z) ^ zo \<and> zp w \<noteq> 0"
+    using zorder_exist[OF `open s` `connected s` `z\<in>s` holo,folded zo_def zp_def] 
+      `f z=0` `\<exists>w\<in>s. f w\<noteq>0`
+    by auto
+  have n:"n=zo" and h:"h=inverse o zp" 
+    unfolding n_def zo_def porder_def h_def zp_def pol_poly_def by simp_all
+  have "h holomorphic_on cball z r"
+    using zp_holo zp_fac holomorphic_on_inverse  unfolding h comp_def by blast
+  moreover have "\<forall>w\<in>cball z r. f w  = h w / (w-z)^n \<and> h w \<noteq>0"
+    using zp_fac unfolding h n comp_def
+    by (metis divide_inverse_commute field_class.field_inverse_zero inverse_inverse_eq 
+      inverse_mult_distrib mult.commute)
+  moreover have "0 < n" unfolding n using `zo>0` by simp
+  ultimately show ?thesis using `0 < r` `cball z r \<subseteq> s` by auto
+qed
+
+lemma base_residue:  
+  fixes f::"complex \<Rightarrow> complex" and z::complex
+  assumes  "open s" "connected s" "z\<in>s" 
+    and holo: "(inverse o f) holomorphic_on s"
+    and "f z=0" 
+    and non_c:"\<exists>w\<in>s. f w\<noteq>0"
+  shows "\<exists>r>0. cball z r \<subseteq> s 
+    \<and> (f has_contour_integral complex_of_real (2 * pi) * \<i> * residue f z) (circlepath z r)"
+proof -
+  def n\<equiv>"porder f z" and h\<equiv>"pol_poly f z"
+  obtain r where "n>0" "0 < r" and
+      r_b:"cball z r \<subseteq> s" and
+      h_holo:"h holomorphic_on cball z r" 
+      and h:"(\<forall>w\<in>cball z r. f w = h w / (w - z) ^ n \<and> h w \<noteq> 0)"
+    using porder_exist[OF `open s` `connected s` `z\<in>s` holo `f z=0` non_c]
+    unfolding n_def h_def by auto
+  def c\<equiv>"complex_of_real (2 * pi) * \<i>"
+  have "residue f z =  (deriv ^^ (n - 1)) h z / fact (n-1)"
+    unfolding residue_def 
+    apply (fold n_def h_def)
+    by simp
+  then have "((\<lambda>u. h u / (u - z) ^ n) has_contour_integral c * residue f z)
+          (circlepath z r)"
+    using Cauchy_has_contour_integral_higher_derivative_circlepath[of z r h z "n -1"
+        ,unfolded Suc_diff_1[OF `n>0`],folded c_def] h_holo r_b
+    by (auto simp add:`r>0` holomorphic_on_imp_continuous_on holomorphic_on_subset)
+  then have "(f has_contour_integral c * residue f z) (circlepath z r)"
+    proof (elim has_contour_integral_eq)
+      fix x assume "x \<in> path_image (circlepath z r)" 
+      hence "x\<in>cball z r" using \<open>0 < r\<close> by auto
+      then show "h x / (x - z) ^ n = f x" using h by auto
+    qed
+  then show ?thesis using `r>0` `cball z r \<subseteq> s` unfolding c_def by auto
+qed
+
+theorem residue_theorem:
+  assumes "open s" "connected (s-poles)" and 
+          holo:"f holomorphic_on s-poles" and
+          "valid_path \<gamma>" and 
+          loop:"pathfinish \<gamma> = pathstart \<gamma>" and
+          "path_image \<gamma> \<subseteq> s-poles" and
+          homo:"\<forall>z. (z \<notin> s) \<longrightarrow> winding_number \<gamma> z = 0" and
+          "finite {p. f p=0}" and
+          poles:"\<forall>p\<in>poles. is_pole f p"
+  shows "contour_integral \<gamma> f = 2 * pi * \<i> *(\<Sum>p\<in>poles. winding_number \<gamma> p * residue f p)"
+proof -
+  def pts\<equiv>"{p. f p=0}"
+  def c\<equiv>"2 * complex_of_real pi * \<i> "
+  def contour\<equiv>"\<lambda>p e. (f has_contour_integral c * residue f p) (circlepath p e)"
+  def avoid\<equiv>"\<lambda>p e. \<forall>w\<in>cball p e. w \<in> s \<and> (w \<noteq> p \<longrightarrow> w \<notin> pts)"
+  have "poles \<subseteq> pts" and "finite pts"
+    using poles `finite {p. f p=0}` unfolding pts_def is_pole_def by auto
+  have "\<exists>e>0. avoid p e \<and> (p\<in>poles \<longrightarrow> contour p e)" 
+      when "p\<in>s" for p 
+    proof -
+      obtain e1 where e:"e1>0" and e:"avoid p e1"
+        using finite_cball_avoid[OF `open s` `finite pts`] `p\<in>s` unfolding avoid_def by auto
+      have "\<exists>e2>0. cball p e2 \<subseteq> ball p e1 \<and> contour p e2"
+        when "p\<in>poles" unfolding c_def contour_def
+        proof (rule base_residue[of "ball p e1" p f,simplified,OF `e1>0`])
+          show "inverse \<circ> f holomorphic_on ball p e1" 
+            proof -
+              def f'\<equiv>"inverse o f"
+              have "f holomorphic_on ball p e1 - {p}" 
+                using holo e `poles \<subseteq> pts` unfolding avoid_def
+                apply (elim holomorphic_on_subset)
+                by auto
+              then have f'_holo:"f' holomorphic_on ball p e1 - {p}" unfolding f'_def comp_def 
+                apply (elim holomorphic_on_inverse)
+                using e pts_def  ball_subset_cball unfolding avoid_def by blast
+              moreover have "isCont f' p" using `p\<in>poles` poles unfolding f'_def is_pole_def by auto
+              ultimately show "f' holomorphic_on ball p e1"
+                apply (elim no_isolated_singularity[rotated])
+                apply (auto simp add:continuous_on_eq_continuous_at[of "ball p e1",simplified])
+                using field_differentiable_imp_continuous_at f'_holo 
+                  holomorphic_on_imp_differentiable_at by fastforce
+            qed
+        next
+          show "f p = 0" using `p\<in>poles` poles unfolding is_pole_def by auto
+        next
+          def p'\<equiv>"p+e1/2"
+          have "p'\<in>ball p e1" and "p'\<noteq>p" using `e1>0` unfolding p'_def by (auto simp add:dist_norm)
+          then show "\<exists>w\<in>ball p e1. f w \<noteq> 0" using e unfolding avoid_def
+            apply (rule_tac x=p' in bexI)
+            by (auto simp add:pts_def)
+        qed
+      then obtain e2 where e2:"p\<in>poles \<longrightarrow> e2>0 \<and> cball p e2 \<subseteq> ball p e1 \<and> contour p e2" by auto
+      def e3\<equiv>"if p\<in>poles then e2 else e1"
+      have "avoid p e3" 
+        using e2 e that  avoid_def e3_def by auto
+      moreover have "e3>0" using `e1>0` e2 unfolding e3_def by auto        
+      moreover have " p\<in>poles \<longrightarrow> contour p e3" using e2 unfolding e3_def by auto 
+      ultimately show ?thesis by auto
+    qed  
+  then obtain h where h:"\<forall>p\<in>s. h p>0 \<and> (avoid p (h p) \<and> (p\<in>poles \<longrightarrow> contour p (h p)))"
+    by metis
+  def cont\<equiv>"\<lambda>p. contour_integral (circlepath p (h p)) f"
+  have "contour_integral \<gamma> f = (\<Sum>p\<in>poles. winding_number \<gamma> p * cont p)"
+    unfolding cont_def
+    proof (rule Cauchy_theorem_singularities[OF `open s` `connected (s-poles)` _ holo `valid_path \<gamma>` 
+        loop `path_image \<gamma> \<subseteq> s-poles` homo])
+      show "finite poles" using `poles \<subseteq> pts` and `finite pts` by (simp add: finite_subset)
+    next
+      show "\<forall>p\<in>s. 0 < h p \<and> (\<forall>w\<in>cball p (h p). w \<in> s \<and> (w \<noteq> p \<longrightarrow> w \<notin> poles))"
+        using   `poles \<subseteq> pts` h unfolding avoid_def by blast
+    qed
+  also have "... = (\<Sum>p\<in>poles. c * (winding_number \<gamma> p * residue f p))" 
+    proof (rule setsum.cong[of poles poles,simplified])
+      fix p assume "p \<in> poles"
+      show "winding_number \<gamma> p * cont p = c * (winding_number \<gamma> p * residue f p)"
+        proof (cases "p\<in>s")
+          assume "p \<in> s"
+          then have "cont p=c*residue f p"
+            unfolding cont_def
+            apply (intro contour_integral_unique)
+            using h[unfolded contour_def] `p \<in> poles` by blast
+          then show ?thesis by auto
+        next
+          assume "p\<notin>s"
+          then have "winding_number \<gamma> p=0" using homo by auto
+          then show ?thesis by auto
+        qed
+    qed
+  also have "... = c * (\<Sum>p\<in>poles. winding_number \<gamma> p * residue f p)" 
+    apply (subst setsum_right_distrib)
+    by simp
+  finally show ?thesis unfolding c_def by auto
+qed   
+
+theorem argument_principle:
+  fixes f::"complex \<Rightarrow> complex" and poles s:: "complex set"
+  defines "pts\<equiv>{p. f p=0}" 
+  defines "zeros\<equiv>pts - poles"
+  assumes "open s" and 
+          connected:"connected (s- pts)" and 
+          f_holo:"f holomorphic_on s-poles" and 
+          h_holo:"h holomorphic_on s" and
+          "valid_path g" and 
+          loop:"pathfinish g = pathstart g" and
+          path_img:"path_image g \<subseteq> s - pts" and
+          homo:"\<forall>z. (z \<notin> s) \<longrightarrow> winding_number g z = 0" and
+          finite:"finite pts" and
+          poles:"\<forall>p\<in>poles. is_pole f p"
+  shows "contour_integral g (\<lambda>x. deriv f x * h x / f x) = 2 * pi * \<i> *
+          ((\<Sum>p\<in>zeros. winding_number g p * h p * zorder f p) 
+           - (\<Sum>p\<in>poles. winding_number g p * h p * porder f p))"
+    (is "?L=?R")
+proof -
+  def c\<equiv>"2 * complex_of_real pi * \<i> "
+  def ff\<equiv>"(\<lambda>x. deriv f x * h x / f x)"
+  def cont_pole\<equiv>"\<lambda>ff p e. (ff has_contour_integral - c  * porder f p * h p) (circlepath p e)"
+  def cont_zero\<equiv>"\<lambda>ff p e. (ff has_contour_integral c * zorder f p * h p ) (circlepath p e)"
+  def avoid\<equiv>"\<lambda>p e. \<forall>w\<in>cball p e. w \<in> s \<and> (w \<noteq> p \<longrightarrow> w \<notin> pts)"
+  have "poles \<subseteq> pts" and "zeros \<subseteq> pts" and "finite zeros" and "pts=zeros \<union> poles"
+    using poles `finite pts` unfolding pts_def zeros_def is_pole_def by auto
+  have "\<exists>e>0. avoid p e \<and> (p\<in>poles \<longrightarrow> cont_pole ff p e) \<and> (p\<in>zeros \<longrightarrow> cont_zero ff p e)" 
+      when "p\<in>s" for p 
+    proof -
+      obtain e1 where e:"e1>0" and e:"avoid p e1"
+        using finite_cball_avoid[OF `open s` `finite pts`] `p\<in>s` unfolding avoid_def by auto
+      have "\<exists>e2>0. cball p e2 \<subseteq> ball p e1 \<and> cont_pole ff p e2"
+        when "p\<in>poles" 
+        proof - 
+          def po\<equiv>"porder f p"
+          def pp\<equiv>"pol_poly f p"
+          def f'\<equiv>"\<lambda>w. pp w / (w - p) ^ po"
+          def ff'\<equiv>"(\<lambda>x. deriv f' x * h x / f' x)"
+          have "inverse \<circ> f holomorphic_on ball p e1" 
+            proof -
+              have "f holomorphic_on ball p e1 - {p}" 
+                using f_holo e `poles \<subseteq> pts` unfolding avoid_def
+                apply (elim holomorphic_on_subset)
+                by auto
+              then have inv_holo:"(inverse o f) holomorphic_on ball p e1 - {p}" 
+                unfolding comp_def 
+                apply (elim holomorphic_on_inverse)
+                using e pts_def  ball_subset_cball unfolding avoid_def by blast
+              moreover have "isCont (inverse o f) p" 
+                using `p\<in>poles` poles unfolding is_pole_def by auto
+              ultimately show "(inverse o f) holomorphic_on ball p e1"
+                apply (elim no_isolated_singularity[rotated])
+                apply (auto simp add:continuous_on_eq_continuous_at[of "ball p e1",simplified])
+                using field_differentiable_imp_continuous_at inv_holo 
+                  holomorphic_on_imp_differentiable_at unfolding comp_def
+                  by fastforce
+            qed
+          moreover have "f p = 0" using `p\<in>poles` poles unfolding is_pole_def by auto
+          moreover have "\<exists>w\<in>ball p e1. f w \<noteq> 0" 
+            proof -
+              def p'\<equiv>"p+e1/2"
+              have "p'\<in>ball p e1" and "p'\<noteq>p" using `e1>0` unfolding p'_def by (auto simp add:dist_norm)
+              then show "\<exists>w\<in>ball p e1. f w \<noteq> 0" using e unfolding avoid_def
+                apply (rule_tac x=p' in bexI)
+                by (auto simp add:pts_def)
+            qed
+          ultimately obtain r where 
+              "0 < po" "r>0"
+              "cball p r \<subseteq> ball p e1" and
+              pp_holo:"pp holomorphic_on cball p r" and
+              pp_po:"(\<forall>w\<in>cball p r. f w = pp w / (w - p) ^ po \<and> pp w \<noteq> 0)"
+            using porder_exist[of "ball p e1" p f,simplified,OF `e1>0`] unfolding po_def pp_def
+            by auto    
+          def e2\<equiv>"r/2"
+          have "e2>0" using `r>0` unfolding e2_def by auto
+          def anal\<equiv>"\<lambda>w. deriv pp w * h w / pp w" and prin\<equiv>"\<lambda>w. - of_nat po * h w / (w - p)"
+          have "((\<lambda>w.  prin w + anal w) has_contour_integral - c * po * h p) (circlepath p e2)"
+            proof (rule  has_contour_integral_add[of _ _ _ _ 0,simplified])
+              have "ball p r \<subseteq> s" 
+                using \<open>cball p r \<subseteq> ball p e1\<close> avoid_def ball_subset_cball e by blast
+              then have "cball p e2 \<subseteq> s"
+                using `r>0` unfolding e2_def by auto  
+              then have "(\<lambda>w. - of_nat po * h w) holomorphic_on cball p e2" 
+                using h_holo
+                by (auto intro!: holomorphic_intros)
+              then show "(prin has_contour_integral - c * of_nat po * h p ) (circlepath p e2)"
+                using Cauchy_integral_circlepath_simple[folded c_def, of "\<lambda>w. - of_nat po * h w"]
+                  `e2>0`
+                unfolding prin_def
+                by (auto simp add: mult.assoc)
+              have "anal holomorphic_on ball p r" unfolding anal_def 
+                using pp_holo h_holo pp_po `ball p r \<subseteq> s`
+                by (auto intro!: holomorphic_intros)
+              then show "(anal has_contour_integral 0) (circlepath p e2)"
+                using e2_def `r>0`
+                by (auto elim!: Cauchy_theorem_disc_simple)
+            qed
+          then have "cont_pole ff' p e2" unfolding cont_pole_def po_def
+            proof (elim has_contour_integral_eq)
+              fix w assume "w \<in> path_image (circlepath p e2)" 
+              then have "w\<in>ball p r" and "w\<noteq>p" unfolding e2_def using `r>0` by auto
+              def wp\<equiv>"w-p"
+              have "wp\<noteq>0" and "pp w \<noteq>0" 
+                unfolding wp_def using `w\<noteq>p` `w\<in>ball p r` pp_po by auto 
+              moreover have der_f':"deriv f' w = - po * pp w / (w-p)^(po+1) + deriv pp w / (w-p)^po" 
+                proof (rule DERIV_imp_deriv)
+                  def der \<equiv> "- po * pp w / (w-p)^(po+1) + deriv pp w / (w-p)^po"
+                  have po:"po = Suc (po - Suc 0) " using `po>0` by auto
+                  have "(pp has_field_derivative (deriv pp w)) (at w)" 
+                    using DERIV_deriv_iff_field_differentiable `w\<in>ball p r`
+                          holomorphic_on_imp_differentiable_at[of _ "ball p r"] 
+                          holomorphic_on_subset [OF pp_holo ball_subset_cball]
+                    by (metis open_ball)
+                  then show "(f' has_field_derivative  der) (at w)" 
+                    using `w\<noteq>p` `po>0` unfolding der_def f'_def
+                    apply (auto intro!: derivative_eq_intros simp add:field_simps)
+                    apply (subst (4) po)
+                    apply (subst power_Suc)
+                    by (auto simp add:field_simps)
+                qed
+              ultimately show "prin w + anal w = ff' w"
+                unfolding ff'_def prin_def anal_def
+                apply simp
+                apply (unfold f'_def)
+                apply (fold wp_def)
+                by (auto simp add:field_simps)
+            qed
+          then have "cont_pole ff p e2" unfolding cont_pole_def   
+            proof (elim has_contour_integral_eq)
+              fix w assume "w \<in> path_image (circlepath p e2)"
+              then have "w\<in>ball p r" and "w\<noteq>p" unfolding e2_def using `r>0` by auto
+              have "deriv f' w =  deriv f w" 
+              proof (rule complex_derivative_transform_within_open[where s="ball p r - {p}"])
+                show "f' holomorphic_on ball p r - {p}" unfolding f'_def using pp_holo
+                  by (auto intro!: holomorphic_intros)
+              next                
+                have "ball p e1 - {p} \<subseteq> s - poles" 
+                  using avoid_def ball_subset_cball e \<open>poles \<subseteq> pts\<close> by auto
+                then have "ball p r - {p} \<subseteq> s - poles" using `cball p r \<subseteq> ball p e1`
+                  using ball_subset_cball by blast
+                then show "f holomorphic_on ball p r - {p}" using f_holo
+                  by auto
+              next
+                show "open (ball p r - {p})" by auto
+              next
+                show "w \<in> ball p r - {p}" using `w\<in>ball p r` `w\<noteq>p` by auto
+              next
+                fix x assume "x \<in> ball p r - {p}"
+                then show "f' x = f x" 
+                  using pp_po unfolding f'_def by auto
+              qed
+              moreover have " f' w  =  f w " 
+                using \<open>w \<in> ball p r\<close> ball_subset_cball subset_iff pp_po unfolding f'_def by auto
+              ultimately show "ff' w = ff w"
+                unfolding ff'_def ff_def by simp
+            qed
+          moreover have "cball p e2 \<subseteq> ball p e1" 
+            using \<open>0 < r\<close> \<open>cball p r \<subseteq> ball p e1\<close> e2_def by auto
+          ultimately show ?thesis using `e2>0` by auto
+        qed
+      then obtain e2 where e2:"p\<in>poles \<longrightarrow> e2>0 \<and> cball p e2 \<subseteq> ball p e1 \<and> cont_pole ff p e2"
+        by auto
+      have "\<exists>e3>0. cball p e3 \<subseteq> ball p e1 \<and> cont_zero ff p e3"
+        when "p\<in>zeros"
+        proof -
+          def zo\<equiv>"zorder f p"
+          def zp\<equiv>"zer_poly f p"
+          def f'\<equiv>"\<lambda>w. zp w * (w - p) ^ zo"
+          def ff'\<equiv>"(\<lambda>x. deriv f' x * h x / f' x)"
+          have "f holomorphic_on ball p e1" 
+            proof -
+              have "ball p e1 \<subseteq> s - poles" 
+                using \<open>poles \<subseteq> pts\<close> avoid_def ball_subset_cball e that zeros_def by fastforce
+              thus ?thesis using f_holo by auto
+            qed
+          moreover have "f p = 0" using `p\<in>zeros` 
+            using DiffD1 mem_Collect_eq pts_def zeros_def by blast
+          moreover have "\<exists>w\<in>ball p e1. f w \<noteq> 0" 
+            proof -
+              def p'\<equiv>"p+e1/2"
+              have "p'\<in>ball p e1" and "p'\<noteq>p" using `e1>0` unfolding p'_def by (auto simp add:dist_norm)
+              then show "\<exists>w\<in>ball p e1. f w \<noteq> 0" using e unfolding avoid_def
+                apply (rule_tac x=p' in bexI)
+                by (auto simp add:pts_def)
+            qed
+          ultimately obtain r where 
+              "0 < zo" "r>0"
+              "cball p r \<subseteq> ball p e1" and
+              pp_holo:"zp holomorphic_on cball p r" and
+              pp_po:"(\<forall>w\<in>cball p r. f w = zp w * (w - p) ^ zo \<and> zp w \<noteq> 0)"
+            using zorder_exist[of "ball p e1" p f,simplified,OF `e1>0`] unfolding zo_def zp_def
+            by auto    
+          def e2\<equiv>"r/2"
+          have "e2>0" using `r>0` unfolding e2_def by auto
+          def anal\<equiv>"\<lambda>w. deriv zp w * h w / zp w" and prin\<equiv>"\<lambda>w. of_nat zo * h w / (w - p)"
+          have "((\<lambda>w.  prin w + anal w) has_contour_integral c * zo * h p) (circlepath p e2)"
+            proof (rule  has_contour_integral_add[of _ _ _ _ 0,simplified])
+              have "ball p r \<subseteq> s" 
+                using \<open>cball p r \<subseteq> ball p e1\<close> avoid_def ball_subset_cball e by blast
+              then have "cball p e2 \<subseteq> s"
+                using `r>0` unfolding e2_def by auto  
+              then have "(\<lambda>w. of_nat zo * h w) holomorphic_on cball p e2" 
+                using h_holo
+                by (auto intro!: holomorphic_intros)
+              then show "(prin has_contour_integral c * of_nat zo * h p ) (circlepath p e2)"
+                using Cauchy_integral_circlepath_simple[folded c_def, of "\<lambda>w. of_nat zo * h w"]
+                  `e2>0`
+                unfolding prin_def
+                by (auto simp add: mult.assoc)
+              have "anal holomorphic_on ball p r" unfolding anal_def 
+                using pp_holo h_holo pp_po `ball p r \<subseteq> s`
+                by (auto intro!: holomorphic_intros)
+              then show "(anal has_contour_integral 0) (circlepath p e2)"
+                using e2_def `r>0`
+                by (auto elim!: Cauchy_theorem_disc_simple)
+            qed
+          then have "cont_zero ff' p e2" unfolding cont_zero_def zo_def
+            proof (elim has_contour_integral_eq)
+              fix w assume "w \<in> path_image (circlepath p e2)" 
+              then have "w\<in>ball p r" and "w\<noteq>p" unfolding e2_def using `r>0` by auto
+              def wp\<equiv>"w-p"
+              have "wp\<noteq>0" and "zp w \<noteq>0" 
+                unfolding wp_def using `w\<noteq>p` `w\<in>ball p r` pp_po by auto 
+              moreover have der_f':"deriv f' w = zo * zp w * (w-p)^(zo-1) + deriv zp w * (w-p)^zo" 
+                proof (rule DERIV_imp_deriv)
+                  def der\<equiv>"zo * zp w * (w-p)^(zo-1) + deriv zp w * (w-p)^zo"
+                  have po:"zo = Suc (zo - Suc 0) " using `zo>0` by auto
+                  have "(zp has_field_derivative (deriv zp w)) (at w)" 
+                    using DERIV_deriv_iff_field_differentiable `w\<in>ball p r`
+                          holomorphic_on_imp_differentiable_at[of _ "ball p r"] 
+                          holomorphic_on_subset [OF pp_holo ball_subset_cball]
+                    by (metis open_ball)
+                  then show "(f' has_field_derivative  der) (at w)" 
+                    using `w\<noteq>p` `zo>0` unfolding der_def f'_def
+                    by (auto intro!: derivative_eq_intros simp add:field_simps)
+                qed
+              ultimately show "prin w + anal w = ff' w"
+                unfolding ff'_def prin_def anal_def
+                apply simp
+                apply (unfold f'_def)
+                apply (fold wp_def)
+                apply (auto simp add:field_simps)
+                by (metis Suc_diff_Suc minus_nat.diff_0 power_Suc)
+            qed
+          then have "cont_zero ff p e2" unfolding cont_zero_def   
+            proof (elim has_contour_integral_eq)
+              fix w assume "w \<in> path_image (circlepath p e2)"
+              then have "w\<in>ball p r" and "w\<noteq>p" unfolding e2_def using `r>0` by auto
+              have "deriv f' w =  deriv f w" 
+                proof (rule complex_derivative_transform_within_open[where s="ball p r - {p}"])
+                  show "f' holomorphic_on ball p r - {p}" unfolding f'_def using pp_holo
+                    by (auto intro!: holomorphic_intros)
+                next                
+                  have "ball p e1 - {p} \<subseteq> s - poles" 
+                    using avoid_def ball_subset_cball e \<open>poles \<subseteq> pts\<close> by auto
+                  then have "ball p r - {p} \<subseteq> s - poles" using `cball p r \<subseteq> ball p e1`
+                    using ball_subset_cball by blast
+                  then show "f holomorphic_on ball p r - {p}" using f_holo
+                    by auto
+                next
+                  show "open (ball p r - {p})" by auto
+                next
+                  show "w \<in> ball p r - {p}" using `w\<in>ball p r` `w\<noteq>p` by auto
+                next
+                  fix x assume "x \<in> ball p r - {p}"
+                  then show "f' x = f x" 
+                    using pp_po unfolding f'_def by auto
+                qed
+              moreover have " f' w  =  f w " 
+                using \<open>w \<in> ball p r\<close> ball_subset_cball subset_iff pp_po unfolding f'_def by auto
+              ultimately show "ff' w = ff w"
+                unfolding ff'_def ff_def by simp
+            qed
+          moreover have "cball p e2 \<subseteq> ball p e1" 
+            using \<open>0 < r\<close> \<open>cball p r \<subseteq> ball p e1\<close> e2_def by auto
+          ultimately show ?thesis using `e2>0` by auto
+        qed
+      then obtain e3 where e3:"p\<in>zeros \<longrightarrow> e3>0 \<and> cball p e3 \<subseteq> ball p e1 \<and> cont_zero ff p e3"
+        by auto          
+      def e4\<equiv>"if p\<in>poles then e2 else if p\<in>zeros then e3 else e1"
+      have "e4>0" using e2 e3 `e1>0` unfolding e4_def by auto
+      moreover have "avoid p e4" using e2 e3 `e1>0` e unfolding e4_def avoid_def by auto
+      moreover have "p\<in>poles \<longrightarrow> cont_pole ff p e4" and "p\<in>zeros \<longrightarrow> cont_zero ff p e4" 
+        by (auto simp add: e2 e3 e4_def pts_def zeros_def)
+      ultimately show ?thesis by auto
+    qed
+  then obtain get_e where get_e:"\<forall>p\<in>s. get_e p>0 \<and> avoid p (get_e p) 
+      \<and> (p\<in>poles \<longrightarrow> cont_pole ff p (get_e p)) \<and> (p\<in>zeros \<longrightarrow> cont_zero ff p (get_e p))"
+    by metis
+  def cont\<equiv>"\<lambda>p. contour_integral (circlepath p (get_e p)) ff"
+  def w\<equiv>"\<lambda>p. winding_number g p"
+  have "contour_integral g ff = (\<Sum>p\<in>pts. w p * cont p)"
+    unfolding cont_def w_def
+    proof (rule Cauchy_theorem_singularities[OF `open s` connected finite _ `valid_path g` loop 
+        path_img homo])
+      have "open (s - pts)" using open_Diff[OF _ finite_imp_closed[OF finite]] `open s` by auto 
+      then show "ff holomorphic_on s - pts" unfolding ff_def using f_holo `poles \<subseteq> pts` h_holo
+        by (auto intro!: holomorphic_intros simp add:pts_def)
+    next
+      show "\<forall>p\<in>s. 0 < get_e p \<and> (\<forall>w\<in>cball p (get_e p). w \<in> s \<and> (w \<noteq> p \<longrightarrow> w \<notin> pts))"
+        using get_e using avoid_def by blast
+    qed
+  also have "... = (\<Sum>p\<in>zeros. w p * cont p) + (\<Sum>p\<in>poles. w p * cont p)"
+    using `finite pts` unfolding `pts=zeros \<union> poles`
+    apply (subst setsum.union_disjoint)
+    by (auto simp add:zeros_def)
+  also have "... = c * ((\<Sum>p\<in>zeros. w p *  h p * zorder f p) - (\<Sum>p\<in>poles. w p *  h p * porder f p))"
+    proof -
+      have "(\<Sum>p\<in>zeros. w p * cont p) = (\<Sum>p\<in>zeros. c * w p *  h p * zorder f p)" 
+        proof (rule setsum.cong[of zeros zeros,simplified])
+          fix p assume "p \<in> zeros"
+          show "w p * cont p = c * w p * h p * (zorder f p)"
+            proof (cases "p\<in>s")
+              assume "p \<in> s"
+              have "cont p = c * h p * (zorder f p)" unfolding cont_def
+                apply (rule contour_integral_unique)
+                using get_e `p\<in>s` `p\<in>zeros` unfolding cont_zero_def                
+                by (metis mult.assoc mult.commute)
+              thus ?thesis by auto
+            next
+              assume "p\<notin>s"
+              then have "w p=0" using homo unfolding w_def by auto
+              then show ?thesis by auto
+            qed
+        qed
+      then have "(\<Sum>p\<in>zeros. w p * cont p) = c * (\<Sum>p\<in>zeros.  w p *  h p * zorder f p)" 
+        apply (subst setsum_right_distrib)
+        by (simp add:algebra_simps)
+      moreover have "(\<Sum>p\<in>poles. w p * cont p) = (\<Sum>p\<in>poles.  - c * w p *  h p * porder f p)" 
+        proof (rule setsum.cong[of poles poles,simplified])
+          fix p assume "p \<in> poles"
+          show "w p * cont p = - c * w p * h p * (porder f p)"
+            proof (cases "p\<in>s")
+              assume "p \<in> s"
+              have "cont p = - c * h p * (porder f p)" unfolding cont_def
+                apply (rule contour_integral_unique)
+                using get_e `p\<in>s` `p\<in>poles` unfolding cont_pole_def               
+                by (metis mult.assoc mult.commute)
+              thus ?thesis by auto
+            next
+              assume "p\<notin>s"
+              then have "w p=0" using homo unfolding w_def by auto
+              then show ?thesis by auto
+            qed
+        qed
+      then have "(\<Sum>p\<in>poles. w p * cont p) = - c * (\<Sum>p\<in>poles. w p *  h p * porder f p)" 
+        apply (subst setsum_right_distrib)
+        by (simp add:algebra_simps)
+      ultimately show ?thesis by (simp add: right_diff_distrib)
+    qed      
+  finally show ?thesis unfolding w_def ff_def c_def by auto
+qed
+
+lemma holomorphic_imp_diff_on:
+  assumes f_holo:"f holomorphic_on s" and "open s"
+  shows "f differentiable_on s"
+proof (rule differentiable_at_imp_differentiable_on)
+  fix x assume "x\<in>s"
+  obtain f' where "(f has_field_derivative f') (at x) "
+    using holomorphic_on_imp_differentiable_at[OF f_holo `open s` `x\<in>s`] 
+    unfolding field_differentiable_def by auto
+  then have " (f has_derivative op * f') (at x)"
+    using has_field_derivative_imp_has_derivative[of f f' "at x"] by auto
+  then show "f differentiable at x" using differentiableI by auto
+qed
+
+theorem Rouche_theorem:
+  fixes f g::"complex \<Rightarrow> complex" and s:: "complex set"
+  defines "fg\<equiv>(\<lambda>p. f p+ g p)"
+  defines "zeros_fg\<equiv>{p. fg p =0}" and "zeros_f\<equiv>{p. f p=0}"
+  assumes
+    "open s" and 
+    connected_fg:"connected (s- zeros_fg)" and 
+    connected_f:"connected (s- zeros_f)" and 
+    "finite zeros_fg" and 
+    "finite zeros_f" and
+    f_holo:"f holomorphic_on s" and 
+    g_holo:"g holomorphic_on s" and
+    "valid_path \<gamma>" and 
+    loop:"pathfinish \<gamma> = pathstart \<gamma>" and
+    path_img:"path_image \<gamma> \<subseteq> s " and
+    path_less:"\<forall>z\<in>path_image \<gamma>. cmod(f z) > cmod(g z)" and 
+    homo:"\<forall>z. (z \<notin> s) \<longrightarrow> winding_number \<gamma> z = 0"
+  shows "(\<Sum>p\<in>zeros_fg. winding_number \<gamma> p * zorder fg p) 
+          = (\<Sum>p\<in>zeros_f. winding_number \<gamma> p * zorder f p)"
+proof -
+  have path_fg:"path_image \<gamma> \<subseteq> s - zeros_fg"
+    proof -
+      have False when "z\<in>path_image \<gamma>" and "f z + g z=0" for z 
+        proof -
+          have "cmod (f z) > cmod (g z)" using `z\<in>path_image \<gamma>` path_less by auto
+          moreover have "f z = - g z"  using `f z + g z =0` by (simp add: eq_neg_iff_add_eq_0)
+          then have "cmod (f z) = cmod (g z)" by auto
+          ultimately show False by auto
+        qed
+      then show ?thesis unfolding zeros_fg_def fg_def using path_img by auto 
+    qed
+  have path_f:"path_image \<gamma> \<subseteq> s - zeros_f"
+    proof -
+      have False when "z\<in>path_image \<gamma>" and "f z =0" for z 
+        proof -
+          have "cmod (g z) < cmod (f z) " using `z\<in>path_image \<gamma>` path_less by auto
+          then have "cmod (g z) < 0" using `f z=0` by auto          
+          then show False by auto
+        qed
+      then show ?thesis unfolding zeros_f_def using path_img by auto 
+    qed
+  def w\<equiv>"\<lambda>p. winding_number \<gamma> p"
+  def c\<equiv>"2 * complex_of_real pi * \<i>"
+  def h\<equiv>"\<lambda>p. g p / f p + 1" 
+  obtain spikes
+    where "finite spikes" and spikes: "\<forall>x\<in>{0..1} - spikes. \<gamma> differentiable at x"
+    using `valid_path \<gamma>`
+    by (auto simp: valid_path_def piecewise_C1_differentiable_on_def C1_differentiable_on_eq)
+  have h_contour:"((\<lambda>x. deriv h x / h x) has_contour_integral 0) \<gamma>" 
+    proof -
+      have outside_img:"0 \<in> outside (path_image (h o \<gamma>))" 
+        proof -
+          have "h p \<in> ball 1 1" when "p\<in>path_image \<gamma>" for p
+            proof -
+              have "cmod (g p/f p) <1" using path_less[rule_format,OF that] 
+                apply (cases "cmod (f p) = 0")
+                by (auto simp add: norm_divide)
+              then show ?thesis unfolding h_def by (auto simp add:dist_complex_def)
+            qed
+          then have "path_image (h o \<gamma>) \<subseteq> ball 1 1" 
+            by (simp add: image_subset_iff path_image_compose)
+          moreover have " (0::complex) \<notin> ball 1 1" by (simp add: dist_norm)
+          ultimately show "?thesis"
+            using  convex_in_outside[of "ball 1 1" "0::complex"]
+            apply (drule_tac outside_mono)
+            by auto
+        qed
+      have valid_h:"valid_path (h \<circ> \<gamma>)"
+        proof (rule valid_path_compose_holomorphic[OF `valid_path \<gamma>` _ _ path_f])
+          show "h holomorphic_on s - zeros_f" 
+            unfolding h_def using f_holo g_holo
+            by (auto intro!: holomorphic_intros simp add:zeros_f_def)
+        next
+          show "open (s - zeros_f)" using `finite zeros_f` `open s` finite_imp_closed
+            by auto
+        qed
+      have "((\<lambda>z. 1/z) has_contour_integral 0) (h \<circ> \<gamma>)" 
+        proof -
+          have "0 \<notin> path_image (h \<circ> \<gamma>)" using outside_img by (simp add: outside_def)
+          then have "((\<lambda>z. 1/z) has_contour_integral c * winding_number (h \<circ> \<gamma>) 0) (h \<circ> \<gamma>)"
+            using has_contour_integral_winding_number[of "h o \<gamma>" 0,simplified] valid_h 
+            unfolding c_def by auto
+          moreover have "winding_number (h o \<gamma>) 0 = 0" 
+            proof -
+              have "0 \<in> outside (path_image (h \<circ> \<gamma>))" using outside_img .
+              moreover have "path (h o \<gamma>)" 
+                using valid_h by auto
+              moreover have "pathfinish (h o \<gamma>) = pathstart (h o \<gamma>)" 
+                by (simp add: loop pathfinish_compose pathstart_compose)
+              ultimately show ?thesis using winding_number_zero_in_outside by auto
+            qed
+          ultimately show ?thesis by auto
+        qed
+      moreover have "vector_derivative (h \<circ> \<gamma>) (at x) = vector_derivative \<gamma> (at x) * deriv h (\<gamma> x)"
+          when "x\<in>{0..1} - spikes" for x 
+        proof (rule vector_derivative_chain_at_general)
+          show "\<gamma> differentiable at x" using that `valid_path \<gamma>` spikes by auto
+        next
+          def der\<equiv>"\<lambda>p. (deriv g p * f p - g p * deriv f p)/(f p * f p)"
+          def t\<equiv>"\<gamma> x"
+          have "f t\<noteq>0" unfolding zeros_f_def t_def 
+            by (metis DiffD1 image_eqI norm_not_less_zero norm_zero path_defs(4) path_less that)
+          moreover have "t\<in>s" 
+            using contra_subsetD path_image_def path_fg t_def that by fastforce
+          ultimately have "(h has_field_derivative der t) (at t)"
+            unfolding h_def der_def using g_holo f_holo
+            apply (auto intro!: derivative_eq_intros)
+            by (auto simp add: DERIV_deriv_iff_field_differentiable 
+              holomorphic_on_imp_differentiable_at[OF _ `open s`])
+          then show "\<exists>g'. (h has_field_derivative g') (at (\<gamma> x))" unfolding t_def by auto
+        qed
+      then have " (op / 1 has_contour_integral 0) (h \<circ> \<gamma>) 
+          = ((\<lambda>x. deriv h x / h x) has_contour_integral 0) \<gamma>"  
+        unfolding has_contour_integral
+        apply (intro has_integral_spike_eq[OF negligible_finite, OF `finite spikes`])
+        by auto
+      ultimately show ?thesis by auto
+    qed
+  then have "contour_integral \<gamma> (\<lambda>x. deriv h x / h x) = 0" 
+    using  contour_integral_unique by simp
+  moreover have "contour_integral \<gamma> (\<lambda>x. deriv fg x / fg x) = contour_integral \<gamma> (\<lambda>x. deriv f x / f x) 
+      + contour_integral \<gamma> (\<lambda>p. deriv h p / h p)" 
+    proof -
+      have "(\<lambda>p. deriv f p / f p) contour_integrable_on \<gamma>" 
+        proof (rule contour_integrable_holomorphic_simple[OF _ _ `valid_path \<gamma>` path_f])
+          show "open (s - zeros_f)" using finite_imp_closed[OF `finite zeros_f`] `open s` 
+            by auto
+          then show "(\<lambda>p. deriv f p / f p) holomorphic_on s - zeros_f"
+            using f_holo
+            by (auto intro!: holomorphic_intros simp add:zeros_f_def)
+        qed
+      moreover have "(\<lambda>p. deriv h p / h p) contour_integrable_on \<gamma>" 
+        using h_contour
+        by (simp add: has_contour_integral_integrable)
+      ultimately have "contour_integral \<gamma> (\<lambda>x. deriv f x / f x + deriv h x / h x) =
+          contour_integral \<gamma> (\<lambda>p. deriv f p / f p) + contour_integral \<gamma> (\<lambda>p. deriv h p / h p)"
+        using contour_integral_add[of "(\<lambda>p. deriv f p / f p)" \<gamma> "(\<lambda>p. deriv h p / h p)" ]
+        by auto
+      moreover have "deriv fg p / fg p =  deriv f p / f p + deriv h p / h p"
+          when "p\<in> path_image \<gamma>" for p 
+        proof -
+          have "fg p\<noteq>0" and "f p\<noteq>0" using path_f path_fg that unfolding zeros_f_def zeros_fg_def
+            by auto
+          have "h p\<noteq>0" 
+            proof (rule ccontr)
+              assume "\<not> h p \<noteq> 0"
+              then have "g p / f p= -1" unfolding h_def by (simp add: add_eq_0_iff2)
+              then have "cmod (g p/f p) = 1" by auto
+              moreover have "cmod (g p/f p) <1" using path_less[rule_format,OF that] 
+                apply (cases "cmod (f p) = 0")
+                by (auto simp add: norm_divide)
+              ultimately show False by auto
+            qed
+          have der_fg:"deriv fg p =  deriv f p + deriv g p" unfolding fg_def
+            using f_holo g_holo holomorphic_on_imp_differentiable_at[OF _  `open s`] path_img that
+            by (auto intro!: deriv_add)
+          have der_h:"deriv h p = (deriv g p * f p - g p * deriv f p)/(f p * f p)"
+            proof -
+              def der\<equiv>"\<lambda>p. (deriv g p * f p - g p * deriv f p)/(f p * f p)"          
+              have "p\<in>s" using path_img that by auto
+              then have "(h has_field_derivative der p) (at p)"
+                unfolding h_def der_def using g_holo f_holo `f p\<noteq>0`
+                apply (auto intro!: derivative_eq_intros)
+                by (auto simp add: DERIV_deriv_iff_field_differentiable 
+                    holomorphic_on_imp_differentiable_at[OF _ `open s`])
+              then show ?thesis unfolding der_def using DERIV_imp_deriv by auto
+            qed
+          show ?thesis
+            apply (simp only:der_fg der_h)   
+            apply (auto simp add:field_simps `h p\<noteq>0` `f p\<noteq>0` `fg p\<noteq>0`)
+            by (auto simp add:field_simps h_def `f p\<noteq>0` fg_def) 
+        qed
+      then have "contour_integral \<gamma> (\<lambda>p. deriv fg p / fg p) 
+          = contour_integral \<gamma> (\<lambda>p. deriv f p / f p + deriv h p / h p)"
+        by (elim contour_integral_eq)        
+      ultimately show ?thesis by auto
+    qed
+  moreover have "contour_integral \<gamma> (\<lambda>x. deriv fg x / fg x) = c * (\<Sum>p\<in>zeros_fg. w p * zorder fg p)"
+    unfolding c_def zeros_fg_def w_def 
+    proof (rule argument_principle[OF `open s` _ _ _ `valid_path \<gamma>` loop _ homo, of _ "{}" "\<lambda>_. 1",simplified])
+      show "connected (s - {p. fg p = 0})" using connected_fg unfolding zeros_fg_def .
+      show "fg holomorphic_on s" unfolding fg_def using f_holo g_holo holomorphic_on_add by auto
+      show "path_image \<gamma> \<subseteq> s - {p. fg p = 0}" using path_fg unfolding zeros_fg_def .
+      show " finite {p. fg p = 0}" using `finite zeros_fg` unfolding zeros_fg_def .
+    qed
+  moreover have "contour_integral \<gamma> (\<lambda>x. deriv f x / f x) = c * (\<Sum>p\<in>zeros_f. w p * zorder f p)"
+    unfolding c_def zeros_f_def w_def 
+    proof (rule argument_principle[OF `open s` _ _ _ `valid_path \<gamma>` loop _ homo, of _ "{}" "\<lambda>_. 1",simplified])
+      show "connected (s - {p. f p = 0})" using connected_f unfolding zeros_f_def .
+      show "f holomorphic_on s" using f_holo g_holo holomorphic_on_add by auto
+      show "path_image \<gamma> \<subseteq> s - {p. f p = 0}" using path_f unfolding zeros_f_def .
+      show "finite {p. f p = 0}" using `finite zeros_f` unfolding zeros_f_def .
+    qed  
+  ultimately have "c * (\<Sum>p\<in>zeros_fg. w p * (zorder fg p)) = c* (\<Sum>p\<in>zeros_f. w p * (zorder f p))"
+    by auto
+  then show ?thesis unfolding c_def using w_def by auto
+qed
+
 end