# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1487775899 0
# Node ID 87972e6177bccdabeb3e7b332c5777953f1b8212
# Parent  9391ea7daa17c7c7b1152a227ac18f636b1750f2
New theory about Winding Numbers

diff -r 9391ea7daa17 -r 87972e6177bc src/HOL/Analysis/Analysis.thy
--- a/src/HOL/Analysis/Analysis.thy	Wed Feb 22 12:30:28 2017 +0000
+++ b/src/HOL/Analysis/Analysis.thy	Wed Feb 22 15:04:59 2017 +0000
@@ -12,6 +12,7 @@
   Weierstrass_Theorems
   Polytope
   Jordan_Curve
+  Winding_Numbers
   Poly_Roots
   Conformal_Mappings
   Generalised_Binomial_Theorem
diff -r 9391ea7daa17 -r 87972e6177bc src/HOL/Analysis/Conformal_Mappings.thy
--- a/src/HOL/Analysis/Conformal_Mappings.thy	Wed Feb 22 12:30:28 2017 +0000
+++ b/src/HOL/Analysis/Conformal_Mappings.thy	Wed Feb 22 15:04:59 2017 +0000
@@ -5,7 +5,7 @@
 text\<open>Also Cauchy's residue theorem by Wenda Li (2016)\<close>
 
 theory Conformal_Mappings
-imports "~~/src/HOL/Analysis/Cauchy_Integral_Theorem"
+imports "Cauchy_Integral_Theorem"
 
 begin
 
