# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1464190715 -3600
# Node ID 82df5181d69988f3df7987cff1104ba7e112dd16
# Parent  6a131df8e3d944580b7856c9744ccb9c46cf0293
updated proof of Residue Theorem (form Wenda Li)

diff -r 6a131df8e3d9 -r 82df5181d699 src/HOL/Multivariate_Analysis/Conformal_Mappings.thy
--- a/src/HOL/Multivariate_Analysis/Conformal_Mappings.thy	Wed May 25 13:13:35 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Conformal_Mappings.thy	Wed May 25 16:38:35 2016 +0100
@@ -9,6 +9,33 @@
 
 begin
 
+lemma finite_ball_avoid:
+  assumes "open S" "finite X" "p \<in> S"
+  shows "\<exists>e>0. \<forall>w\<in>ball p e. w\<in>S \<and> (w\<noteq>p \<longrightarrow> w\<notin>X)"
+proof -
+  obtain e1 where "0 < e1" and e1_b:"ball p e1 \<subseteq> S" 
+    using open_contains_ball_eq[OF \<open>open S\<close>] assms by auto
+  obtain e2 where "0<e2" and "\<forall>x\<in>X. x \<noteq> p \<longrightarrow> e2 \<le> dist p x" 
+    using finite_set_avoid[OF \<open>finite X\<close>,of p] by auto
+  hence "\<forall>w\<in>ball p (min e1 e2). w\<in>S \<and> (w\<noteq>p \<longrightarrow> w\<notin>X)" 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> X)" using \<open>e2>0\<close> \<open>e1>0\<close> 
+    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 X" "p \<in> S"
+  shows "\<exists>e>0. \<forall>w\<in>cball p e. w\<in>S \<and> (w\<noteq>p \<longrightarrow> w\<notin>X)"
+proof -
+  obtain e1 where "e1>0" and e1: "\<forall>w\<in>ball p e1. w\<in>S \<and> (w\<noteq>p \<longrightarrow> w\<notin>X)" 
+    using finite_ball_avoid[OF assms] by auto
+  define e2 where "e2 \<equiv> e1/2"
+  have "e2>0" and "e2<e1" unfolding e2_def using \<open>e1>0\<close> 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> X)" using \<open>e2>0\<close> e1 by auto
+qed
+
 subsection\<open>Cauchy's inequality and more versions of Liouville\<close>
 
 lemma Cauchy_higher_deriv_bound:
@@ -2134,159 +2161,282 @@
   qed
 qed
 
-subsection \<open>Cauchy's residue theorem\<close>
+subsection \<open>Foundations of Cauchy's residue theorem\<close>
 
-text\<open>Wenda Li (2016)\<close>
+text\<open>Wenda Li and LC Paulson (2016). A Formal Proof of Cauchy's Residue Theorem.
+    Interactive Theorem Proving\<close>
 
-declare valid_path_imp_path [simp] 
+definition residue :: "(complex \<Rightarrow> complex) \<Rightarrow> complex \<Rightarrow> complex" where
+  "residue f z = (SOME int. \<exists>e>0. \<forall>\<epsilon>>0. \<epsilon><e 
+    \<longrightarrow> (f has_contour_integral 2*pi* ii *int) (circlepath z \<epsilon>))"
 
-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" 
+lemma contour_integral_circlepath_eq:
+  assumes "open s" and f_holo:"f holomorphic_on (s-{z})" and "0<e1" "e1\<le>e2" 
+    and e2_cball:"cball z e2 \<subseteq> s"
+  shows
+    "f contour_integrable_on circlepath z e1"
+    "f contour_integrable_on circlepath z e2"
+    "contour_integral (circlepath z e2) f = contour_integral (circlepath z e1) f"
 proof -
-  have "n>m \<Longrightarrow> False"
+  define l where "l \<equiv> linepath (z+e2) (z+e1)"
+  have [simp]:"valid_path l" "pathstart l=z+e2" "pathfinish l=z+e1" unfolding l_def by auto
+  have "e2>0" using \<open>e1>0\<close> \<open>e1\<le>e2\<close> by auto
+  have zl_img:"z\<notin>path_image l"
+    proof 
+      assume "z \<in> path_image l"
+      then have "e2 \<le> cmod (e2 - e1)"
+        using segment_furthest_le[of z "z+e2" "z+e1" "z+e2",simplified] \<open>e1>0\<close> \<open>e2>0\<close> unfolding l_def
+        by (auto simp add:closed_segment_commute)
+      thus False using \<open>e2>0\<close> \<open>e1>0\<close> \<open>e1\<le>e2\<close> 
+        apply (subst (asm) norm_of_real)
+        by auto
+    qed
+  define g where "g \<equiv> circlepath z e2 +++ l +++ reversepath (circlepath z e1) +++ reversepath l"
+  show [simp]: "f contour_integrable_on circlepath z e2" "f contour_integrable_on (circlepath z e1)" 
     proof -
-      assume "n>m"
-      have "(h \<longlongrightarrow> 0) (at z within ball z r)" 
-        proof (rule Lim_transform_within[OF _ \<open>r>0\<close>, 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 \<open>n>m\<close> 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
-          define F where "F = at z within ball z r"
-          define f' where [abs_def]: "f' x = (x - z) ^ (n-m)" for x
-          have "f' z=0" using \<open>n>m\<close> 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] \<open>r>0\<close>
-            unfolding F_def by auto
-          ultimately show " ((\<lambda>w. f' w * g w) \<longlongrightarrow> 0) F" using tendsto_mult by fastforce
+      show "f contour_integrable_on circlepath z e2" 
+        apply (intro contour_integrable_continuous_circlepath[OF 
+                continuous_on_subset[OF holomorphic_on_imp_continuous_on[OF f_holo]]])
+        using \<open>e2>0\<close> e2_cball by auto
+      show "f contour_integrable_on (circlepath z e1)" 
+        apply (intro contour_integrable_continuous_circlepath[OF 
+                      continuous_on_subset[OF holomorphic_on_imp_continuous_on[OF f_holo]]])
+        using \<open>e1>0\<close> \<open>e1\<le>e2\<close> e2_cball by auto
+    qed
+  have [simp]:"f contour_integrable_on l"
+    proof -
+      have "closed_segment (z + e2) (z + e1) \<subseteq> cball z e2" using \<open>e2>0\<close> \<open>e1>0\<close> \<open>e1\<le>e2\<close>
+        by (intro closed_segment_subset,auto simp add:dist_norm)
+      hence "closed_segment (z + e2) (z + e1) \<subseteq> s - {z}" using zl_img e2_cball unfolding l_def
+        by auto
+      then show "f contour_integrable_on l" unfolding l_def
+        apply (intro contour_integrable_continuous_linepath[OF 
+                      continuous_on_subset[OF holomorphic_on_imp_continuous_on[OF f_holo]]])
+        by auto
+    qed
+  let ?ig="\<lambda>g. contour_integral g f"
+  have "(f has_contour_integral 0) g"
+    proof (rule Cauchy_theorem_global[OF _ f_holo])
+      show "open (s - {z})" using \<open>open s\<close> by auto
+      show "valid_path g" unfolding g_def l_def by auto
+      show "pathfinish g = pathstart g" unfolding g_def l_def by auto
+    next
+      have path_img:"path_image g \<subseteq> cball z e2"
+        proof -
+          have "closed_segment (z + e2) (z + e1) \<subseteq> cball z e2" using \<open>e2>0\<close> \<open>e1>0\<close> \<open>e1\<le>e2\<close>
+            by (intro closed_segment_subset,auto simp add:dist_norm)  
+          moreover have "sphere z \<bar>e1\<bar> \<subseteq> cball z e2" using \<open>e2>0\<close> \<open>e1\<le>e2\<close> \<open>e1>0\<close> by auto
+          ultimately show ?thesis unfolding g_def l_def using \<open>e2>0\<close> 
+            by (simp add: path_image_join closed_segment_commute)
         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 \<open>r>0\<close>) 
-      moreover have "at z within ball z r \<noteq> bot" using \<open>r>0\<close> 
-        by (auto simp add:trivial_limit_within islimpt_ball)
-      ultimately have "h z=0" by (auto intro: tendsto_unique)
-      thus False using asm \<open>r>0\<close> 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 _ \<open>r>0\<close>, 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 \<open>m>n\<close> 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
-          define F where "F = at z within ball z r"
-          define f' where [abs_def]: "f' x = (x - z) ^ (m-n)" for x
-          have "f' z=0" using \<open>m>n\<close> 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] \<open>r>0\<close>
-            unfolding F_def by auto
-          ultimately show " ((\<lambda>w. f' w * h w) \<longlongrightarrow> 0) F" using tendsto_mult by fastforce
+      show "path_image g \<subseteq> s - {z}"  
+        proof -
+          have "z\<notin>path_image g" using zl_img      
+            unfolding g_def l_def by (auto simp add: path_image_join closed_segment_commute)
+          moreover note \<open>cball z e2 \<subseteq> s\<close> and path_img
+          ultimately show ?thesis by auto
         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 \<open>r>0\<close>) 
-      moreover have "at z within ball z r \<noteq> bot" using \<open>r>0\<close> 
-        by (auto simp add:trivial_limit_within islimpt_ball)
-      ultimately have "g z=0" by (auto intro: tendsto_unique)
-      thus False using asm \<open>r>0\<close> by auto
-    qed
-  ultimately show "n=m" by fastforce
+      show "winding_number g w = 0" when"w \<notin> s - {z}" for w
+        proof -
+          have "winding_number g w = 0" when "w\<notin>s" using that e2_cball
+            apply (intro winding_number_zero_outside[OF _ _ _ _ path_img])
+            by (auto simp add:g_def l_def)
+          moreover have "winding_number g z=0" 
+            proof -
+              let ?Wz="\<lambda>g. winding_number g z"
+              have "?Wz g = ?Wz (circlepath z e2) + ?Wz l + ?Wz (reversepath (circlepath z e1)) 
+                  + ?Wz (reversepath l)"
+                using \<open>e2>0\<close> \<open>e1>0\<close> zl_img unfolding g_def l_def  
+                by (subst winding_number_join,auto simp add:path_image_join closed_segment_commute)+
+              also have "... = ?Wz (circlepath z e2) + ?Wz (reversepath (circlepath z e1))"
+                using zl_img
+                apply (subst (2) winding_number_reversepath)
+                by (auto simp add:l_def closed_segment_commute)
+              also have "... = 0"
+                proof -
+                  have "?Wz (circlepath z e2) = 1" using \<open>e2>0\<close>
+                    by (auto intro: winding_number_circlepath_centre)
+                  moreover have "?Wz (reversepath (circlepath z e1)) = -1" using \<open>e1>0\<close>
+                    apply (subst winding_number_reversepath)
+                    by (auto intro: winding_number_circlepath_centre)
+                  ultimately show ?thesis by auto
+                qed
+              finally show ?thesis .
+            qed
+          ultimately show ?thesis using that by auto
+        qed  
+    qed        
+  then have "0 = ?ig g" using contour_integral_unique by simp
+  also have "... = ?ig (circlepath z e2) + ?ig l + ?ig (reversepath (circlepath z e1)) 
+      + ?ig (reversepath l)"
+    unfolding g_def 
+    by (auto simp add:contour_integrable_reversepath_eq)
+  also have "... = ?ig (circlepath z e2)  - ?ig (circlepath z e1)"
+    by (auto simp add:contour_integral_reversepath)
+  finally show "contour_integral (circlepath z e2) f = contour_integral (circlepath z e1) f" 
+    by simp
 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>open s\<close> \<open>connected s\<close> \<open>z\<in>s\<close> \<open>f z=0\<close>]
-    by (metis assms(3) assms(5) assms(6))
-  define r' where "r' = 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 \<open>ball z r \<subseteq> s\<close> by auto
-  moreover have "r'>0" unfolding r'_def using \<open>0<r\<close> 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:\<open>0 < n\<close>)
-next
-  fix m n 
-  define fac where "fac n g r \<longleftrightarrow> (\<forall>w\<in>cball z r. f w = (w - z) ^ n * g w \<and> g w \<noteq> 0)" for n g r
-  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
-  define r where "r = min r1 r2"
-  have "r>0" using \<open>r1>0\<close> \<open>r2>0\<close> 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)
+lemma base_residue:
+  assumes "open s" "z\<in>s" "r>0" and f_holo:"f holomorphic_on (s - {z})" 
+    and r_cball:"cball z r \<subseteq> s"
+  shows "(f has_contour_integral 2*pi*ii* (residue f z)) (circlepath z r)"
+proof -
+  obtain e where "e>0" and e_cball:"cball z e \<subseteq> s" 
+    using open_contains_cball[of s] \<open>open s\<close> \<open>z\<in>s\<close> by auto
+  define c where "c \<equiv> 2*pi*ii"
+  define i where "i \<equiv> contour_integral (circlepath z e) f / c"
+  have "(f has_contour_integral c*i) (circlepath z \<epsilon>)" when "\<epsilon>>0" "\<epsilon><e" for \<epsilon> 
+    proof -
+      have "contour_integral (circlepath z e) f = contour_integral (circlepath z \<epsilon>) f"
+          "f contour_integrable_on circlepath z \<epsilon>"
+          "f contour_integrable_on circlepath z e"
+        using \<open>\<epsilon><e\<close>
+        by (intro contour_integral_circlepath_eq[OF \<open>open s\<close> f_holo \<open>\<epsilon>>0\<close> _ e_cball],auto)+        
+      then show ?thesis unfolding i_def c_def
+        by (auto intro:has_contour_integral_integral)
+    qed
+  then have "\<exists>e>0. \<forall>\<epsilon>>0. \<epsilon><e \<longrightarrow> (f has_contour_integral c * (residue f z)) (circlepath z \<epsilon>)" 
+    unfolding residue_def c_def
+    apply (rule_tac someI[of _ i],intro  exI[where x=e])
+    by (auto simp add:\<open>e>0\<close> c_def)
+  then obtain e' where "e'>0" 
+      and e'_def:"\<forall>\<epsilon>>0. \<epsilon><e' \<longrightarrow> (f has_contour_integral c * (residue f z)) (circlepath z \<epsilon>)"
+    by auto
+  let ?int="\<lambda>e. contour_integral (circlepath z e) f"
+  def \<epsilon>\<equiv>"Min {r,e'} / 2"
+  have "\<epsilon>>0" "\<epsilon>\<le>r" "\<epsilon><e'" using \<open>r>0\<close> \<open>e'>0\<close> unfolding \<epsilon>_def by auto
+  have "(f has_contour_integral c * (residue f z)) (circlepath z \<epsilon>)"
+    using e'_def[rule_format,OF \<open>\<epsilon>>0\<close> \<open>\<epsilon><e'\<close>] .
+  then show ?thesis unfolding c_def 
+    using contour_integral_circlepath_eq[OF \<open>open s\<close> f_holo \<open>\<epsilon>>0\<close> \<open>\<epsilon>\<le>r\<close> r_cball] 
+    by (auto elim: has_contour_integral_eqpath[of _ _ "circlepath z \<epsilon>" "circlepath z r"])
+qed
+
+
+lemma residue_holo:
+  assumes "open s" "z \<in> s" and f_holo: "f holomorphic_on s"
+  shows "residue f z = 0"
+proof -
+  define c where "c \<equiv> 2 * pi * \<i>"
+  obtain e where "e>0" and e_cball:"cball z e \<subseteq> s" using \<open>open s\<close> \<open>z\<in>s\<close> 
+    using open_contains_cball_eq by blast
+  have "(f has_contour_integral c*residue f z) (circlepath z e)"
+    using f_holo
+    by (auto intro: base_residue[OF \<open>open s\<close> \<open>z\<in>s\<close> \<open>e>0\<close> _ e_cball,folded c_def])    
+  moreover have "(f has_contour_integral 0) (circlepath z e)" 
+    using f_holo e_cball \<open>e>0\<close>
+    by (auto intro: Cauchy_theorem_convex_simple[of _ "cball z e"])
+  ultimately have "c*residue f z =0"
+    using has_contour_integral_unique by blast
+  thus ?thesis unfolding c_def  by auto    
 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>open s\<close>] 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 \<open>finite pts\<close>,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 \<open>e2>0\<close> \<open>e1>0\<close> 
-    apply (rule_tac x="min e1 e2" in exI)
-    by auto
+
+lemma residue_const:"residue (\<lambda>_. c) z = 0"
+  by (intro residue_holo[of "UNIV::complex set"],auto intro:holomorphic_intros)
+
+
+lemma residue_add:
+  assumes "open s" "z \<in> s" and f_holo: "f holomorphic_on s - {z}" 
+      and g_holo:"g holomorphic_on s - {z}"
+  shows "residue (\<lambda>z. f z + g z) z= residue f z + residue g z"
+proof -
+  define c where "c \<equiv> 2 * pi * \<i>"
+  define fg where "fg \<equiv> (\<lambda>z. f z+g z)"
+  obtain e where "e>0" and e_cball:"cball z e \<subseteq> s" using \<open>open s\<close> \<open>z\<in>s\<close> 
+    using open_contains_cball_eq by blast
+  have "(fg has_contour_integral c * residue fg z) (circlepath z e)" 
+    unfolding fg_def using f_holo g_holo
+    apply (intro base_residue[OF \<open>open s\<close> \<open>z\<in>s\<close> \<open>e>0\<close> _ e_cball,folded c_def])
+    by (auto intro:holomorphic_intros)
+  moreover have "(fg has_contour_integral c*residue f z + c* residue g z) (circlepath z e)"
+    unfolding fg_def using f_holo g_holo
+    by (auto intro: has_contour_integral_add base_residue[OF \<open>open s\<close> \<open>z\<in>s\<close> \<open>e>0\<close> _ e_cball,folded c_def])      
+  ultimately have "c*(residue f z + residue g z) = c * residue fg z"
+    using has_contour_integral_unique by (auto simp add:distrib_left)
+  thus ?thesis unfolding fg_def 
+    by (auto simp add:c_def)
 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