diff -r 9391ea7daa17 -r 87972e6177bc src/HOL/Analysis/Winding_Numbers.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Analysis/Winding_Numbers.thy	Wed Feb 22 15:04:59 2017 +0000
@@ -0,0 +1,783 @@
+section \<open>Winding Numbers\<close>
+
+text\<open>By John Harrison et al.  Ported from HOL Light by L C Paulson (2017)\<close>
+
+theory Winding_Numbers
+imports Polytope Jordan_Curve Cauchy_Integral_Theorem
+begin
+
+subsection\<open>Winding number for a triangle\<close>
+
+lemma wn_triangle1:
+  assumes "0 \<in> interior(convex hull {a,b,c})"
+    shows "~ (Im(a/b) \<le> 0 \<and> 0 \<le> Im(b/c))"
+proof -
+  { assume 0: "Im(a/b) \<le> 0" "0 \<le> Im(b/c)"
+    have "0 \<notin> interior (convex hull {a,b,c})"
+    proof (cases "a=0 \<or> b=0 \<or> c=0")
+      case True then show ?thesis
+        by (auto simp: not_in_interior_convex_hull_3)
+    next
+      case False
+      then have "b \<noteq> 0" by blast
+      { fix x y::complex and u::real
+        assume eq_f': "Im x * Re b \<le> Im b * Re x" "Im y * Re b \<le> Im b * Re y" "0 \<le> u" "u \<le> 1"
+        then have "((1 - u) * Im x) * Re b \<le> Im b * ((1 - u) * Re x)"
+          by (simp add: mult_left_mono mult.assoc mult.left_commute [of "Im b"])
+        then have "((1 - u) * Im x + u * Im y) * Re b \<le> Im b * ((1 - u) * Re x + u * Re y)"
+          using eq_f' ordered_comm_semiring_class.comm_mult_left_mono
+          by (fastforce simp add: algebra_simps)
+      }
+      with False 0 have "convex hull {a,b,c} \<le> {z. Im z * Re b \<le> Im b * Re z}"
+        apply (simp add: Complex.Im_divide divide_simps complex_neq_0 [symmetric])
+        apply (simp add: algebra_simps)
+        apply (rule hull_minimal)
+        apply (auto simp: algebra_simps convex_alt)
+        done
+      moreover have "0 \<notin> interior({z. Im z * Re b \<le> Im b * Re z})"
+      proof
+        assume "0 \<in> interior {z. Im z * Re b \<le> Im b * Re z}"
+        then obtain e where "e>0" and e: "ball 0 e \<subseteq> {z. Im z * Re b \<le> Im b * Re z}"
+          by (meson mem_interior)
+        def z \<equiv> "- sgn (Im b) * (e/3) + sgn (Re b) * (e/3) * ii"
+        have "z \<in> ball 0 e"
+          using `e>0`
+          apply (simp add: z_def dist_norm)
+          apply (rule le_less_trans [OF norm_triangle_ineq4])
+          apply (simp add: norm_mult abs_sgn_eq)
+          done
+        then have "z \<in> {z. Im z * Re b \<le> Im b * Re z}"
+          using e by blast
+        then show False
+          using `e>0` `b \<noteq> 0`
+          apply (simp add: z_def dist_norm sgn_if less_eq_real_def mult_less_0_iff complex.expand split: if_split_asm)
+          apply (auto simp: algebra_simps)
+          apply (meson less_asym less_trans mult_pos_pos neg_less_0_iff_less)
+          by (metis less_asym mult_pos_pos neg_less_0_iff_less)
+      qed
+      ultimately show ?thesis
+        using interior_mono by blast
+    qed
+  } with assms show ?thesis by blast
+qed
+
+lemma wn_triangle2_0:
+  assumes "0 \<in> interior(convex hull {a,b,c})"
+  shows
+       "0 < Im((b - a) * cnj (b)) \<and>
+        0 < Im((c - b) * cnj (c)) \<and>
+        0 < Im((a - c) * cnj (a))
+        \<or>
+        Im((b - a) * cnj (b)) < 0 \<and>
+        0 < Im((b - c) * cnj (b)) \<and>
+        0 < Im((a - b) * cnj (a)) \<and>
+        0 < Im((c - a) * cnj (c))"
+proof -
+  have [simp]: "{b,c,a} = {a,b,c}" "{c,a,b} = {a,b,c}" by auto
+  show ?thesis
+    using wn_triangle1 [OF assms] wn_triangle1 [of b c a] wn_triangle1 [of c a b] assms
+    by (auto simp: algebra_simps Im_complex_div_gt_0 Im_complex_div_lt_0 not_le not_less)
+qed
+
+lemma wn_triangle2:
+  assumes "z \<in> interior(convex hull {a,b,c})"
+   shows "0 < Im((b - a) * cnj (b - z)) \<and>
+          0 < Im((c - b) * cnj (c - z)) \<and>
+          0 < Im((a - c) * cnj (a - z))
+          \<or>
+          Im((b - a) * cnj (b - z)) < 0 \<and>
+          0 < Im((b - c) * cnj (b - z)) \<and>
+          0 < Im((a - b) * cnj (a - z)) \<and>
+          0 < Im((c - a) * cnj (c - z))"
+proof -
+  have 0: "0 \<in> interior(convex hull {a-z, b-z, c-z})"
+    using assms convex_hull_translation [of "-z" "{a,b,c}"]
+                interior_translation [of "-z"]
+    by simp
+  show ?thesis using wn_triangle2_0 [OF 0]
+    by simp
+qed
+
+lemma wn_triangle3:
+  assumes z: "z \<in> interior(convex hull {a,b,c})"
+      and "0 < Im((b-a) * cnj (b-z))"
+          "0 < Im((c-b) * cnj (c-z))"
+          "0 < Im((a-c) * cnj (a-z))"
+    shows "winding_number (linepath a b +++ linepath b c +++ linepath c a) z = 1"
+proof -
+  have znot[simp]: "z \<notin> closed_segment a b" "z \<notin> closed_segment b c" "z \<notin> closed_segment c a"
+    using z interior_of_triangle [of a b c]
+    by (auto simp: closed_segment_def)
+  have gt0: "0 < Re (winding_number (linepath a b +++ linepath b c +++ linepath c a) z)"
+    using assms
+    by (simp add: winding_number_linepath_pos_lt path_image_join winding_number_join_pos_combined)
+  have lt2: "Re (winding_number (linepath a b +++ linepath b c +++ linepath c a) z) < 2"
+    using winding_number_lt_half_linepath [of _ a b]
+    using winding_number_lt_half_linepath [of _ b c]
+    using winding_number_lt_half_linepath [of _ c a] znot
+    apply (fastforce simp add: winding_number_join path_image_join)
+    done
+  show ?thesis
+    by (rule winding_number_eq_1) (simp_all add: path_image_join gt0 lt2)
+qed
+
+proposition winding_number_triangle:
+  assumes z: "z \<in> interior(convex hull {a,b,c})"
+    shows "winding_number(linepath a b +++ linepath b c +++ linepath c a) z =
+           (if 0 < Im((b - a) * cnj (b - z)) then 1 else -1)"
+proof -
+  have [simp]: "{a,c,b} = {a,b,c}"  by auto
+  have znot[simp]: "z \<notin> closed_segment a b" "z \<notin> closed_segment b c" "z \<notin> closed_segment c a"
+    using z interior_of_triangle [of a b c]
+    by (auto simp: closed_segment_def)
+  then have [simp]: "z \<notin> closed_segment b a" "z \<notin> closed_segment c b" "z \<notin> closed_segment a c"
+    using closed_segment_commute by blast+
+  have *: "winding_number (linepath a b +++ linepath b c +++ linepath c a) z =
+            winding_number (reversepath (linepath a c +++ linepath c b +++ linepath b a)) z"
+    by (simp add: reversepath_joinpaths winding_number_join not_in_path_image_join)
+  show ?thesis
+    using wn_triangle2 [OF z] apply (rule disjE)
+    apply (simp add: wn_triangle3 z)
+    apply (simp add: path_image_join winding_number_reversepath * wn_triangle3 z)
+    done
+qed
+
+subsection\<open>Winding numbers for simple closed paths\<close>
+
+lemma winding_number_from_innerpath:
+  assumes "simple_path c1" and c1: "pathstart c1 = a" "pathfinish c1 = b"
+      and "simple_path c2" and c2: "pathstart c2 = a" "pathfinish c2 = b"
+      and "simple_path c" and c: "pathstart c = a" "pathfinish c = b"
+      and c1c2: "path_image c1 \<inter> path_image c2 = {a,b}"
+      and c1c:  "path_image c1 \<inter> path_image c = {a,b}"
+      and c2c:  "path_image c2 \<inter> path_image c = {a,b}"
+      and ne_12: "path_image c \<inter> inside(path_image c1 \<union> path_image c2) \<noteq> {}"
+      and z: "z \<in> inside(path_image c1 \<union> path_image c)"
+      and wn_d: "winding_number (c1 +++ reversepath c) z = d"
+      and "a \<noteq> b" "d \<noteq> 0"
+  obtains "z \<in> inside(path_image c1 \<union> path_image c2)" "winding_number (c1 +++ reversepath c2) z = d"
+proof -
+  obtain 0: "inside(path_image c1 \<union> path_image c) \<inter> inside(path_image c2 \<union> path_image c) = {}"
+     and 1: "inside(path_image c1 \<union> path_image c) \<union> inside(path_image c2 \<union> path_image c) \<union>
+             (path_image c - {a,b}) = inside(path_image c1 \<union> path_image c2)"
+    by (rule split_inside_simple_closed_curve
+              [OF \<open>simple_path c1\<close> c1 \<open>simple_path c2\<close> c2 \<open>simple_path c\<close> c \<open>a \<noteq> b\<close> c1c2 c1c c2c ne_12])
+  have znot: "z \<notin> path_image c"  "z \<notin> path_image c1" "z \<notin> path_image c2"
+    using union_with_outside z 1 by auto
+  have wn_cc2: "winding_number (c +++ reversepath c2) z = 0"
+    apply (rule winding_number_zero_in_outside)
+    apply (simp_all add: \<open>simple_path c2\<close> c c2 \<open>simple_path c\<close> simple_path_imp_path path_image_join)
+    by (metis "0" ComplI UnE disjoint_iff_not_equal sup.commute union_with_inside z znot)
+  show ?thesis
+  proof
+    show "z \<in> inside (path_image c1 \<union> path_image c2)"
+      using "1" z by blast
+    have "winding_number c1 z - winding_number c z = d "
+      using assms znot
+      by (metis wn_d winding_number_join simple_path_imp_path winding_number_reversepath add.commute path_image_reversepath path_reversepath pathstart_reversepath uminus_add_conv_diff)
+    then show "winding_number (c1 +++ reversepath c2) z = d"
+      using wn_cc2 by (simp add: winding_number_join simple_path_imp_path assms znot winding_number_reversepath)
+  qed
+qed
+
+
+
+lemma simple_closed_path_wn1:
+  fixes a::complex and e::real
+  assumes "0 < e"
+    and sp_pl: "simple_path(p +++ linepath (a - e) (a + e))"
+    and psp:   "pathstart p = a + e"
+    and pfp:   "pathfinish p = a - e"
+    and disj:  "ball a e \<inter> path_image p = {}"
+obtains z where "z \<in> inside (path_image (p +++ linepath (a - e) (a + e)))"
+                "cmod (winding_number (p +++ linepath (a - e) (a + e)) z) = 1"
+proof -
+  have "arc p" and arc_lp: "arc (linepath (a - e) (a + e))"
+    and pap: "path_image p \<inter> path_image (linepath (a - e) (a + e)) \<subseteq> {pathstart p, a-e}"
+    using simple_path_join_loop_eq [of "linepath (a - e) (a + e)" p] assms by auto
+  have mid_eq_a: "midpoint (a - e) (a + e) = a"
+    by (simp add: midpoint_def)
+  then have "a \<in> path_image(p +++ linepath (a - e) (a + e))"
+    apply (simp add: assms path_image_join)
+    by (metis midpoint_in_closed_segment)
+  have "a \<in> frontier(inside (path_image(p +++ linepath (a - e) (a + e))))"
+    apply (simp add: assms Jordan_inside_outside)
+    apply (simp_all add: assms path_image_join)
+    by (metis mid_eq_a midpoint_in_closed_segment)
+  with \<open>0 < e\<close> obtain c where c: "c \<in> inside (path_image(p +++ linepath (a - e) (a + e)))"
+                  and dac: "dist a c < e"
+    by (auto simp: frontier_straddle)
+  then have "c \<notin> path_image(p +++ linepath (a - e) (a + e))"
+    using inside_no_overlap by blast
+  then have "c \<notin> path_image p"
+            "c \<notin> closed_segment (a - of_real e) (a + of_real e)"
+    by (simp_all add: assms path_image_join)
+  with \<open>0 < e\<close> dac have "c \<notin> affine hull {a - of_real e, a + of_real e}"
+    by (simp add: segment_as_ball not_le)
+  with \<open>0 < e\<close> have *: "~collinear{a - e, c,a + e}"
+    using collinear_3_affine_hull [of "a-e" "a+e"] by (auto simp: insert_commute)
+  have 13: "1/3 + 1/3 + 1/3 = (1::real)" by simp
+  have "(1/3) *\<^sub>R (a - of_real e) + (1/3) *\<^sub>R c + (1/3) *\<^sub>R (a + of_real e) \<in> interior(convex hull {a - e, c, a + e})"
+    using interior_convex_hull_3_minimal [OF * DIM_complex]
+    by clarsimp (metis 13 zero_less_divide_1_iff zero_less_numeral)
+  then obtain z where z: "z \<in> interior(convex hull {a - e, c, a + e})" by force
+  have [simp]: "z \<notin> closed_segment (a - e) c"
+    by (metis DIM_complex Diff_iff IntD2 inf_sup_absorb interior_of_triangle z)
+  have [simp]: "z \<notin> closed_segment (a + e) (a - e)"
+    by (metis DIM_complex DiffD2 Un_iff interior_of_triangle z)
+  have [simp]: "z \<notin> closed_segment c (a + e)"
+    by (metis (no_types, lifting) DIM_complex DiffD2 Un_insert_right inf_sup_aci(5) insertCI interior_of_triangle mk_disjoint_insert z)
+  show thesis
+  proof
+    have "norm (winding_number (linepath (a - e) c +++ linepath c (a + e) +++ linepath (a + e) (a - e)) z) = 1"
+      using winding_number_triangle [OF z] by simp
+    have zin: "z \<in> inside (path_image (linepath (a + e) (a - e)) \<union> path_image p)"
+      and zeq: "winding_number (linepath (a + e) (a - e) +++ reversepath p) z =
+                winding_number (linepath (a - e) c +++ linepath c (a + e) +++ linepath (a + e) (a - e)) z"
+    proof (rule winding_number_from_innerpath
+        [of "linepath (a + e) (a - e)" "a+e" "a-e" p
+          "linepath (a + e) c +++ linepath c (a - e)" z
+          "winding_number (linepath (a - e)  c +++ linepath  c (a + e) +++ linepath (a + e) (a - e)) z"])
+      show sp_aec: "simple_path (linepath (a + e) c +++ linepath c (a - e))"
+      proof (rule arc_imp_simple_path [OF arc_join])
+        show "arc (linepath (a + e) c)"
+          by (metis \<open>c \<notin> path_image p\<close> arc_linepath pathstart_in_path_image psp)
+        show "arc (linepath c (a - e))"
+          by (metis \<open>c \<notin> path_image p\<close> arc_linepath pathfinish_in_path_image pfp)
+        show "path_image (linepath (a + e) c) \<inter> path_image (linepath c (a - e)) \<subseteq> {pathstart (linepath c (a - e))}"
+          by clarsimp (metis "*" IntI Int_closed_segment closed_segment_commute singleton_iff)
+      qed auto
+      show "simple_path p"
+        using \<open>arc p\<close> arc_simple_path by blast
+      show sp_ae2: "simple_path (linepath (a + e) (a - e))"
+        using \<open>arc p\<close> arc_distinct_ends pfp psp by fastforce
+      show pa: "pathfinish (linepath (a + e) (a - e)) = a - e"
+           "pathstart (linepath (a + e) c +++ linepath c (a - e)) = a + e"
+           "pathfinish (linepath (a + e) c +++ linepath c (a - e)) = a - e"
+           "pathstart p = a + e" "pathfinish p = a - e"
+           "pathstart (linepath (a + e) (a - e)) = a + e"
+        by (simp_all add: assms)
+      show 1: "path_image (linepath (a + e) (a - e)) \<inter> path_image p = {a + e, a - e}"
+      proof
+        show "path_image (linepath (a + e) (a - e)) \<inter> path_image p \<subseteq> {a + e, a - e}"
+          using pap closed_segment_commute psp segment_convex_hull by fastforce
+        show "{a + e, a - e} \<subseteq> path_image (linepath (a + e) (a - e)) \<inter> path_image p"
+          using pap pathfinish_in_path_image pathstart_in_path_image pfp psp by fastforce
+      qed
+      show 2: "path_image (linepath (a + e) (a - e)) \<inter> path_image (linepath (a + e) c +++ linepath c (a - e)) =
+               {a + e, a - e}"  (is "?lhs = ?rhs")
+      proof
+        have "\<not> collinear {c, a + e, a - e}"
+          using * by (simp add: insert_commute)
+        then have "convex hull {a + e, a - e} \<inter> convex hull {a + e, c} = {a + e}"
+                  "convex hull {a + e, a - e} \<inter> convex hull {c, a - e} = {a - e}"
+          by (metis (full_types) Int_closed_segment insert_commute segment_convex_hull)+
+        then show "?lhs \<subseteq> ?rhs"
+          by (metis Int_Un_distrib equalityD1 insert_is_Un path_image_join path_image_linepath path_join_eq path_linepath segment_convex_hull simple_path_def sp_aec)
+        show "?rhs \<subseteq> ?lhs"
+          using segment_convex_hull by (simp add: path_image_join)
+      qed
+      have "path_image p \<inter> path_image (linepath (a + e) c) \<subseteq> {a + e}"
+      proof (clarsimp simp: path_image_join)
+        fix x
+        assume "x \<in> path_image p" and x_ac: "x \<in> closed_segment (a + e) c"
+        then have "dist x a \<ge> e"
+          by (metis IntI all_not_in_conv disj dist_commute mem_ball not_less)
+        with x_ac dac \<open>e > 0\<close> show "x = a + e"
+          by (auto simp: norm_minus_commute dist_norm closed_segment_eq_open dest: open_segment_furthest_le [where y=a])
+      qed
+      moreover
+      have "path_image p \<inter> path_image (linepath c (a - e)) \<subseteq> {a - e}"
+      proof (clarsimp simp: path_image_join)
+        fix x
+        assume "x \<in> path_image p" and x_ac: "x \<in> closed_segment c (a - e)"
+        then have "dist x a \<ge> e"
+          by (metis IntI all_not_in_conv disj dist_commute mem_ball not_less)
+        with x_ac dac \<open>e > 0\<close> show "x = a - e"
+          by (auto simp: norm_minus_commute dist_norm closed_segment_eq_open dest: open_segment_furthest_le [where y=a])
+      qed
+      ultimately
+      have "path_image p \<inter> path_image (linepath (a + e) c +++ linepath c (a - e)) \<subseteq> {a + e, a - e}"
+        by (force simp: path_image_join)
+      then show 3: "path_image p \<inter> path_image (linepath (a + e) c +++ linepath c (a - e)) = {a + e, a - e}"
+        apply (rule equalityI)
+        apply (clarsimp simp: path_image_join)
+        apply (metis pathstart_in_path_image psp pathfinish_in_path_image pfp)
+        done
+      show 4: "path_image (linepath (a + e) c +++ linepath c (a - e)) \<inter>
+               inside (path_image (linepath (a + e) (a - e)) \<union> path_image p) \<noteq> {}"
+        apply (clarsimp simp: path_image_join segment_convex_hull disjoint_iff_not_equal)
+        by (metis (no_types, hide_lams) UnI1 Un_commute c closed_segment_commute ends_in_segment(1) path_image_join
+                  path_image_linepath pathstart_linepath pfp segment_convex_hull)
+      show zin_inside: "z \<in> inside (path_image (linepath (a + e) (a - e)) \<union>
+                                    path_image (linepath (a + e) c +++ linepath c (a - e)))"
+        apply (simp add: path_image_join)
+        by (metis z inside_of_triangle DIM_complex Un_commute closed_segment_commute)
+      show 5: "winding_number
+             (linepath (a + e) (a - e) +++ reversepath (linepath (a + e) c +++ linepath c (a - e))) z =
+            winding_number (linepath (a - e) c +++ linepath c (a + e) +++ linepath (a + e) (a - e)) z"
+        by (simp add: reversepath_joinpaths path_image_join winding_number_join)
+      show 6: "winding_number (linepath (a - e) c +++ linepath c (a + e) +++ linepath (a + e) (a - e)) z \<noteq> 0"
+        by (simp add: winding_number_triangle z)
+      show "winding_number (linepath (a + e) (a - e) +++ reversepath p) z =
+            winding_number (linepath (a - e) c +++ linepath c (a + e) +++ linepath (a + e) (a - e)) z"
+        by (metis 1 2 3 4 5 6 pa sp_aec sp_ae2 \<open>arc p\<close> \<open>simple_path p\<close> arc_distinct_ends winding_number_from_innerpath zin_inside)
+    qed (use assms \<open>e > 0\<close> in auto)
+    show "z \<in> inside (path_image (p +++ linepath (a - e) (a + e)))"
+      using zin by (simp add: assms path_image_join Un_commute closed_segment_commute)
+    then have "cmod (winding_number (p +++ linepath (a - e) (a + e)) z) =
+               cmod ((winding_number(reversepath (p +++ linepath (a - e) (a + e))) z))"
+      apply (subst winding_number_reversepath)
+      using simple_path_imp_path sp_pl apply blast
+       apply (metis IntI emptyE inside_no_overlap)
+      by (simp add: inside_def)
+    also have "... = cmod (winding_number(linepath (a + e) (a - e) +++ reversepath p) z)"
+      by (simp add: pfp reversepath_joinpaths)
+    also have "... = cmod (winding_number (linepath (a - e) c +++ linepath c (a + e) +++ linepath (a + e) (a - e)) z)"
+      by (simp add: zeq)
+    also have "... = 1"
+      using z by (simp add: interior_of_triangle winding_number_triangle)
+    finally show "cmod (winding_number (p +++ linepath (a - e) (a + e)) z) = 1" .
+  qed
+qed
+
+
+
+lemma simple_closed_path_wn2:
+  fixes a::complex and d e::real
+  assumes "0 < d" "0 < e"
+    and sp_pl: "simple_path(p +++ linepath (a - d) (a + e))"
+    and psp:   "pathstart p = a + e"
+    and pfp:   "pathfinish p = a - d"
+obtains z where "z \<in> inside (path_image (p +++ linepath (a - d) (a + e)))"
+                "cmod (winding_number (p +++ linepath (a - d) (a + e)) z) = 1"
+proof -
+  have [simp]: "a + of_real x \<in> closed_segment (a - \<alpha>) (a - \<beta>) \<longleftrightarrow> x \<in> closed_segment (-\<alpha>) (-\<beta>)" for x \<alpha> \<beta>::real
+    using closed_segment_translation_eq [of a]
+    by (metis (no_types, hide_lams) add_uminus_conv_diff of_real_minus of_real_closed_segment)
+  have [simp]: "a - of_real x \<in> closed_segment (a + \<alpha>) (a + \<beta>) \<longleftrightarrow> -x \<in> closed_segment \<alpha> \<beta>" for x \<alpha> \<beta>::real
+    by (metis closed_segment_translation_eq diff_conv_add_uminus of_real_closed_segment of_real_minus)
+  have "arc p" and arc_lp: "arc (linepath (a - d) (a + e))" and "path p"
+    and pap: "path_image p \<inter> closed_segment (a - d) (a + e) \<subseteq> {a+e, a-d}"
+    using simple_path_join_loop_eq [of "linepath (a - d) (a + e)" p] assms arc_imp_path  by auto
+  have "0 \<in> closed_segment (-d) e"
+    using \<open>0 < d\<close> \<open>0 < e\<close> closed_segment_eq_real_ivl by auto
+  then have "a \<in> path_image (linepath (a - d) (a + e))"
+    using of_real_closed_segment [THEN iffD2]
+    by (force dest: closed_segment_translation_eq [of a, THEN iffD2] simp del: of_real_closed_segment)
+  then have "a \<notin> path_image p"
+    using \<open>0 < d\<close> \<open>0 < e\<close> pap by auto
+  then obtain k where "0 < k" and k: "ball a k \<inter> (path_image p) = {}"
+    using \<open>0 < e\<close> \<open>path p\<close> not_on_path_ball by blast
+  define kde where "kde \<equiv> (min k (min d e)) / 2"
+  have "0 < kde" "kde < k" "kde < d" "kde < e"
+    using \<open>0 < k\<close> \<open>0 < d\<close> \<open>0 < e\<close> by (auto simp: kde_def)
+  let ?q = "linepath (a + kde) (a + e) +++ p +++ linepath (a - d) (a - kde)"
+  have "- kde \<in> closed_segment (-d) e"
+    using \<open>0 < kde\<close> \<open>kde < d\<close> \<open>kde < e\<close> closed_segment_eq_real_ivl by auto
+  then have a_diff_kde: "a - kde \<in> closed_segment (a - d) (a + e)"
+    using of_real_closed_segment [THEN iffD2]
+    by (force dest: closed_segment_translation_eq [of a, THEN iffD2] simp del: of_real_closed_segment)
+  then have clsub2: "closed_segment (a - d) (a - kde) \<subseteq> closed_segment (a - d) (a + e)"
+    by (simp add: subset_closed_segment)
+  then have "path_image p \<inter> closed_segment (a - d) (a - kde) \<subseteq> {a + e, a - d}"
+    using pap by force
+  moreover
+  have "a + e \<notin> path_image p \<inter> closed_segment (a - d) (a - kde)"
+    using \<open>0 < kde\<close> \<open>kde < d\<close> \<open>0 < e\<close> by (auto simp: closed_segment_eq_real_ivl)
+  ultimately have sub_a_diff_d: "path_image p \<inter> closed_segment (a - d) (a - kde) \<subseteq> {a - d}"
+    by blast
+  have "kde \<in> closed_segment (-d) e"
+    using \<open>0 < kde\<close> \<open>kde < d\<close> \<open>kde < e\<close> closed_segment_eq_real_ivl by auto
+  then have a_diff_kde: "a + kde \<in> closed_segment (a - d) (a + e)"
+    using of_real_closed_segment [THEN iffD2]
+    by (force dest: closed_segment_translation_eq [of "a", THEN iffD2] simp del: of_real_closed_segment)
+  then have clsub1: "closed_segment (a + kde) (a + e) \<subseteq> closed_segment (a - d) (a + e)"
+    by (simp add: subset_closed_segment)
+  then have "closed_segment (a + kde) (a + e) \<inter> path_image p \<subseteq> {a + e, a - d}"
+    using pap by force
+  moreover
+  have "closed_segment (a + kde) (a + e) \<inter> closed_segment (a - d) (a - kde) = {}"
+  proof (clarsimp intro!: equals0I)
+    fix y
+    assume y1: "y \<in> closed_segment (a + kde) (a + e)"
+       and y2: "y \<in> closed_segment (a - d) (a - kde)"
+    obtain u where u: "y = a + of_real u" and "0 < u"
+      using y1 \<open>0 < kde\<close> \<open>kde < e\<close> \<open>0 < e\<close> apply (clarsimp simp: in_segment)
+      apply (rule_tac u = "(1 - u)*kde + u*e" in that)
+       apply (auto simp: scaleR_conv_of_real algebra_simps)
+      by (meson le_less_trans less_add_same_cancel2 less_eq_real_def mult_left_mono)
+    moreover
+    obtain v where v: "y = a + of_real v" and "v \<le> 0"
+      using y2 \<open>0 < kde\<close> \<open>0 < d\<close> \<open>0 < e\<close> apply (clarsimp simp: in_segment)
+      apply (rule_tac v = "- ((1 - u)*d + u*kde)" in that)
+       apply (force simp: scaleR_conv_of_real algebra_simps)
+      by (meson less_eq_real_def neg_le_0_iff_le segment_bound_lemma)
+    ultimately show False
+      by auto
+  qed
+  moreover have "a - d \<notin> closed_segment (a + kde) (a + e)"
+    using \<open>0 < kde\<close> \<open>kde < d\<close> \<open>0 < e\<close> by (auto simp: closed_segment_eq_real_ivl)
+  ultimately have sub_a_plus_e:
+    "closed_segment (a + kde) (a + e) \<inter> (path_image p \<union> closed_segment (a - d) (a - kde))
+       \<subseteq> {a + e}"
+    by auto
+  have "kde \<in> closed_segment (-kde) e"
+    using \<open>0 < kde\<close> \<open>kde < d\<close> \<open>kde < e\<close> closed_segment_eq_real_ivl by auto
+  then have a_add_kde: "a + kde \<in> closed_segment (a - kde) (a + e)"
+    using of_real_closed_segment [THEN iffD2]
+    by (force dest: closed_segment_translation_eq [of "a", THEN iffD2] simp del: of_real_closed_segment)
+  have "closed_segment (a - kde) (a + kde) \<inter> closed_segment (a + kde) (a + e) = {a + kde}"
+    by (metis a_add_kde Int_closed_segment)
+  moreover
+  have "path_image p \<inter> closed_segment (a - kde) (a + kde) = {}"
+  proof (rule equals0I, clarify)
+    fix y  assume "y \<in> path_image p" "y \<in> closed_segment (a - kde) (a + kde)"
+    with equals0D [OF k, of y] \<open>0 < kde\<close> \<open>kde < k\<close> show False
+      by (auto simp: dist_norm dest: dist_decreases_closed_segment [where c=a])
+  qed
+  moreover
+  have "- kde \<in> closed_segment (-d) kde"
+    using \<open>0 < kde\<close> \<open>kde < d\<close> \<open>kde < e\<close> closed_segment_eq_real_ivl by auto
+  then have a_diff_kde': "a - kde \<in> closed_segment (a - d) (a + kde)"
+    using of_real_closed_segment [THEN iffD2]
+    by (force dest: closed_segment_translation_eq [of a, THEN iffD2] simp del: of_real_closed_segment)
+  then have "closed_segment (a - d) (a - kde) \<inter> closed_segment (a - kde) (a + kde) = {a - kde}"
+    by (metis Int_closed_segment)
+  ultimately
+  have pa_subset_pm_kde: "path_image ?q \<inter> closed_segment (a - kde) (a + kde) \<subseteq> {a - kde, a + kde}"
+    by (auto simp: path_image_join assms)
+  have ge_kde1: "\<exists>y. x = a + y \<and> y \<ge> kde" if "x \<in> closed_segment (a + kde) (a + e)" for x
+    using that \<open>kde < e\<close> mult_le_cancel_left
+    apply (auto simp: in_segment)
+    apply (rule_tac x="(1-u)*kde + u*e" in exI)
+    apply (fastforce simp: algebra_simps scaleR_conv_of_real)
+    done
+  have ge_kde2: "\<exists>y. x = a + y \<and> y \<le> -kde" if "x \<in> closed_segment (a - d) (a - kde)" for x
+    using that \<open>kde < d\<close> affine_ineq
+    apply (auto simp: in_segment)
+    apply (rule_tac x="- ((1-u)*d + u*kde)" in exI)
+    apply (fastforce simp: algebra_simps scaleR_conv_of_real)
+    done
+  have notin_paq: "x \<notin> path_image ?q" if "dist a x < kde" for x
+    using that using \<open>0 < kde\<close> \<open>kde < d\<close> \<open>kde < k\<close>
+    apply (auto simp: path_image_join assms dist_norm dest!: ge_kde1 ge_kde2)
+    by (meson k disjoint_iff_not_equal le_less_trans less_eq_real_def mem_ball that)
+  obtain z where zin: "z \<in> inside (path_image (?q +++ linepath (a - kde) (a + kde)))"
+           and z1: "cmod (winding_number (?q +++ linepath (a - kde) (a + kde)) z) = 1"
+  proof (rule simple_closed_path_wn1 [of kde ?q a])
+    show "simple_path (?q +++ linepath (a - kde) (a + kde))"
+    proof (intro simple_path_join_loop conjI)
+      show "arc ?q"
+      proof (rule arc_join)
+        show "arc (linepath (a + kde) (a + e))"
+          using \<open>kde < e\<close> \<open>arc p\<close> by (force simp: pfp)
+        show "arc (p +++ linepath (a - d) (a - kde))"
+          using \<open>kde < d\<close> \<open>kde < e\<close> \<open>arc p\<close> sub_a_diff_d by (force simp: pfp intro: arc_join)
+      qed (auto simp: psp pfp path_image_join sub_a_plus_e)
+      show "arc (linepath (a - kde) (a + kde))"
+        using \<open>0 < kde\<close> by auto
+    qed (use pa_subset_pm_kde in auto)
+  qed (use \<open>0 < kde\<close> notin_paq in auto)
+  have eq: "path_image (?q +++ linepath (a - kde) (a + kde)) = path_image (p +++ linepath (a - d) (a + e))"
+            (is "?lhs = ?rhs")
+  proof
+    show "?lhs \<subseteq> ?rhs"
+      using clsub1 clsub2 apply (auto simp: path_image_join assms)
+      by (meson subsetCE subset_closed_segment)
+    show "?rhs \<subseteq> ?lhs"
+      apply (simp add: path_image_join assms Un_ac)
+        by (metis Un_closed_segment Un_assoc a_diff_kde a_diff_kde' le_supI2 subset_refl)
+    qed
+  show thesis
+  proof
+    show zzin: "z \<in> inside (path_image (p +++ linepath (a - d) (a + e)))"
+      by (metis eq zin)
+    then have znotin: "z \<notin> path_image p"
+      by (metis ComplD Un_iff inside_Un_outside path_image_join pathfinish_linepath pathstart_reversepath pfp reversepath_linepath)
+    have znotin_de: "z \<notin> closed_segment (a - d) (a + kde)"
+      by (metis ComplD Un_iff Un_closed_segment a_diff_kde inside_Un_outside path_image_join path_image_linepath pathstart_linepath pfp zzin)
+    have "winding_number (linepath (a - d) (a + e)) z =
+          winding_number (linepath (a - d) (a + kde)) z + winding_number (linepath (a + kde) (a + e)) z"
+      apply (rule winding_number_split_linepath)
+      apply (simp add: a_diff_kde)
+      by (metis ComplD Un_iff inside_Un_outside path_image_join path_image_linepath pathstart_linepath pfp zzin)
+    also have "... = winding_number (linepath (a + kde) (a + e)) z +
+                     (winding_number (linepath (a - d) (a - kde)) z +
+                      winding_number (linepath (a - kde) (a + kde)) z)"
+      by (simp add: winding_number_split_linepath [of "a-kde", symmetric] znotin_de a_diff_kde')
+    finally have "winding_number (p +++ linepath (a - d) (a + e)) z =
+                    winding_number p z + winding_number (linepath (a + kde) (a + e)) z +
+                   (winding_number (linepath (a - d) (a - kde)) z +
+                    winding_number (linepath (a - kde) (a + kde)) z)"
+      by (metis (no_types, lifting) ComplD Un_iff \<open>arc p\<close> add.assoc arc_imp_path eq path_image_join path_join_path_ends path_linepath simple_path_imp_path sp_pl union_with_outside winding_number_join zin)
+    also have "... = winding_number ?q z + winding_number (linepath (a - kde) (a + kde)) z"
+      using \<open>path p\<close> znotin assms zzin clsub1
+      apply (subst winding_number_join, auto)
+      apply (metis (no_types, hide_lams) ComplD Un_iff contra_subsetD inside_Un_outside path_image_join path_image_linepath pathstart_linepath)
+      apply (metis Un_iff Un_closed_segment a_diff_kde' not_in_path_image_join path_image_linepath znotin_de)
+      by (metis Un_iff Un_closed_segment a_diff_kde' path_image_linepath path_linepath pathstart_linepath winding_number_join znotin_de)
+    also have "... = winding_number (?q +++ linepath (a - kde) (a + kde)) z"
+      using \<open>path p\<close> assms zin
+      apply (subst winding_number_join [symmetric], auto)
+      apply (metis ComplD Un_iff path_image_join pathfinish_join pathfinish_linepath pathstart_linepath union_with_outside)
+      by (metis Un_iff Un_closed_segment a_diff_kde' znotin_de)
+    finally have "winding_number (p +++ linepath (a - d) (a + e)) z =
+                  winding_number (?q +++ linepath (a - kde) (a + kde)) z" .
+    then show "cmod (winding_number (p +++ linepath (a - d) (a + e)) z) = 1"
+      by (simp add: z1)
+  qed
+qed
+
+
+proposition simple_closed_path_wn3:
+  fixes p :: "real \<Rightarrow> complex"
+  assumes "simple_path p" and loop: "pathfinish p = pathstart p"
+  obtains z where "z \<in> inside (path_image p)" "cmod (winding_number p z) = 1"
+proof -
+  have ins: "inside(path_image p) \<noteq> {}" "open(inside(path_image p))"
+            "connected(inside(path_image p))"
+   and out: "outside(path_image p) \<noteq> {}" "open(outside(path_image p))"
+            "connected(outside(path_image p))"
+   and bo:  "bounded(inside(path_image p))" "\<not> bounded(outside(path_image p))"
+   and ins_out: "inside(path_image p) \<inter> outside(path_image p) = {}"
+                "inside(path_image p) \<union> outside(path_image p) = - path_image p"
+   and fro: "frontier(inside(path_image p)) = path_image p"
+            "frontier(outside(path_image p)) = path_image p"
+    using Jordan_inside_outside [OF assms] by auto
+  obtain a where a: "a \<in> inside(path_image p)"
+    using \<open>inside (path_image p) \<noteq> {}\<close> by blast
+  obtain d::real where "0 < d" and d_fro: "a - d \<in> frontier (inside (path_image p))"
+                 and d_int: "\<And>\<epsilon>. \<lbrakk>0 \<le> \<epsilon>; \<epsilon> < d\<rbrakk> \<Longrightarrow> (a - \<epsilon>) \<in> inside (path_image p)"
+    apply (rule ray_to_frontier [of "inside (path_image p)" a "-1"])
+    using \<open>bounded (inside (path_image p))\<close> \<open>open (inside (path_image p))\<close> a interior_eq
+       apply (auto simp: of_real_def)
+    done
+  obtain e::real where "0 < e" and e_fro: "a + e \<in> frontier (inside (path_image p))"
+    and e_int: "\<And>\<epsilon>. \<lbrakk>0 \<le> \<epsilon>; \<epsilon> < e\<rbrakk> \<Longrightarrow> (a + \<epsilon>) \<in> inside (path_image p)"
+    apply (rule ray_to_frontier [of "inside (path_image p)" a 1])
+    using \<open>bounded (inside (path_image p))\<close> \<open>open (inside (path_image p))\<close> a interior_eq
+       apply (auto simp: of_real_def)
+    done
+  obtain t0 where "0 \<le> t0" "t0 \<le> 1" and pt: "p t0 = a - d"
+    using a d_fro fro by (auto simp: path_image_def)
+  obtain q where "simple_path q" and q_ends: "pathstart q = a - d" "pathfinish q = a - d"
+    and q_eq_p: "path_image q = path_image p"
+    and wn_q_eq_wn_p: "\<And>z. z \<in> inside(path_image p) \<Longrightarrow> winding_number q z = winding_number p z"
+  proof
+    show "simple_path (shiftpath t0 p)"
+      by (simp add: pathstart_shiftpath pathfinish_shiftpath
+          simple_path_shiftpath path_image_shiftpath \<open>0 \<le> t0\<close> \<open>t0 \<le> 1\<close> assms)
+    show "pathstart (shiftpath t0 p) = a - d"
+      using pt by (simp add: \<open>t0 \<le> 1\<close> pathstart_shiftpath)
+    show "pathfinish (shiftpath t0 p) = a - d"
+      by (simp add: \<open>0 \<le> t0\<close> loop pathfinish_shiftpath pt)
+    show "path_image (shiftpath t0 p) = path_image p"
+      by (simp add: \<open>0 \<le> t0\<close> \<open>t0 \<le> 1\<close> loop path_image_shiftpath)
+    show "winding_number (shiftpath t0 p) z = winding_number p z"
+      if "z \<in> inside (path_image p)" for z
+      by (metis ComplD Un_iff \<open>0 \<le> t0\<close> \<open>t0 \<le> 1\<close> \<open>simple_path p\<close> atLeastAtMost_iff inside_Un_outside
+          loop simple_path_imp_path that winding_number_shiftpath)
+  qed
+  have ad_not_ae: "a - d \<noteq> a + e"
+    by (metis \<open>0 < d\<close> \<open>0 < e\<close> add.left_inverse add_left_cancel add_uminus_conv_diff
+        le_add_same_cancel2 less_eq_real_def not_less of_real_add of_real_def of_real_eq_0_iff pt)
+  have ad_ae_q: "{a - d, a + e} \<subseteq> path_image q"
+    using \<open>path_image q = path_image p\<close> d_fro e_fro fro(1) by auto
+  have ada: "open_segment (a - d) a \<subseteq> inside (path_image p)"
+  proof (clarsimp simp: in_segment)
+    fix u::real assume "0 < u" "u < 1"
+    with d_int have "a - (1 - u) * d \<in> inside (path_image p)"
+      by (metis \<open>0 < d\<close> add.commute diff_add_cancel left_diff_distrib' less_add_same_cancel2 less_eq_real_def mult.left_neutral zero_less_mult_iff)
+    then show "(1 - u) *\<^sub>R (a - d) + u *\<^sub>R a \<in> inside (path_image p)"
+      by (simp add: diff_add_eq of_real_def real_vector.scale_right_diff_distrib)
+  qed
+  have aae: "open_segment a (a + e) \<subseteq> inside (path_image p)"
+  proof (clarsimp simp: in_segment)
+    fix u::real assume "0 < u" "u < 1"
+    with e_int have "a + u * e \<in> inside (path_image p)"
+      by (meson \<open>0 < e\<close> less_eq_real_def mult_less_cancel_right2 not_less zero_less_mult_iff)
+    then show "(1 - u) *\<^sub>R a + u *\<^sub>R (a + e) \<in> inside (path_image p)"
+      apply (simp add: algebra_simps)
+      by (simp add: diff_add_eq of_real_def real_vector.scale_right_diff_distrib)
+  qed
+  have "complex_of_real (d * d + (e * e + d * (e + e))) \<noteq> 0"
+    using ad_not_ae
+    by (metis \<open>0 < d\<close> \<open>0 < e\<close> add_strict_left_mono less_add_same_cancel1 not_sum_squares_lt_zero
+        of_real_eq_0_iff zero_less_double_add_iff_zero_less_single_add zero_less_mult_iff)
+  then have a_in_de: "a \<in> open_segment (a - d) (a + e)"
+    using ad_not_ae \<open>0 < d\<close> \<open>0 < e\<close>
+    apply (auto simp: in_segment algebra_simps scaleR_conv_of_real)
+    apply (rule_tac x="d / (d+e)" in exI)
+    apply (auto simp: field_simps)
+    done
+  then have "open_segment (a - d) (a + e) \<subseteq> inside (path_image p)"
+    using ada a aae Un_open_segment [of a "a-d" "a+e"] by blast
+  then have "path_image q \<inter> open_segment (a - d) (a + e) = {}"
+    using inside_no_overlap by (fastforce simp: q_eq_p)
+  with ad_ae_q have paq_Int_cs: "path_image q \<inter> closed_segment (a - d) (a + e) = {a - d, a + e}"
+    by (simp add: closed_segment_eq_open)
+  obtain t where "0 \<le> t" "t \<le> 1" and qt: "q t = a + e"
+    using a e_fro fro ad_ae_q by (auto simp: path_defs)
+  then have "t \<noteq> 0"
+    by (metis ad_not_ae pathstart_def q_ends(1))
+  then have "t \<noteq> 1"
+    by (metis ad_not_ae pathfinish_def q_ends(2) qt)
+  have q01: "q 0 = a - d" "q 1 = a - d"
+    using q_ends by (auto simp: pathstart_def pathfinish_def)
+  obtain z where zin: "z \<in> inside (path_image (subpath t 0 q +++ linepath (a - d) (a + e)))"
+             and z1: "cmod (winding_number (subpath t 0 q +++ linepath (a - d) (a + e)) z) = 1"
+  proof (rule simple_closed_path_wn2 [of d e "subpath t 0 q" a], simp_all add: q01)
+    show "simple_path (subpath t 0 q +++ linepath (a - d) (a + e))"
+    proof (rule simple_path_join_loop, simp_all add: qt q01)
+      have "inj_on q (closed_segment t 0)"
+        using \<open>0 \<le> t\<close> \<open>simple_path q\<close> \<open>t \<le> 1\<close> \<open>t \<noteq> 0\<close> \<open>t \<noteq> 1\<close>
+        by (fastforce simp: simple_path_def inj_on_def closed_segment_eq_real_ivl)
+      then show "arc (subpath t 0 q)"
+        using \<open>0 \<le> t\<close> \<open>simple_path q\<close> \<open>t \<le> 1\<close> \<open>t \<noteq> 0\<close>
+        by (simp add: arc_subpath_eq simple_path_imp_path)
+      show "arc (linepath (a - d) (a + e))"
+        by (simp add: ad_not_ae)
+      show "path_image (subpath t 0 q) \<inter> closed_segment (a - d) (a + e) \<subseteq> {a + e, a - d}"
+        using qt paq_Int_cs  \<open>simple_path q\<close> \<open>0 \<le> t\<close> \<open>t \<le> 1\<close>
+        by (force simp: dest: rev_subsetD [OF _ path_image_subpath_subset] intro: simple_path_imp_path)
+    qed
+  qed (auto simp: \<open>0 < d\<close> \<open>0 < e\<close> qt)
+  have pa01_Un: "path_image (subpath 0 t q) \<union> path_image (subpath 1 t q) = path_image q"
+    unfolding path_image_subpath
+    using \<open>0 \<le> t\<close> \<open>t \<le> 1\<close> by (force simp: path_image_def image_iff)
+  with paq_Int_cs have pa_01q:
+        "(path_image (subpath 0 t q) \<union> path_image (subpath 1 t q)) \<inter> closed_segment (a - d) (a + e) = {a - d, a + e}"
+    by metis
+  have z_notin_ed: "z \<notin> closed_segment (a + e) (a - d)"
+    using zin q01 by (simp add: path_image_join closed_segment_commute inside_def)
+  have z_notin_0t: "z \<notin> path_image (subpath 0 t q)"
+    by (metis (no_types, hide_lams) IntI Un_upper1 subsetD empty_iff inside_no_overlap path_image_join
+        path_image_subpath_commute pathfinish_subpath pathstart_def pathstart_linepath q_ends(1) qt subpath_trivial zin)
+  have [simp]: "- winding_number (subpath t 0 q) z = winding_number (subpath 0 t q) z"
+    by (metis \<open>0 \<le> t\<close> \<open>simple_path q\<close> \<open>t \<le> 1\<close> atLeastAtMost_iff zero_le_one
+              path_image_subpath_commute path_subpath real_eq_0_iff_le_ge_0
+              reversepath_subpath simple_path_imp_path winding_number_reversepath z_notin_0t)
+  obtain z_in_q: "z \<in> inside(path_image q)"
+     and wn_q: "winding_number (subpath 0 t q +++ subpath t 1 q) z = - winding_number (subpath t 0 q +++ linepath (a - d) (a + e)) z"
+  proof (rule winding_number_from_innerpath
+          [of "subpath 0 t q" "a-d" "a+e" "subpath 1 t q" "linepath (a - d) (a + e)"
+            z "- winding_number (subpath t 0 q +++ linepath (a - d) (a + e)) z"],
+         simp_all add: q01 qt pa01_Un reversepath_subpath)
+    show "simple_path (subpath 0 t q)" "simple_path (subpath 1 t q)"
+      by (simp_all add: \<open>0 \<le> t\<close> \<open>simple_path q\<close> \<open>t \<le> 1\<close> \<open>t \<noteq> 0\<close> \<open>t \<noteq> 1\<close> simple_path_subpath)
+    show "simple_path (linepath (a - d) (a + e))"
+      using ad_not_ae by blast
+    show "path_image (subpath 0 t q) \<inter> path_image (subpath 1 t q) = {a - d, a + e}"  (is "?lhs = ?rhs")
+    proof
+      show "?lhs \<subseteq> ?rhs"
+        using \<open>0 \<le> t\<close> \<open>simple_path q\<close> \<open>t \<le> 1\<close> \<open>t \<noteq> 1\<close> q_ends qt q01
+        by (force simp: pathfinish_def qt simple_path_def path_image_subpath)
+      show "?rhs \<subseteq> ?lhs"
+        using \<open>0 \<le> t\<close> \<open>t \<le> 1\<close> q01 qt by (force simp: path_image_subpath)
+    qed
+    show "path_image (subpath 0 t q) \<inter> closed_segment (a - d) (a + e) = {a - d, a + e}" (is "?lhs = ?rhs")
+    proof
+      show "?lhs \<subseteq> ?rhs"  using paq_Int_cs pa01_Un by fastforce
+      show "?rhs \<subseteq> ?lhs"  using \<open>0 \<le> t\<close> \<open>t \<le> 1\<close> q01 qt by (force simp: path_image_subpath)
+    qed
+    show "path_image (subpath 1 t q) \<inter> closed_segment (a - d) (a + e) = {a - d, a + e}" (is "?lhs = ?rhs")
+    proof
+      show "?lhs \<subseteq> ?rhs"  by (auto simp: pa_01q [symmetric])
+      show "?rhs \<subseteq> ?lhs"  using \<open>0 \<le> t\<close> \<open>t \<le> 1\<close> q01 qt by (force simp: path_image_subpath)
+    qed
+    show "closed_segment (a - d) (a + e) \<inter> inside (path_image q) \<noteq> {}"
+      using a a_in_de open_closed_segment pa01_Un q_eq_p by fastforce
+    show "z \<in> inside (path_image (subpath 0 t q) \<union> closed_segment (a - d) (a + e))"
+      by (metis path_image_join path_image_linepath path_image_subpath_commute pathfinish_subpath pathstart_linepath q01(1) zin)
+    show "winding_number (subpath 0 t q +++ linepath (a + e) (a - d)) z =
+      - winding_number (subpath t 0 q +++ linepath (a - d) (a + e)) z"
+      using z_notin_ed z_notin_0t \<open>0 \<le> t\<close> \<open>simple_path q\<close> \<open>t \<le> 1\<close>
+      by (simp add: simple_path_imp_path qt q01 path_image_subpath_commute closed_segment_commute winding_number_join winding_number_reversepath [symmetric])
+    show "- complex_of_real d \<noteq> complex_of_real e"
+      using ad_not_ae by auto
+    show "winding_number (subpath t 0 q +++ linepath (a - d) (a + e)) z \<noteq> 0"
+      using z1 by auto
+  qed
+  show ?thesis
+  proof
+    show "z \<in> inside (path_image p)"
+      using q_eq_p z_in_q by auto
+    then have [simp]: "z \<notin> path_image q"
+      by (metis disjoint_iff_not_equal inside_no_overlap q_eq_p)
+    have [simp]: "z \<notin> path_image (subpath 1 t q)"
+      using inside_def pa01_Un z_in_q by fastforce
+    have "winding_number(subpath 0 t q +++ subpath t 1 q) z = winding_number(subpath 0 1 q) z"
+      using z_notin_0t \<open>0 \<le> t\<close> \<open>simple_path q\<close> \<open>t \<le> 1\<close>
+      by (simp add: simple_path_imp_path qt path_image_subpath_commute winding_number_join winding_number_subpath_combine)
+    with wn_q have "winding_number (subpath t 0 q +++ linepath (a - d) (a + e)) z = - winding_number q z"
+      by auto
+    with z1 have "cmod (winding_number q z) = 1"
+      by simp
+    with z1 wn_q_eq_wn_p show "cmod (winding_number p z) = 1"
+      using z1 wn_q_eq_wn_p  by (simp add: \<open>z \<in> inside (path_image p)\<close>)
+    qed
+qed
+
+
+theorem simple_closed_path_winding_number_inside:
+  assumes "simple_path \<gamma>"
+  obtains "\<And>z. z \<in> inside(path_image \<gamma>) \<Longrightarrow> winding_number \<gamma> z = 1"
+        | "\<And>z. z \<in> inside(path_image \<gamma>) \<Longrightarrow> winding_number \<gamma> z = -1"
+proof (cases "pathfinish \<gamma> = pathstart \<gamma>")
+  case True
+  have "path \<gamma>"
+    by (simp add: assms simple_path_imp_path)
+  then obtain k where k: "\<And>z. z \<in> inside(path_image \<gamma>) \<Longrightarrow> winding_number \<gamma> z = k"
+  proof (rule winding_number_constant)
+    show "connected (inside(path_image \<gamma>))"
+      by (simp add: Jordan_inside_outside True assms)
+  qed (use inside_no_overlap True in auto)
+  obtain z where zin: "z \<in> inside (path_image \<gamma>)" and z1: "cmod (winding_number \<gamma> z) = 1"
+    using simple_closed_path_wn3 [of \<gamma>] True assms by blast
+  with k have "winding_number \<gamma> z = k"
+    by blast
+  have "winding_number \<gamma> z \<in> \<int>"
+    using zin integer_winding_number [OF \<open>path \<gamma>\<close> True] inside_def by blast
+  with z1 consider "winding_number \<gamma> z = 1" | "winding_number \<gamma> z = -1"
+    apply (auto simp: Ints_def abs_if split: if_split_asm)
+    by (metis of_int_1 of_int_eq_iff of_int_minus)
+  then show ?thesis
+    using that \<open>winding_number \<gamma> z = k\<close> k by auto
+next
+  case False
+  then show ?thesis
+    using inside_simple_curve_imp_closed assms that(2) by blast
+qed
+
+corollary simple_closed_path_abs_winding_number_inside:
+  assumes "simple_path \<gamma>" "z \<in> inside(path_image \<gamma>)"
+    shows "\<bar>Re (winding_number \<gamma> z)\<bar> = 1"
+  by (metis assms norm_minus_cancel norm_one one_complex.simps(1) real_norm_def simple_closed_path_winding_number_inside uminus_complex.simps(1))
+
+corollary simple_closed_path_norm_winding_number_inside:
+  assumes "simple_path \<gamma>" "z \<in> inside(path_image \<gamma>)"
+  shows "norm (winding_number \<gamma> z) = 1"
+proof -
+  have "pathfinish \<gamma> = pathstart \<gamma>"
+    using assms inside_simple_curve_imp_closed by blast
+  with assms integer_winding_number have "winding_number \<gamma> z \<in> \<int>"
+    by (simp add: inside_def simple_path_def)
+  then show ?thesis
+    by (metis assms norm_minus_cancel norm_one simple_closed_path_winding_number_inside)
+qed
+
+corollary simple_closed_path_winding_number_cases:
+   "\<lbrakk>simple_path \<gamma>; pathfinish \<gamma> = pathstart \<gamma>; z \<notin> path_image \<gamma>\<rbrakk> \<Longrightarrow> winding_number \<gamma> z \<in> {-1,0,1}"
+apply (simp add: inside_Un_outside [of "path_image \<gamma>", symmetric, unfolded set_eq_iff Set.Compl_iff] del: inside_Un_outside)
+   apply (rule simple_closed_path_winding_number_inside)
+  using simple_path_def winding_number_zero_in_outside by blast+
+
+corollary simple_closed_path_winding_number_pos:
+   "\<lbrakk>simple_path \<gamma>; pathfinish \<gamma> = pathstart \<gamma>; z \<notin> path_image \<gamma>; 0 < Re(winding_number \<gamma> z)\<rbrakk>
+    \<Longrightarrow> winding_number \<gamma> z = 1"
+using simple_closed_path_winding_number_cases
+  by fastforce
+
+end
+