-  define e2 where "e2 = e1/2"
-  have "e2>0" and "e2<e1" unfolding e2_def using \<open>e1>0\<close> 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 \<open>e2>0\<close> e1 by auto
+  
+lemma residue_lmul:
+  assumes "open s" "z \<in> s" and f_holo: "f holomorphic_on s - {z}" 
+  shows "residue (\<lambda>z. c * (f z)) z= c * residue f z"
+proof (cases "c=0")
+  case True
+  thus ?thesis using residue_const by auto
+next  
+  case False
+  def c'\<equiv>"2 * pi * \<i>"
+  def f'\<equiv>"(\<lambda>z. c * (f z))"
+  obtain e where "e>0" and e_cball:"cball z e \<subseteq> s" using \<open>open s\<close> \<open>z\<in>s\<close> 
+    using open_contains_cball_eq by blast
+  have "(f' has_contour_integral c' * residue f' z) (circlepath z e)"
+    unfolding f'_def using f_holo
+    apply (intro base_residue[OF \<open>open s\<close> \<open>z\<in>s\<close> \<open>e>0\<close> _ e_cball,folded c'_def])
+    by (auto intro:holomorphic_intros)
+  moreover have "(f' has_contour_integral c * (c' * residue f z)) (circlepath z e)"
+    unfolding f'_def using f_holo
+    by (auto intro: has_contour_integral_lmul 
+      base_residue[OF \<open>open s\<close> \<open>z\<in>s\<close> \<open>e>0\<close> _ e_cball,folded c'_def])    
+  ultimately have "c' * residue f' z  = c * (c' * residue f z)"
+    using has_contour_integral_unique by auto  
+  thus ?thesis unfolding f'_def c'_def using False
+    by (auto simp add:field_simps)
 qed
 
+lemma residue_rmul:
+  assumes "open s" "z \<in> s" and f_holo: "f holomorphic_on s - {z}" 
+  shows "residue (\<lambda>z. (f z) * c) z= residue f z * c"
+using residue_lmul[OF assms,of c] by (auto simp add:algebra_simps)
+
+lemma residue_div:
+  assumes "open s" "z \<in> s" and f_holo: "f holomorphic_on s - {z}" 
+  shows "residue (\<lambda>z. (f z) / c) z= residue f z / c "
+using residue_lmul[OF assms,of "1/c"] by (auto simp add:algebra_simps)
+
+lemma residue_neg:
+  assumes "open s" "z \<in> s" and f_holo: "f holomorphic_on s - {z}" 
+  shows "residue (\<lambda>z. - (f z)) z= - residue f z"
+using residue_lmul[OF assms,of "-1"] by auto
+
+lemma residue_diff:
+  assumes "open s" "z \<in> s" and f_holo: "f holomorphic_on s - {z}" 
+      and g_holo:"g holomorphic_on s - {z}"
+  shows "residue (\<lambda>z. f z - g z) z= residue f z - residue g z"
+using residue_add[OF assms(1,2,3),of "\<lambda>z. - g z"] residue_neg[OF assms(1,2,4)] 
+by (auto intro:holomorphic_intros g_holo)
+
+lemma residue_simple:
+  assumes "open s" "z\<in>s" and f_holo:"f holomorphic_on s"
+  shows "residue (\<lambda>w. f w / (w - z)) z = f z"
+proof -
+  define c where "c \<equiv> 2 * pi * \<i>"
+  def f'\<equiv>"\<lambda>w. f w / (w - z)"
+  obtain e where "e>0" and e_cball:"cball z e \<subseteq> s" using \<open>open s\<close> \<open>z\<in>s\<close> 
+    using open_contains_cball_eq by blast
+  have "(f' has_contour_integral c * f z) (circlepath z e)"
+    unfolding f'_def c_def using \<open>e>0\<close> f_holo e_cball
+    by (auto intro!: Cauchy_integral_circlepath_simple holomorphic_intros)
+  moreover have "(f' has_contour_integral c * residue f' z) (circlepath z e)"
+    unfolding f'_def using f_holo
+    apply (intro base_residue[OF \<open>open s\<close> \<open>z\<in>s\<close> \<open>e>0\<close> _ e_cball,folded c_def])
+    by (auto intro!:holomorphic_intros)
+  ultimately have "c * f z = c * residue f' z"
+    using has_contour_integral_unique by blast
+  thus ?thesis unfolding c_def f'_def  by auto
+qed
+
+
+
+subsubsection \<open>Cauchy's residue theorem\<close>
+
 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 \<open>finite pts\<close>]) print_cases
+proof (induct arbitrary:s thesis a rule:finite_induct[OF \<open>finite pts\<close>]) 
   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>open s\<close>,of a b ] \<open>connected (s - {})\<close>
@@ -2299,42 +2449,42 @@
 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>open s\<close> \<open>finite (insert p pts)\<close>,rule_format,of a]  
+    using finite_ball_avoid[OF \<open>open s\<close> \<open>finite (insert p pts)\<close>, of a]  
       \<open>a \<in> s - insert p pts\<close>
     by auto
-  define a' where "a' = a+e/2"
+  define a' where "a' \<equiv> a+e/2"
   have "a'\<in>s-{p} -pts"  using e[rule_format,of "a+e/2"] \<open>e>0\<close>  
     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)
-  define g where "g = linepath a a' +++ g'"
+  define g where "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 \<open>e>0\<close> 
-      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
+    proof (rule subset_path_image_join)
+      have "closed_segment a a' \<subseteq> ball a e" using \<open>e>0\<close> 
+        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 \<open>e>0\<close> 
-      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: \<open>e>0\<close>)
-  qed
+    proof -
+      have "closed_segment a a' \<subseteq> ball a e" using \<open>e>0\<close> 
+        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: \<open>e>0\<close>)
+    qed
   ultimately show ?case using idt.prems(1)[of g] by auto
 qed
 
@@ -2376,10 +2526,10 @@
   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)
-  define p_circ where "p_circ = circlepath p (h p)"
-  define p_circ_pt where "p_circ_pt = linepath (p+h p) (p+h p)"
-  define n_circ where "n_circ n = (op +++ p_circ ^^ n) p_circ_pt" for n
-  define cp where "cp = (if n\<ge>0 then reversepath (n_circ (nat n)) else n_circ (nat (- n)))"
+  define p_circ where "p_circ \<equiv> circlepath p (h p)" 
+  define p_circ_pt where "p_circ_pt \<equiv> linepath (p+h p) (p+h p)"
+  define n_circ where "n_circ \<equiv> \<lambda>n. (op +++ p_circ ^^ n) p_circ_pt"
+  define cp where "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" 
@@ -2467,7 +2617,7 @@
           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])
+            by (auto simp: valid_path_imp_path 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
@@ -2495,13 +2645,14 @@
         using n_circ(5)  by auto
     next
       show "winding_number cp p = - n" 
-        unfolding cp_def using winding_number_reversepath n_circ \<open>h p>0\<close> by auto
+        unfolding cp_def using winding_number_reversepath n_circ \<open>h p>0\<close> 
+        by (auto simp: valid_path_imp_path)
     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))
+        by (auto simp add: valid_path_imp_path 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
@@ -2510,7 +2661,7 @@
         unfolding cp_def using contour_integral_reversepath[OF n_circ(1)] n_circ(9)
         by auto
     qed
-  define g' where "g' = g +++ pg +++ cp +++ (reversepath pg)"
+  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 _ _ \<open>finite pts\<close> ]) 
       show "connected (s - {p} - pts)" using connected by (metis Diff_insert2)
@@ -2524,8 +2675,8 @@
         unfolding g'_def cp_def using pg(2) by simp
       show "path_image g' \<subseteq> s - {p} - pts" 
         proof -
-          define s' where "s' = s - {p} - pts"
-          have s': "s' = s-insert p pts " unfolding s'_def by auto
+          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')           
@@ -2539,9 +2690,10 @@
           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 \<open>valid_path g\<close> by simp
+              show "path g" using \<open>valid_path g\<close> by (simp add: valid_path_imp_path)
               show "z \<notin> path_image g" using z path_img by auto
-              show "path (pg +++ cp +++ reversepath pg)" using pg(3) cp by auto
+              show "path (pg +++ cp +++ reversepath pg)" using pg(3) cp 
+                by (simp add: valid_path_imp_path)
             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)
@@ -2553,7 +2705,8 @@
               + 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
+               and "pathfinish pg = pathstart (cp +++ reversepath pg)" 
+                by (auto simp add: valid_path_imp_path)
               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 
@@ -2561,12 +2714,12 @@
             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 (auto intro!:winding_number_join simp: valid_path_imp_path)
             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
+            apply (auto simp: valid_path_imp_path)
             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 .
@@ -2612,22 +2765,22 @@
       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 (simp_all add: valid_path_imp_path)
         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 (simp_all add: valid_path_imp_path)
         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
+        by (simp_all add: valid_path_imp_path)
       also have "... = winding_number g p' + winding_number cp p'"
         apply (subst winding_number_reversepath)
-        by auto
+        by (simp_all add: valid_path_imp_path)
       also have "... = winding_number g p'" using that by auto
       finally show ?thesis .
     qed
@@ -2637,9 +2790,8 @@
     by (auto simp add:setsum.insert[OF \<open>finite pts\<close> \<open>p\<notin>pts\<close>] algebra_simps)         
 qed  
 
-
 lemma Cauchy_theorem_singularities:
-  assumes "open s" "connected (s-pts)" "finite pts" and 
+  assumes "open s" "connected s" "finite pts" and 
           holo:"f holomorphic_on s-pts" and
           "valid_path g" and 
           loop:"pathfinish g = pathstart g" and
@@ -2649,15 +2801,17 @@
   shows "contour_integral g f = (\<Sum>p\<in>pts. winding_number g p * contour_integral (circlepath p (h p)) f)"
     (is "?L=?R")
 proof -
-  define circ
-    where [abs_def]: "circ p = winding_number g p * contour_integral (circlepath p (h p)) f" for p
-  define pts1 where "pts1 = pts \<inter> s" 
-  define pts2 where "pts2 = pts - pts1"
+  define circ where "circ \<equiv> \<lambda>p. winding_number g p * contour_integral (circlepath p (h p)) f"
+  define pts1 where "pts1 \<equiv> pts \<inter> s" 
+  define pts2 where "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>open s\<close> _ _ \<open>pts1\<subseteq>s\<close> _ \<open>valid_path g\<close> loop _ homo])
-      show "connected (s - pts1)" by (metis Diff_Int2 Int_absorb assms(2) pts1_def)
+      have "finite pts1" unfolding pts1_def using \<open>finite pts\<close> by auto
+      then show "connected (s - pts1)" 
+        using \<open>open s\<close> \<open>connected s\<close> connected_open_delete_finite[of s] by auto
+    next
       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 
@@ -2681,6 +2835,88 @@
     by auto
 qed
 
+lemma Residue_theorem:
+  fixes s pts::"complex set" and f::"complex \<Rightarrow> complex"
+    and g::"real \<Rightarrow> complex"
+  assumes "open s" "connected s" "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" 
+  shows "contour_integral g f = 2 * pi * \<i> *(\<Sum>p\<in>pts. winding_number g p * residue f p)"
+proof -
+  define c where "c \<equiv>  2 * pi * \<i>"
+  obtain h where 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))" 
+    using finite_cball_avoid[OF \<open>open s\<close> \<open>finite pts\<close>] by metis
+  have "contour_integral g f 
+      = (\<Sum>p\<in>pts. winding_number g p * contour_integral (circlepath p (h p)) f)"
+    using Cauchy_theorem_singularities[OF assms avoid] .
+  also have "... = (\<Sum>p\<in>pts.  c * winding_number g p * residue f p)"
+    proof (intro setsum.cong)
+      show "pts = pts" by simp
+    next
+      fix x assume "x \<in> pts" 
+      show "winding_number g x * contour_integral (circlepath x (h x)) f 
+          = c * winding_number g x * residue f x"   
+        proof (cases "x\<in>s")
+          case False
+          then have "winding_number g x=0" using homo by auto
+          thus ?thesis by auto
+        next
+          case True
+          have "contour_integral (circlepath x (h x)) f = c* residue f x"  
+            using \<open>x\<in>pts\<close> \<open>finite pts\<close> avoid[rule_format,OF True]
+            apply (intro base_residue[of "s-(pts-{x})",THEN contour_integral_unique,folded c_def])
+            by (auto intro:holomorphic_on_subset[OF holo] open_Diff[OF \<open>open s\<close> finite_imp_closed])
+          then show ?thesis by auto
+        qed
+    qed
+  also have "... = c * (\<Sum>p\<in>pts. winding_number g p * residue f p)"
+    by (simp add: setsum_right_distrib algebra_simps) 
+  finally show ?thesis unfolding c_def .
+qed    
+
+subsection \<open>The argument principle\<close>
+
+definition is_pole :: "('a::topological_space \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> 'a \<Rightarrow> bool" where
+  "is_pole f a =  (LIM x (at a). f x :> at_infinity)"
+
+lemma is_pole_tendsto:
+  fixes f::"('a::topological_space \<Rightarrow> 'b::real_normed_div_algebra)"
+  shows "is_pole f x \<Longrightarrow> ((inverse o f) \<longlongrightarrow> 0) (at x)"
+unfolding is_pole_def 
+by (auto simp add:filterlim_inverse_at_iff[symmetric] comp_def filterlim_at)
+
+lemma is_pole_inverse_holomorphic:
+  assumes "open s"
+    and f_holo:"f holomorphic_on (s-{z})" 
+    and pole:"is_pole f z" 
+    and non_z:"\<forall>x\<in>s-{z}. f x\<noteq>0"
+  shows "(\<lambda>x. if x=z then 0 else inverse (f x)) holomorphic_on s"
+proof -
+  define g where "g \<equiv> \<lambda>x. if x=z then 0 else inverse (f x)"
+  have "isCont g z" unfolding isCont_def  using is_pole_tendsto[OF pole]
+    apply (subst Lim_cong_at[where b=z and y=0 and g="inverse \<circ> f"])
+    by (simp_all add:g_def)
+  moreover have "continuous_on (s-{z}) f" using f_holo holomorphic_on_imp_continuous_on by auto
+  hence "continuous_on (s-{z}) (inverse o f)" unfolding comp_def
+    by (auto elim!:continuous_on_inverse simp add:non_z)
+  hence "continuous_on (s-{z}) g" unfolding g_def    
+    apply (subst continuous_on_cong[where t="s-{z}" and g="inverse o f"])
+    by auto
+  ultimately have "continuous_on s g" using open_delete[OF \<open>open s\<close>] \<open>open s\<close>
+    by (auto simp add:continuous_on_eq_continuous_at)
+  moreover have "(inverse o f) holomorphic_on (s-{z})"
+    unfolding comp_def using f_holo
+    by (auto elim!:holomorphic_on_inverse simp add:non_z)
+  hence "g holomorphic_on (s-{z})"
+    apply (subst holomorphic_cong[where t="s-{z}" and g="inverse o f"])
+    by (auto simp add:g_def)
+  ultimately show ?thesis unfolding g_def using \<open>open s\<close>
+    by (auto elim!: no_isolated_singularity)    
+qed
+
 
 (*order of the zero of f at z*)
 definition zorder::"(complex \<Rightarrow> complex) \<Rightarrow> complex \<Rightarrow> nat" where
@@ -2693,17 +2929,126 @@
 
 (*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"
+  "porder f z = (let f'=(\<lambda>x. if x=z then 0 else inverse (f x)) in zorder 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"
+  "pol_poly f z = (let f'=(\<lambda> x. if x=z then 0 else inverse (f x)) 
+      in inverse o zer_poly 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))"
+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 _ \<open>r>0\<close>, 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 \<open>n>m\<close> 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
+          define F where "F \<equiv> at z within ball z r"
+          define f' where "f' \<equiv> \<lambda>x. (x - z) ^ (n-m)"
+          have "f' z=0" using \<open>n>m\<close> 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] \<open>r>0\<close>
+            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 \<open>r>0\<close>) 
+      moreover have "at z within ball z r \<noteq> bot" using \<open>r>0\<close> 
+        by (auto simp add:trivial_limit_within islimpt_ball)
+      ultimately have "h z=0" by (auto intro: tendsto_unique)
+      thus False using asm \<open>r>0\<close> 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 _ \<open>r>0\<close>, 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 \<open>m>n\<close> 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
+          define F where "F \<equiv> at z within ball z r"
+          define f' where "f' \<equiv>\<lambda>x. (x - z) ^ (m-n)"
+          have "f' z=0" using \<open>m>n\<close> 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] \<open>r>0\<close>
+            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 \<open>r>0\<close>) 
+      moreover have "at z within ball z r \<noteq> bot" using \<open>r>0\<close> 
+        by (auto simp add:trivial_limit_within islimpt_ball)
+      ultimately have "g z=0" by (auto intro: tendsto_unique)
+      thus False using asm \<open>r>0\<close> by auto
+    qed
+  ultimately show "n=m" by fastforce
+qed
 
-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 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>open s\<close> \<open>connected s\<close> \<open>z\<in>s\<close> \<open>f z=0\<close>]
+    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 \<open>ball z r \<subseteq> s\<close> by auto
+  moreover have "r'>0" unfolding r'_def using \<open>0<r\<close> 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:\<open>0 < n\<close>)
+next
+  fix m n 
+  define fac where "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
+  define r where "r \<equiv> min r1 r2"
+  have "r>0" using \<open>r1>0\<close> \<open>r2>0\<close> 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 zorder_exist:  
   fixes f::"complex \<Rightarrow> complex" and z::complex
@@ -2714,8 +3059,8 @@
   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 -
-  define P where "P h r n \<longleftrightarrow> 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)" for h r n
+  define P where "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"
@@ -2739,7 +3084,7 @@
   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
-  define r3 where "r3 = min r1 r2"
+  define r3 where "r3 \<equiv> min r1 r2"
   have "P h r3 n" using \<open>P h r1 n\<close> \<open>r2>0\<close> unfolding P_def r3_def
     by auto
   moreover have "cball z r3 \<subseteq> s" using \<open>cball z r2 \<subseteq> s\<close> unfolding r3_def by auto
@@ -2748,279 +3093,185 @@
 
 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"
+  defines "n \<equiv> porder f z" and "h \<equiv> pol_poly f z"
+  assumes "open s" "z \<in> s" 
+    and holo:"f holomorphic_on s-{z}"
+    and "is_pole f z"
   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)"
+    \<and> (\<forall>w\<in>cball z r. (w\<noteq>z \<longrightarrow> f w  = h w / (w-z)^n) \<and> h w \<noteq>0)"
 proof -
-  define zo where "zo = zorder (inverse \<circ> f) z"
-  define zp where "zp = 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>open s\<close> \<open>connected s\<close> \<open>z\<in>s\<close> holo,folded zo_def zp_def] 
-      \<open>f z=0\<close> \<open>\<exists>w\<in>s. f w\<noteq>0\<close>
+  obtain e where "e>0" and e_ball:"ball z e \<subseteq> s"and e_def: "\<forall>x\<in>ball z e-{z}. f x\<noteq>0"
+    proof - 
+      have "\<forall>\<^sub>F z in at z. f z \<noteq> 0" 
+        using \<open>is_pole f z\<close> filterlim_at_infinity_imp_eventually_ne unfolding is_pole_def  
+        by auto
+      then obtain e1 where "e1>0" and e1_def: "\<forall>x. x \<noteq> z \<and> dist x z < e1 \<longrightarrow> f x \<noteq> 0"
+        using eventually_at[of "\<lambda>x. f x\<noteq>0" z,simplified] by auto
+      obtain e2 where "e2>0" and "ball z e2 \<subseteq>s" using \<open>open s\<close> \<open>z\<in>s\<close> openE by auto
+      define e where "e \<equiv> min e1 e2"
+      have "e>0" using \<open>e1>0\<close> \<open>e2>0\<close> unfolding e_def by auto
+      moreover have "ball z e \<subseteq> s" unfolding e_def using \<open>ball z e2 \<subseteq> s\<close> by auto 
+      moreover have "\<forall>x\<in>ball z e-{z}. f x\<noteq>0" using e1_def \<open>e1>0\<close> \<open>e2>0\<close> unfolding e_def 
+        by (simp add: DiffD1 DiffD2 dist_commute singletonI)
+      ultimately show ?thesis using that by auto
+    qed
+  define g where "g \<equiv> \<lambda>x. if x=z then 0 else inverse (f x)"
+  define zo where "zo \<equiv> zorder g z" 
+  define zp where "zp \<equiv> zer_poly g z" 
+  have "\<exists>w\<in>ball z e. g w \<noteq> 0" 
+    proof -
+      obtain w where w:"w\<in>ball z e-{z}" using \<open>0 < e\<close>
+        by (metis open_ball all_not_in_conv centre_in_ball insert_Diff_single 
+          insert_absorb not_open_singleton)
+      hence "w\<noteq>z" "f w\<noteq>0" using e_def[rule_format,of w] mem_ball
+        by (auto simp add:dist_commute)
+      then show ?thesis unfolding g_def using w by auto
+    qed
+  moreover have "g holomorphic_on ball z e" 
+    apply (intro is_pole_inverse_holomorphic[of "ball z e",OF _ _ \<open>is_pole f z\<close> e_def,folded g_def])
+    using holo e_ball by auto
+  moreover have "g z=0" unfolding g_def by auto
+  ultimately obtain r where "0 < zo" "0 < r" "cball z r \<subseteq> ball z e" 
+      and zp_holo: "zp holomorphic_on cball z r" and
+      zp_fac: "\<forall>w\<in>cball z r. g w = zp w * (w - z) ^ zo \<and> zp w \<noteq> 0"
+    using zorder_exist[of "ball z e" z g,simplified,folded zo_def zp_def] \<open>e>0\<close> 
     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
+    unfolding n_def zo_def porder_def h_def zp_def pol_poly_def g_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
+  moreover have "\<forall>w\<in>cball z r. (w\<noteq>z \<longrightarrow> f w  = h w / (w-z)^n) \<and> h w \<noteq>0"
+    using zp_fac unfolding h n comp_def g_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 \<open>zo>0\<close> by simp
-  ultimately show ?thesis using \<open>0 < r\<close> \<open>cball z r \<subseteq> s\<close> 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 -
-  define n where "n = porder f z"
-  define h where "h = 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>open s\<close> \<open>connected s\<close> \<open>z\<in>s\<close> holo \<open>f z=0\<close> non_c]
-    unfolding n_def h_def by auto
-  define c where "c = 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 \<open>n>0\<close>],folded c_def] h_holo r_b
-    by (auto simp add:\<open>r>0\<close> 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 \<open>r>0\<close> \<open>cball z r \<subseteq> s\<close> unfolding c_def by auto
+  ultimately show ?thesis using \<open>0 < r\<close> \<open>cball z r \<subseteq> ball z e\<close> e_ball 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)"
+lemma residue_porder:
+  fixes f::"complex \<Rightarrow> complex" and z::complex
+  defines "n \<equiv> porder f z" and "h \<equiv> pol_poly f z"
+  assumes "open s" "z \<in> s" 
+    and holo:"f holomorphic_on s - {z}"
+    and pole:"is_pole f z"
+  shows "residue f z = ((deriv ^^ (n - 1)) h z / fact (n-1))"
 proof -
-  define pts where "pts = {p. f p=0}"
-  define c where "c = 2 * complex_of_real pi * \<i> "
-  define contour
-    where "contour p e = (f has_contour_integral c * residue f p) (circlepath p e)" for p e
-  define avoid where "avoid p e \<longleftrightarrow> (\<forall>w\<in>cball p e. w \<in> s \<and> (w \<noteq> p \<longrightarrow> w \<notin> pts))" for p e
-  have "poles \<subseteq> pts" and "finite pts"
-    using poles \<open>finite {p. f p=0}\<close> 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>open s\<close> \<open>finite pts\<close>] \<open>p\<in>s\<close> 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 \<open>e1>0\<close>])
-        show "inverse \<circ> f holomorphic_on ball p e1"
-        proof -
-          define f' where "f' = inverse o f"
-          have "f holomorphic_on ball p e1 - {p}" 
-            using holo e \<open>poles \<subseteq> pts\<close> 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 \<open>p\<in>poles\<close> 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 \<open>p\<in>poles\<close> poles unfolding is_pole_def by auto
-      next
-        define p' where "p' = p+e1/2"
-        have "p'\<in>ball p e1" and "p'\<noteq>p" using \<open>e1>0\<close> 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
-      define e3 where "e3 = (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 \<open>e1>0\<close> 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
-  define cont where "cont p = contour_integral (circlepath p (h p)) f" for p
-  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>open s\<close> \<open>connected (s-poles)\<close> _ holo \<open>valid_path \<gamma>\<close> 
-      loop \<open>path_image \<gamma> \<subseteq> s-poles\<close> homo])
-    show "finite poles" using \<open>poles \<subseteq> pts\<close> and \<open>finite pts\<close> 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   \<open>poles \<subseteq> pts\<close> 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] \<open>p \<in> poles\<close> 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
+  define g where "g \<equiv> \<lambda>x. if x=z then 0 else inverse (f x)"
+  obtain r where "0 < n" "0 < r" and r_cball:"cball z r \<subseteq> s" and h_holo: "h holomorphic_on cball z r" 
+      and h_divide:"(\<forall>w\<in>cball z r. (w\<noteq>z \<longrightarrow> f w = h w / (w - z) ^ n) \<and> h w \<noteq> 0)"
+    using porder_exist[OF \<open>open s\<close> \<open>z \<in> s\<close> holo pole, folded n_def h_def] by blast
+  have r_nonzero:"\<And>w. w \<in> ball z r - {z} \<Longrightarrow> f w \<noteq> 0"
+    using h_divide by simp
+  define c where "c \<equiv> 2 * pi * \<i>"
+  define der_f where "der_f \<equiv> ((deriv ^^ (n - 1)) h z / fact (n-1))"
+  def h'\<equiv>"\<lambda>u. h u / (u - z) ^ n"
+  have "(h' has_contour_integral c / fact (n - 1) * (deriv ^^ (n - 1)) h z) (circlepath z r)" 
+    unfolding h'_def
+    proof (rule Cauchy_has_contour_integral_higher_derivative_circlepath[of z r h z "n-1",
+        folded c_def Suc_pred'[OF \<open>n>0\<close>]])
+      show "continuous_on (cball z r) h" using holomorphic_on_imp_continuous_on h_holo by simp
+      show "h holomorphic_on ball z r" using h_holo by auto
+      show " z \<in> ball z r" using \<open>r>0\<close> 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   
+  then have "(h' has_contour_integral c * der_f) (circlepath z r)" unfolding der_f_def by auto
+  then have "(f has_contour_integral c * der_f) (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 - {z}" using \<open>r>0\<close> by auto
+      then show "h' x = f x" using h_divide unfolding h'_def by auto
+    qed
+  moreover have "(f has_contour_integral c * residue f z) (circlepath z r)"
+    using base_residue[OF \<open>open s\<close> \<open>z\<in>s\<close> \<open>r>0\<close> holo r_cball,folded c_def] .
+  ultimately have "c * der_f =  c * residue f z" using has_contour_integral_unique by blast
+  hence "der_f = residue f z" unfolding c_def by auto
+  thus ?thesis unfolding der_f_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"
+  defines "zeros\<equiv>{p. f p=0} - poles"
   assumes "open s" and 
-          connected:"connected (s- pts)" and 
+          "connected s" 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
+          path_img:"path_image g \<subseteq> s - (zeros \<union> poles)" and
           homo:"\<forall>z. (z \<notin> s) \<longrightarrow> winding_number g z = 0" and
-          finite:"finite pts" and
+          finite:"finite (zeros \<union> poles)" 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 -
-  define c where "c = 2 * complex_of_real pi * \<i> "
-  define ff where [abs_def]: "ff x = deriv f x * h x / f x" for x
-  define cont_pole where "cont_pole ff p e \<longleftrightarrow>
-    (ff has_contour_integral - c  * porder f p * h p) (circlepath p e)" for ff p e
-  define cont_zero where "cont_zero ff p e \<longleftrightarrow>
-    (ff has_contour_integral c * zorder f p * h p ) (circlepath p e)" for ff p e
-  define avoid where "avoid p e \<longleftrightarrow> (\<forall>w\<in>cball p e. w \<in> s \<and> (w \<noteq> p \<longrightarrow> w \<notin> pts))" for p e
-  have "poles \<subseteq> pts" and "zeros \<subseteq> pts" and "finite zeros" and "pts=zeros \<union> poles"
-    using poles \<open>finite pts\<close> unfolding pts_def zeros_def is_pole_def by auto
+  define c where "c \<equiv> 2 * complex_of_real pi * \<i> "
+  define ff where "ff \<equiv> (\<lambda>x. deriv f x * h x / f x)"
+  define cont_pole where "cont_pole \<equiv> \<lambda>ff p e. (ff has_contour_integral - c  * porder f p * h p) (circlepath p e)"
+  define cont_zero where "cont_zero \<equiv> \<lambda>ff p e. (ff has_contour_integral c * zorder f p * h p ) (circlepath p e)"
+  define avoid where "avoid \<equiv> \<lambda>p e. \<forall>w\<in>cball p e. w \<in> s \<and> (w \<noteq> p \<longrightarrow> w \<notin> zeros \<union> poles)"
   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>open s\<close> \<open>finite pts\<close>] \<open>p\<in>s\<close> unfolding avoid_def by auto
+      obtain e1 where "e1>0" and e1_avoid:"avoid p e1"
+        using finite_cball_avoid[OF \<open>open s\<close> finite] \<open>p\<in>s\<close> 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 - 
-          define po where "po = porder f p"
-          define pp where "pp = pol_poly f p"
-          define f' where [abs_def]: "f' w = pp w / (w - p) ^ po" for w
-          define ff' where [abs_def]: "ff' x = deriv f' x * h x / f' x" for x
-          have "inverse \<circ> f holomorphic_on ball p e1" 
-            proof -
-              have "f holomorphic_on ball p e1 - {p}" 
-                using f_holo e \<open>poles \<subseteq> pts\<close> 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 \<open>p\<in>poles\<close> 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 \<open>p\<in>poles\<close> poles unfolding is_pole_def by auto
-          moreover have "\<exists>w\<in>ball p e1. f w \<noteq> 0" 
-            proof -
-              define p' where "p' = p+e1/2"
-              have "p'\<in>ball p e1" and "p'\<noteq>p" using \<open>e1>0\<close> 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 
+          define po where "po \<equiv> porder f p"
+          define pp where "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 "f holomorphic_on ball p e1 - {p}" 
+            apply (intro holomorphic_on_subset[OF f_holo])
+            using e1_avoid \<open>p\<in>poles\<close> unfolding avoid_def by auto
+          then 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 \<open>e1>0\<close>] unfolding po_def pp_def
+              pp_po:"(\<forall>w\<in>cball p r. (w\<noteq>p \<longrightarrow> f w = pp w / (w - p) ^ po) \<and> pp w \<noteq> 0)"
+            using porder_exist[of "ball p e1" p f,simplified,OF \<open>e1>0\<close>] poles \<open>p\<in>poles\<close>
+            unfolding po_def pp_def 
             by auto    
-          define e2 where "e2 = r/2"
+          define e2 where "e2 \<equiv> r/2"
           have "e2>0" using \<open>r>0\<close> unfolding e2_def by auto
-          define anal where [abs_def]: "anal w = deriv pp w * h w / pp w" for w
-          define prin where [abs_def]: "prin w = - of_nat po * h w / (w - p)" for w
+          define anal where "anal \<equiv> \<lambda>w. deriv pp w * h w / pp w" 
+          define prin where "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 \<open>r>0\<close> 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"]
-                \<open>e2>0\<close>
-              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 \<open>ball p r \<subseteq> s\<close>
-              by (auto intro!: holomorphic_intros)
-            then show "(anal has_contour_integral 0) (circlepath p e2)"
-              using e2_def \<open>r>0\<close>
-              by (auto elim!: Cauchy_theorem_disc_simple)
-          qed
+            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 e1_avoid by blast
+              then have "cball p e2 \<subseteq> s"
+                using \<open>r>0\<close> 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"]
+                  \<open>e2>0\<close>
+                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 \<open>ball p r \<subseteq> s\<close>
+                by (auto intro!: holomorphic_intros)
+              then show "(anal has_contour_integral 0) (circlepath p e2)"
+                using e2_def \<open>r>0\<close>
+                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 \<open>r>0\<close> by auto
-              define wp where "wp = w-p"
+              define wp where "wp \<equiv> w-p"
               have "wp\<noteq>0" and "pp w \<noteq>0" 
                 unfolding wp_def using \<open>w\<noteq>p\<close> \<open>w\<in>ball p r\<close> 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)
-                  define der where "der = - po * pp w / (w-p)^(po+1) + deriv pp w / (w-p)^po"
+                  define der where "der \<equiv> - po * pp w / (w-p)^(po+1) + deriv pp w / (w-p)^po"
                   have po:"po = Suc (po - Suc 0) " using \<open>po>0\<close> by auto
                   have "(pp has_field_derivative (deriv pp w)) (at w)" 
-                    using DERIV_deriv_iff_field_differentiable \<open>w\<in>ball p r\<close>
-                          holomorphic_on_imp_differentiable_at[of _ "ball p r"] 
-                          holomorphic_on_subset [OF pp_holo ball_subset_cball]
-                    by (metis open_ball)
+                    using DERIV_deriv_iff_has_field_derivative pp_holo \<open>w\<noteq>p\<close> 
+                      by (meson open_ball \<open>w \<in> ball p r\<close> ball_subset_cball holomorphic_derivI holomorphic_on_subset)
                   then show "(f' has_field_derivative  der) (at w)" 
                     using \<open>w\<noteq>p\<close> \<open>po>0\<close> unfolding der_def f'_def
                     apply (auto intro!: derivative_eq_intros simp add:field_simps)
@@ -3040,27 +3291,29 @@
               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 \<open>r>0\<close> 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 \<open>cball p r \<subseteq> ball p e1\<close>
-                  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 \<open>w\<in>ball p r\<close> \<open>w\<noteq>p\<close> 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
+                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 e1_avoid
+                    by auto
+                  then have "ball p r - {p} \<subseteq> s - poles" using \<open>cball p r \<subseteq> ball p e1\<close>
+                    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 \<open>w\<in>ball p r\<close> \<open>w\<noteq>p\<close> 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
+                using \<open>w \<in> ball p r\<close> ball_subset_cball subset_iff pp_po \<open>w\<noteq>p\<close> 
+                unfolding f'_def by auto
               ultimately show "ff' w = ff w"
                 unfolding ff'_def ff_def by simp
             qed
@@ -3073,27 +3326,26 @@
       have "\<exists>e3>0. cball p e3 \<subseteq> ball p e1 \<and> cont_zero ff p e3"
         when "p\<in>zeros"
         proof -
-          define zo where "zo = zorder f p"
-          define zp where "zp = zer_poly f p"
-          define f' where [abs_def]: "f' w = zp w * (w - p) ^ zo" for w
-          define ff' where [abs_def]: "ff' x = deriv f' x * h x / f' x" for x
+          define zo where "zo \<equiv> zorder f p"
+          define zp where "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
+            proof -
+              have "ball p e1 \<subseteq> s - poles" 
+                using avoid_def ball_subset_cball e1_avoid that zeros_def by fastforce
+              thus ?thesis using f_holo by auto
+            qed
           moreover have "f p = 0" using \<open>p\<in>zeros\<close> 
-            using DiffD1 mem_Collect_eq pts_def zeros_def by blast
+            using DiffD1 mem_Collect_eq zeros_def by blast
           moreover have "\<exists>w\<in>ball p e1. f w \<noteq> 0" 
-          proof -
-            define p' where "p' = p+e1/2"
-            have "p'\<in>ball p e1" and "p'\<noteq>p"
-              using \<open>e1>0\<close> 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
+            proof -
+              def p'\<equiv>"p+e1/2"
+              have "p'\<in>ball p e1" and "p'\<noteq>p" using \<open>e1>0\<close> unfolding p'_def by (auto simp add:dist_norm)
+              then show "\<exists>w\<in>ball p e1. f w \<noteq> 0" using e1_avoid unfolding avoid_def
+                apply (rule_tac x=p' in bexI)
+                by (auto simp add:zeros_def)
+            qed
           ultimately obtain r where 
               "0 < zo" "r>0"
               "cball p r \<subseteq> ball p e1" and
@@ -3101,59 +3353,57 @@
               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 \<open>e1>0\<close>] unfolding zo_def zp_def
             by auto    
-          define e2 where "e2 = r/2"
+          define e2 where "e2 \<equiv> r/2"
           have "e2>0" using \<open>r>0\<close> unfolding e2_def by auto
-          define anal where [abs_def]: "anal w = deriv zp w * h w / zp w" for w
-          define prin where [abs_def]: "prin w = of_nat zo * h w / (w - p)" for w
+          define anal where "anal \<equiv> \<lambda>w. deriv zp w * h w / zp w" 
+          define prin where "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 \<open>r>0\<close> 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"]
-                \<open>e2>0\<close>
-              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 \<open>ball p r \<subseteq> s\<close>
-              by (auto intro!: holomorphic_intros)
-            then show "(anal has_contour_integral 0) (circlepath p e2)"
-              using e2_def \<open>r>0\<close>
-              by (auto elim!: Cauchy_theorem_disc_simple)
-          qed
+            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 e1_avoid by blast
+              then have "cball p e2 \<subseteq> s"
+                using \<open>r>0\<close> 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"]
+                  \<open>e2>0\<close>
+                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 \<open>ball p r \<subseteq> s\<close>
+                by (auto intro!: holomorphic_intros)
+              then show "(anal has_contour_integral 0) (circlepath p e2)"
+                using e2_def \<open>r>0\<close>
+                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 \<open>r>0\<close> by auto
-            define wp where "wp = w-p"
-            have "wp\<noteq>0" and "zp w \<noteq>0" 
-              unfolding wp_def using \<open>w\<noteq>p\<close> \<open>w\<in>ball p r\<close> 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)
-                define der where "der = zo * zp w * (w-p)^(zo-1) + deriv zp w * (w-p)^zo"
-                have po:"zo = Suc (zo - Suc 0) " using \<open>zo>0\<close> by auto
-                have "(zp has_field_derivative (deriv zp w)) (at w)" 
-                  using DERIV_deriv_iff_field_differentiable \<open>w\<in>ball p r\<close>
-                        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 \<open>w\<noteq>p\<close> \<open>zo>0\<close> 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
+            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 \<open>r>0\<close> by auto
+              define wp where "wp \<equiv> w-p"
+              have "wp\<noteq>0" and "zp w \<noteq>0" 
+                unfolding wp_def using \<open>w\<noteq>p\<close> \<open>w\<in>ball p r\<close> 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)
+                  define der where "der \<equiv> zo * zp w * (w-p)^(zo-1) + deriv zp w * (w-p)^zo"
+                  have po:"zo = Suc (zo - Suc 0) " using \<open>zo>0\<close> by auto
+                  have "(zp has_field_derivative (deriv zp w)) (at w)" 
+                    using DERIV_deriv_iff_has_field_derivative pp_holo
+                    by (meson Topology_Euclidean_Space.open_ball \<open>w \<in> ball p r\<close> ball_subset_cball holomorphic_derivI holomorphic_on_subset)
+                  then show "(f' has_field_derivative  der) (at w)" 
+                    using \<open>w\<noteq>p\<close> \<open>zo>0\<close> 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)"
@@ -3164,7 +3414,7 @@
                     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
+                    using avoid_def ball_subset_cball e1_avoid by auto
                   then have "ball p r - {p} \<subseteq> s - poles" using \<open>cball p r \<subseteq> ball p e1\<close>
                     using ball_subset_cball by blast
                   then show "f holomorphic_on ball p r - {p}" using f_holo
@@ -3189,31 +3439,31 @@
         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          
-      define e4 where "e4 = (if p\<in>poles then e2 else if p\<in>zeros then e3 else e1)"
+      define e4 where "e4 \<equiv> if p\<in>poles then e2 else if p\<in>zeros then e3 else e1"
       have "e4>0" using e2 e3 \<open>e1>0\<close> unfolding e4_def by auto
-      moreover have "avoid p e4" using e2 e3 \<open>e1>0\<close> e unfolding e4_def avoid_def by auto
+      moreover have "avoid p e4" using e2 e3 \<open>e1>0\<close> e1_avoid 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)
+        by (auto simp add: e2 e3 e4_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
-  define cont where "cont p = contour_integral (circlepath p (get_e p)) ff" for p
-  define w where "w p = winding_number g p" for p
-  have "contour_integral g ff = (\<Sum>p\<in>pts. w p * cont p)"
+  define cont where "cont \<equiv> \<lambda>p. contour_integral (circlepath p (get_e p)) ff"
+  define w where "w \<equiv> \<lambda>p. winding_number g p"
+  have "contour_integral g ff = (\<Sum>p\<in>zeros \<union> poles. w p * cont p)"
     unfolding cont_def w_def
-  proof (rule Cauchy_theorem_singularities[OF \<open>open s\<close> connected finite _ \<open>valid_path g\<close> loop 
-      path_img homo])
-    have "open (s - pts)" using open_Diff[OF _ finite_imp_closed[OF finite]] \<open>open s\<close> by auto 
-    then show "ff holomorphic_on s - pts" unfolding ff_def using f_holo \<open>poles \<subseteq> pts\<close> 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
+    proof (rule Cauchy_theorem_singularities[OF \<open>open s\<close> \<open>connected s\<close> finite _ \<open>valid_path g\<close> loop 
+        path_img homo])
+      have "open (s - (zeros \<union> poles))" using open_Diff[OF _ finite_imp_closed[OF finite]] \<open>open s\<close> by auto 
+      then show "ff holomorphic_on s - (zeros \<union> poles)" unfolding ff_def using f_holo h_holo
+        by (auto intro!: holomorphic_intros simp add:zeros_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> zeros \<union> poles))"
+        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 \<open>finite pts\<close> unfolding \<open>pts=zeros \<union> poles\<close>
+    using finite 
     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))"
@@ -3263,27 +3513,14 @@
   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>open s\<close> \<open>x\<in>s\<close>] 
-    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
+subsection \<open>Rouche's theorem \<close>
 
 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 
+    "open s" and "connected s" and 
     "finite zeros_fg" and 
     "finite zeros_f" and
     f_holo:"f holomorphic_on s" and 
@@ -3317,9 +3554,9 @@
         qed
       then show ?thesis unfolding zeros_f_def using path_img by auto 
     qed
-  define w where "w p = winding_number \<gamma> p" for p
-  define c where "c = 2 * complex_of_real pi * \<i>"
-  define h where [abs_def]: "h p = g p / f p + 1"  for p
+  define w where "w \<equiv> \<lambda>p. winding_number \<gamma> p"
+  define c where "c \<equiv> 2 * complex_of_real pi * \<i>"
+  define h where "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 \<open>valid_path \<gamma>\<close>
@@ -3339,9 +3576,7 @@
             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
+            using  convex_in_outside[of "ball 1 1" 0] outside_mono by blast
         qed
       have valid_h:"valid_path (h \<circ> \<gamma>)"
         proof (rule valid_path_compose_holomorphic[OF \<open>valid_path \<gamma>\<close> _ _ path_f])
@@ -3362,7 +3597,7 @@
             proof -
               have "0 \<in> outside (path_image (h \<circ> \<gamma>))" using outside_img .
               moreover have "path (h o \<gamma>)" 
-                using valid_h by auto
+                using valid_h  by (simp add: valid_path_imp_path)
               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
@@ -3374,17 +3609,15 @@
         proof (rule vector_derivative_chain_at_general)
           show "\<gamma> differentiable at x" using that \<open>valid_path \<gamma>\<close> spikes by auto
         next
-          define der where "der p = (deriv g p * f p - g p * deriv f p)/(f p * f p)" for p
-          define t where "t = \<gamma> x"
+          define der where "der \<equiv> \<lambda>p. (deriv g p * f p - g p * deriv f p)/(f p * f p)"
+          define t where "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>open s\<close>])
+            unfolding h_def der_def using g_holo f_holo \<open>open s\<close>
+            by (auto intro!: holomorphic_derivI derivative_eq_intros )
           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>) 
@@ -3420,29 +3653,27 @@
           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
+            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>open s\<close>] path_img that
-            by (auto intro!: deriv_add)
+            by auto
           have der_h:"deriv h p = (deriv g p * f p - g p * deriv f p)/(f p * f p)"
-          proof -
-            define der where "der p = (deriv g p * f p - g p * deriv f p)/(f p * f p)" for 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 \<open>f p\<noteq>0\<close>
-              apply (auto intro!: derivative_eq_intros)
-              by (auto simp add: DERIV_deriv_iff_field_differentiable 
-                  holomorphic_on_imp_differentiable_at[OF _ \<open>open s\<close>])
-            then show ?thesis unfolding der_def using DERIV_imp_deriv by auto
-          qed
+            proof -
+              define der where "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 \<open>open s\<close> \<open>f p\<noteq>0\<close>
+                by (auto intro!: derivative_eq_intros holomorphic_derivI)
+              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 \<open>h p\<noteq>0\<close> \<open>f p\<noteq>0\<close> \<open>fg p\<noteq>0\<close>)
@@ -3455,21 +3686,21 @@
     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>open s\<close> _ _ _ \<open>valid_path \<gamma>\<close> loop _ homo, of _ "{}" "\<lambda>_. 1",simplified])
-      show "connected (s - {p. fg p = 0})" using connected_fg unfolding zeros_fg_def .
+    proof (rule argument_principle[OF \<open>open s\<close> \<open>connected s\<close> _ _ \<open>valid_path \<gamma>\<close> loop _ homo
+        , of _ "{}" "\<lambda>_. 1",simplified])
       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 \<open>finite zeros_fg\<close> 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>open s\<close> _ _ _ \<open>valid_path \<gamma>\<close> loop _ homo, of _ "{}" "\<lambda>_. 1",simplified])
-      show "connected (s - {p. f p = 0})" using connected_f unfolding zeros_f_def .
+    proof (rule argument_principle[OF \<open>open s\<close> \<open>connected s\<close> _ _ \<open>valid_path \<gamma>\<close> loop _ homo
+        , of _ "{}" "\<lambda>_. 1",simplified])
       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 \<open>finite zeros_f\<close> unfolding zeros_f_def .
+      show " finite {p. f p = 0}" using \<open>finite zeros_f\<close> 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))"
+  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
diff -r 6a131df8e3d9 -r 82df5181d699 src/HOL/Multivariate_Analysis/Path_Connected.thy
--- a/src/HOL/Multivariate_Analysis/Path_Connected.thy	Wed May 25 13:13:35 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Path_Connected.thy	Wed May 25 16:38:35 2016 +0100
@@ -2073,10 +2073,26 @@
    "2 \<le> DIM('N::euclidean_space) \<Longrightarrow> path_connected(ball a r - {a::'N})"
 by (simp add: path_connected_open_delete)
 
-lemma connected_punctured_ball:
+corollary connected_punctured_ball:
    "2 \<le> DIM('N::euclidean_space) \<Longrightarrow> connected(ball a r - {a::'N})"
 by (simp add: connected_open_delete)
 
+corollary connected_open_delete_finite:
+  fixes S T::"'a::euclidean_space set"
+  assumes S: "open S" "connected S" and 2: "2 \<le> DIM('a)" and "finite T"
+  shows "connected(S - T)" 
+  using \<open>finite T\<close> S 
+proof (induct T)
+  case empty
+  show ?case using \<open>connected S\<close> by simp
+next
+  case (insert x F)
+  then have "connected (S-F)" by auto
+  moreover have "open (S - F)" using finite_imp_closed[OF \<open>finite F\<close>] \<open>open S\<close> by auto
+  ultimately have "connected (S - F - {x})" using connected_open_delete[OF _ _ 2] by auto
+  thus ?case by (metis Diff_insert)
+qed
+
 subsection\<open>Relations between components and path components\<close>
 
 lemma open_connected_component:
diff -r 6a131df8e3d9 -r 82df5181d699 src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Wed May 25 13:13:35 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Wed May 25 16:38:35 2016 +0100
@@ -9253,6 +9253,34 @@
   shows "cball x d = ball y e \<longleftrightarrow> d < 0 \<and> e \<le> 0"
   using ball_eq_cball_iff by blast
 
+lemma finite_ball_avoid:
+  fixes S :: "'a :: euclidean_space set"
+  assumes "open S" "finite X" "p \<in> S"
+  shows "\<exists>e>0. \<forall>w\<in>ball p e. w\<in>S \<and> (w\<noteq>p \<longrightarrow> w\<notin>X)"
+proof -
+  obtain e1 where "0 < e1" and e1_b:"ball p e1 \<subseteq> S" 
+    using open_contains_ball_eq[OF \<open>open S\<close>] assms by auto
+  obtain e2 where "0 < e2" and "\<forall>x\<in>X. x \<noteq> p \<longrightarrow> e2 \<le> dist p x" 
+    using finite_set_avoid[OF \<open>finite X\<close>,of p] by auto
+  hence "\<forall>w\<in>ball p (min e1 e2). w\<in>S \<and> (w\<noteq>p \<longrightarrow> w\<notin>X)" 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> X)" using \<open>e2>0\<close> \<open>e1>0\<close> 
+    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 X" "p \<in> S"
+  shows "\<exists>e>0. \<forall>w\<in>cball p e. w\<in>S \<and> (w\<noteq>p \<longrightarrow> w\<notin>X)"
+proof -
+  obtain e1 where "e1>0" and e1: "\<forall>w\<in>ball p e1. w\<in>S \<and> (w\<noteq>p \<longrightarrow> w\<notin>X)" 
+    using finite_ball_avoid[OF assms] by auto
+  define e2 where "e2 \<equiv> e1/2"
+  have "e2>0" and "e2 < e1" unfolding e2_def using \<open>e1>0\<close> 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> X)" using \<open>e2>0\<close> e1 by auto
+qed
+
 no_notation
   eucl_less (infix "<e" 50)