Theory Winding_Numbers

theory Winding_Numbers
imports Jordan_Curve Riemann_Mapping
section ‹Winding Numbers›

text‹By John Harrison et al.  Ported from HOL Light by L C Paulson (2017)›

theory Winding_Numbers
imports Polytope Jordan_Curve Riemann_Mapping
begin

lemma simply_connected_inside_simple_path:
  fixes p :: "real ⇒ complex"
  shows "simple_path p ⟹ simply_connected(inside(path_image p))"
  using Jordan_inside_outside connected_simple_path_image inside_simple_curve_imp_closed simply_connected_eq_frontier_properties
  by fastforce

lemma simply_connected_Int:
  fixes S :: "complex set"
  assumes "open S" "open T" "simply_connected S" "simply_connected T" "connected (S ∩ T)"
  shows "simply_connected (S ∩ T)"
  using assms by (force simp: simply_connected_eq_winding_number_zero open_Int)

subsection‹Winding number for a triangle›

lemma wn_triangle1:
  assumes "0 ∈ interior(convex hull {a,b,c})"
    shows "~ (Im(a/b) ≤ 0 ∧ 0 ≤ Im(b/c))"
proof -
  { assume 0: "Im(a/b) ≤ 0" "0 ≤ Im(b/c)"
    have "0 ∉ interior (convex hull {a,b,c})"
    proof (cases "a=0 ∨ b=0 ∨ c=0")
      case True then show ?thesis
        by (auto simp: not_in_interior_convex_hull_3)
    next
      case False
      then have "b ≠ 0" by blast
      { fix x y::complex and u::real
        assume eq_f': "Im x * Re b ≤ Im b * Re x" "Im y * Re b ≤ Im b * Re y" "0 ≤ u" "u ≤ 1"
        then have "((1 - u) * Im x) * Re b ≤ 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 ≤ 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} ≤ {z. Im z * Re b ≤ 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 ∉ interior({z. Im z * Re b ≤ Im b * Re z})"
      proof
        assume "0 ∈ interior {z. Im z * Re b ≤ Im b * Re z}"
        then obtain e where "e>0" and e: "ball 0 e ⊆ {z. Im z * Re b ≤ Im b * Re z}"
          by (meson mem_interior)
        define z where "z ≡ - sgn (Im b) * (e/3) + sgn (Re b) * (e/3) * 𝗂"
        have "z ∈ 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 ∈ {z. Im z * Re b ≤ Im b * Re z}"
          using e by blast
        then show False
          using ‹e>0› ‹b ≠ 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 ∈ interior(convex hull {a,b,c})"
  shows
       "0 < Im((b - a) * cnj (b)) ∧
        0 < Im((c - b) * cnj (c)) ∧
        0 < Im((a - c) * cnj (a))
        ∨
        Im((b - a) * cnj (b)) < 0 ∧
        0 < Im((b - c) * cnj (b)) ∧
        0 < Im((a - b) * cnj (a)) ∧
        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 ∈ interior(convex hull {a,b,c})"
   shows "0 < Im((b - a) * cnj (b - z)) ∧
          0 < Im((c - b) * cnj (c - z)) ∧
          0 < Im((a - c) * cnj (a - z))
          ∨
          Im((b - a) * cnj (b - z)) < 0 ∧
          0 < Im((b - c) * cnj (b - z)) ∧
          0 < Im((a - b) * cnj (a - z)) ∧
          0 < Im((c - a) * cnj (c - z))"
proof -
  have 0: "0 ∈ 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 ∈ 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 ∉ closed_segment a b" "z ∉ closed_segment b c" "z ∉ 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 ∈ 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 ∉ closed_segment a b" "z ∉ closed_segment b c" "z ∉ closed_segment c a"
    using z interior_of_triangle [of a b c]
    by (auto simp: closed_segment_def)
  then have [simp]: "z ∉ closed_segment b a" "z ∉ closed_segment c b" "z ∉ 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‹Winding numbers for simple closed paths›

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 ∩ path_image c2 = {a,b}"
      and c1c:  "path_image c1 ∩ path_image c = {a,b}"
      and c2c:  "path_image c2 ∩ path_image c = {a,b}"
      and ne_12: "path_image c ∩ inside(path_image c1 ∪ path_image c2) ≠ {}"
      and z: "z ∈ inside(path_image c1 ∪ path_image c)"
      and wn_d: "winding_number (c1 +++ reversepath c) z = d"
      and "a ≠ b" "d ≠ 0"
  obtains "z ∈ inside(path_image c1 ∪ path_image c2)" "winding_number (c1 +++ reversepath c2) z = d"
proof -
  obtain 0: "inside(path_image c1 ∪ path_image c) ∩ inside(path_image c2 ∪ path_image c) = {}"
     and 1: "inside(path_image c1 ∪ path_image c) ∪ inside(path_image c2 ∪ path_image c) ∪
             (path_image c - {a,b}) = inside(path_image c1 ∪ path_image c2)"
    by (rule split_inside_simple_closed_curve
              [OF ‹simple_path c1› c1 ‹simple_path c2› c2 ‹simple_path c› c ‹a ≠ b› c1c2 c1c c2c ne_12])
  have znot: "z ∉ path_image c"  "z ∉ path_image c1" "z ∉ 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: ‹simple_path c2› c c2 ‹simple_path c› 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 ∈ inside (path_image c1 ∪ 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 ∩ path_image p = {}"
obtains z where "z ∈ 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 ∩ path_image (linepath (a - e) (a + e)) ⊆ {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 ∈ path_image(p +++ linepath (a - e) (a + e))"
    apply (simp add: assms path_image_join)
    by (metis midpoint_in_closed_segment)
  have "a ∈ 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 ‹0 < e› obtain c where c: "c ∈ inside (path_image(p +++ linepath (a - e) (a + e)))"
                  and dac: "dist a c < e"
    by (auto simp: frontier_straddle)
  then have "c ∉ path_image(p +++ linepath (a - e) (a + e))"
    using inside_no_overlap by blast
  then have "c ∉ path_image p"
            "c ∉ closed_segment (a - of_real e) (a + of_real e)"
    by (simp_all add: assms path_image_join)
  with ‹0 < e› dac have "c ∉ affine hull {a - of_real e, a + of_real e}"
    by (simp add: segment_as_ball not_le)
  with ‹0 < e› 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) *R (a - of_real e) + (1/3) *R c + (1/3) *R (a + of_real e) ∈ 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 ∈ interior(convex hull {a - e, c, a + e})" by force
  have [simp]: "z ∉ closed_segment (a - e) c"
    by (metis DIM_complex Diff_iff IntD2 inf_sup_absorb interior_of_triangle z)
  have [simp]: "z ∉ closed_segment (a + e) (a - e)"
    by (metis DIM_complex DiffD2 Un_iff interior_of_triangle z)
  have [simp]: "z ∉ 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 ∈ inside (path_image (linepath (a + e) (a - e)) ∪ 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 ‹c ∉ path_image p› arc_linepath pathstart_in_path_image psp)
        show "arc (linepath c (a - e))"
          by (metis ‹c ∉ path_image p› arc_linepath pathfinish_in_path_image pfp)
        show "path_image (linepath (a + e) c) ∩ path_image (linepath c (a - e)) ⊆ {pathstart (linepath c (a - e))}"
          by clarsimp (metis "*" IntI Int_closed_segment closed_segment_commute singleton_iff)
      qed auto
      show "simple_path p"
        using ‹arc p› arc_simple_path by blast
      show sp_ae2: "simple_path (linepath (a + e) (a - e))"
        using ‹arc p› 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)) ∩ path_image p = {a + e, a - e}"
      proof
        show "path_image (linepath (a + e) (a - e)) ∩ path_image p ⊆ {a + e, a - e}"
          using pap closed_segment_commute psp segment_convex_hull by fastforce
        show "{a + e, a - e} ⊆ path_image (linepath (a + e) (a - e)) ∩ 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)) ∩ path_image (linepath (a + e) c +++ linepath c (a - e)) =
               {a + e, a - e}"  (is "?lhs = ?rhs")
      proof
        have "¬ collinear {c, a + e, a - e}"
          using * by (simp add: insert_commute)
        then have "convex hull {a + e, a - e} ∩ convex hull {a + e, c} = {a + e}"
                  "convex hull {a + e, a - e} ∩ convex hull {c, a - e} = {a - e}"
          by (metis (full_types) Int_closed_segment insert_commute segment_convex_hull)+
        then show "?lhs ⊆ ?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 ⊆ ?lhs"
          using segment_convex_hull by (simp add: path_image_join)
      qed
      have "path_image p ∩ path_image (linepath (a + e) c) ⊆ {a + e}"
      proof (clarsimp simp: path_image_join)
        fix x
        assume "x ∈ path_image p" and x_ac: "x ∈ closed_segment (a + e) c"
        then have "dist x a ≥ e"
          by (metis IntI all_not_in_conv disj dist_commute mem_ball not_less)
        with x_ac dac ‹e > 0› 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 ∩ path_image (linepath c (a - e)) ⊆ {a - e}"
      proof (clarsimp simp: path_image_join)
        fix x
        assume "x ∈ path_image p" and x_ac: "x ∈ closed_segment c (a - e)"
        then have "dist x a ≥ e"
          by (metis IntI all_not_in_conv disj dist_commute mem_ball not_less)
        with x_ac dac ‹e > 0› 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 ∩ path_image (linepath (a + e) c +++ linepath c (a - e)) ⊆ {a + e, a - e}"
        by (force simp: path_image_join)
      then show 3: "path_image p ∩ 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)) ∩
               inside (path_image (linepath (a + e) (a - e)) ∪ path_image p) ≠ {}"
        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 ∈ inside (path_image (linepath (a + e) (a - e)) ∪
                                    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 ≠ 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 ‹arc p› ‹simple_path p› arc_distinct_ends winding_number_from_innerpath zin_inside)
    qed (use assms ‹e > 0› in auto)
    show "z ∈ 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 ∈ 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 ∈ closed_segment (a - α) (a - β) ⟷ x ∈ closed_segment (-α) (-β)" for x α β::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 ∈ closed_segment (a + α) (a + β) ⟷ -x ∈ closed_segment α β" for x α β::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 ∩ closed_segment (a - d) (a + e) ⊆ {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 ∈ closed_segment (-d) e"
    using ‹0 < d› ‹0 < e› closed_segment_eq_real_ivl by auto
  then have "a ∈ 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 ∉ path_image p"
    using ‹0 < d› ‹0 < e› pap by auto
  then obtain k where "0 < k" and k: "ball a k ∩ (path_image p) = {}"
    using ‹0 < e› ‹path p› not_on_path_ball by blast
  define kde where "kde ≡ (min k (min d e)) / 2"
  have "0 < kde" "kde < k" "kde < d" "kde < e"
    using ‹0 < k› ‹0 < d› ‹0 < e› by (auto simp: kde_def)
  let ?q = "linepath (a + kde) (a + e) +++ p +++ linepath (a - d) (a - kde)"
  have "- kde ∈ closed_segment (-d) e"
    using ‹0 < kde› ‹kde < d› ‹kde < e› closed_segment_eq_real_ivl by auto
  then have a_diff_kde: "a - kde ∈ 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) ⊆ closed_segment (a - d) (a + e)"
    by (simp add: subset_closed_segment)
  then have "path_image p ∩ closed_segment (a - d) (a - kde) ⊆ {a + e, a - d}"
    using pap by force
  moreover
  have "a + e ∉ path_image p ∩ closed_segment (a - d) (a - kde)"
    using ‹0 < kde› ‹kde < d› ‹0 < e› by (auto simp: closed_segment_eq_real_ivl)
  ultimately have sub_a_diff_d: "path_image p ∩ closed_segment (a - d) (a - kde) ⊆ {a - d}"
    by blast
  have "kde ∈ closed_segment (-d) e"
    using ‹0 < kde› ‹kde < d› ‹kde < e› closed_segment_eq_real_ivl by auto
  then have a_diff_kde: "a + kde ∈ 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) ⊆ closed_segment (a - d) (a + e)"
    by (simp add: subset_closed_segment)
  then have "closed_segment (a + kde) (a + e) ∩ path_image p ⊆ {a + e, a - d}"
    using pap by force
  moreover
  have "closed_segment (a + kde) (a + e) ∩ closed_segment (a - d) (a - kde) = {}"
  proof (clarsimp intro!: equals0I)
    fix y
    assume y1: "y ∈ closed_segment (a + kde) (a + e)"
       and y2: "y ∈ closed_segment (a - d) (a - kde)"
    obtain u where u: "y = a + of_real u" and "0 < u"
      using y1 ‹0 < kde› ‹kde < e› ‹0 < e› 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 ≤ 0"
      using y2 ‹0 < kde› ‹0 < d› ‹0 < e› 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 ∉ closed_segment (a + kde) (a + e)"
    using ‹0 < kde› ‹kde < d› ‹0 < e› by (auto simp: closed_segment_eq_real_ivl)
  ultimately have sub_a_plus_e:
    "closed_segment (a + kde) (a + e) ∩ (path_image p ∪ closed_segment (a - d) (a - kde))
       ⊆ {a + e}"
    by auto
  have "kde ∈ closed_segment (-kde) e"
    using ‹0 < kde› ‹kde < d› ‹kde < e› closed_segment_eq_real_ivl by auto
  then have a_add_kde: "a + kde ∈ 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) ∩ closed_segment (a + kde) (a + e) = {a + kde}"
    by (metis a_add_kde Int_closed_segment)
  moreover
  have "path_image p ∩ closed_segment (a - kde) (a + kde) = {}"
  proof (rule equals0I, clarify)
    fix y  assume "y ∈ path_image p" "y ∈ closed_segment (a - kde) (a + kde)"
    with equals0D [OF k, of y] ‹0 < kde› ‹kde < k› show False
      by (auto simp: dist_norm dest: dist_decreases_closed_segment [where c=a])
  qed
  moreover
  have "- kde ∈ closed_segment (-d) kde"
    using ‹0 < kde› ‹kde < d› ‹kde < e› closed_segment_eq_real_ivl by auto
  then have a_diff_kde': "a - kde ∈ 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) ∩ closed_segment (a - kde) (a + kde) = {a - kde}"
    by (metis Int_closed_segment)
  ultimately
  have pa_subset_pm_kde: "path_image ?q ∩ closed_segment (a - kde) (a + kde) ⊆ {a - kde, a + kde}"
    by (auto simp: path_image_join assms)
  have ge_kde1: "∃y. x = a + y ∧ y ≥ kde" if "x ∈ closed_segment (a + kde) (a + e)" for x
    using that ‹kde < e› 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: "∃y. x = a + y ∧ y ≤ -kde" if "x ∈ closed_segment (a - d) (a - kde)" for x
    using that ‹kde < d› 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 ∉ path_image ?q" if "dist a x < kde" for x
    using that using ‹0 < kde› ‹kde < d› ‹kde < k›
    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 ∈ 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 ‹kde < e› ‹arc p› by (force simp: pfp)
        show "arc (p +++ linepath (a - d) (a - kde))"
          using ‹kde < d› ‹kde < e› ‹arc p› 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 ‹0 < kde› by auto
    qed (use pa_subset_pm_kde in auto)
  qed (use ‹0 < kde› 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 ⊆ ?rhs"
      using clsub1 clsub2 apply (auto simp: path_image_join assms)
      by (meson subsetCE subset_closed_segment)
    show "?rhs ⊆ ?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 ∈ inside (path_image (p +++ linepath (a - d) (a + e)))"
      by (metis eq zin)
    then have znotin: "z ∉ 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 ∉ 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 ‹arc p› 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 ‹path p› 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 ‹path p› 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 ⇒ complex"
  assumes "simple_path p" and loop: "pathfinish p = pathstart p"
  obtains z where "z ∈ inside (path_image p)" "cmod (winding_number p z) = 1"
proof -
  have ins: "inside(path_image p) ≠ {}" "open(inside(path_image p))"
            "connected(inside(path_image p))"
   and out: "outside(path_image p) ≠ {}" "open(outside(path_image p))"
            "connected(outside(path_image p))"
   and bo:  "bounded(inside(path_image p))" "¬ bounded(outside(path_image p))"
   and ins_out: "inside(path_image p) ∩ outside(path_image p) = {}"
                "inside(path_image p) ∪ 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 ∈ inside(path_image p)"
    using ‹inside (path_image p) ≠ {}› by blast
  obtain d::real where "0 < d" and d_fro: "a - d ∈ frontier (inside (path_image p))"
                 and d_int: "⋀ε. ⟦0 ≤ ε; ε < d⟧ ⟹ (a - ε) ∈ inside (path_image p)"
    apply (rule ray_to_frontier [of "inside (path_image p)" a "-1"])
    using ‹bounded (inside (path_image p))› ‹open (inside (path_image p))› a interior_eq
       apply (auto simp: of_real_def)
    done
  obtain e::real where "0 < e" and e_fro: "a + e ∈ frontier (inside (path_image p))"
    and e_int: "⋀ε. ⟦0 ≤ ε; ε < e⟧ ⟹ (a + ε) ∈ inside (path_image p)"
    apply (rule ray_to_frontier [of "inside (path_image p)" a 1])
    using ‹bounded (inside (path_image p))› ‹open (inside (path_image p))› a interior_eq
       apply (auto simp: of_real_def)
    done
  obtain t0 where "0 ≤ t0" "t0 ≤ 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: "⋀z. z ∈ inside(path_image p) ⟹ 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 ‹0 ≤ t0› ‹t0 ≤ 1› assms)
    show "pathstart (shiftpath t0 p) = a - d"
      using pt by (simp add: ‹t0 ≤ 1› pathstart_shiftpath)
    show "pathfinish (shiftpath t0 p) = a - d"
      by (simp add: ‹0 ≤ t0› loop pathfinish_shiftpath pt)
    show "path_image (shiftpath t0 p) = path_image p"
      by (simp add: ‹0 ≤ t0› ‹t0 ≤ 1› loop path_image_shiftpath)
    show "winding_number (shiftpath t0 p) z = winding_number p z"
      if "z ∈ inside (path_image p)" for z
      by (metis ComplD Un_iff ‹0 ≤ t0› ‹t0 ≤ 1› ‹simple_path p› atLeastAtMost_iff inside_Un_outside
          loop simple_path_imp_path that winding_number_shiftpath)
  qed
  have ad_not_ae: "a - d ≠ a + e"
    by (metis ‹0 < d› ‹0 < e› 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} ⊆ path_image q"
    using ‹path_image q = path_image p› d_fro e_fro fro(1) by auto
  have ada: "open_segment (a - d) a ⊆ 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 ∈ inside (path_image p)"
      by (metis ‹0 < d› 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) *R (a - d) + u *R a ∈ 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) ⊆ inside (path_image p)"
  proof (clarsimp simp: in_segment)
    fix u::real assume "0 < u" "u < 1"
    with e_int have "a + u * e ∈ inside (path_image p)"
      by (meson ‹0 < e› less_eq_real_def mult_less_cancel_right2 not_less zero_less_mult_iff)
    then show "(1 - u) *R a + u *R (a + e) ∈ 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))) ≠ 0"
    using ad_not_ae
    by (metis ‹0 < d› ‹0 < e› 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 ∈ open_segment (a - d) (a + e)"
    using ad_not_ae ‹0 < d› ‹0 < e›
    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) ⊆ inside (path_image p)"
    using ada a aae Un_open_segment [of a "a-d" "a+e"] by blast
  then have "path_image q ∩ 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 ∩ closed_segment (a - d) (a + e) = {a - d, a + e}"
    by (simp add: closed_segment_eq_open)
  obtain t where "0 ≤ t" "t ≤ 1" and qt: "q t = a + e"
    using a e_fro fro ad_ae_q by (auto simp: path_defs)
  then have "t ≠ 0"
    by (metis ad_not_ae pathstart_def q_ends(1))
  then have "t ≠ 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 ∈ 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 ‹0 ≤ t› ‹simple_path q› ‹t ≤ 1› ‹t ≠ 0› ‹t ≠ 1›
        by (fastforce simp: simple_path_def inj_on_def closed_segment_eq_real_ivl)
      then show "arc (subpath t 0 q)"
        using ‹0 ≤ t› ‹simple_path q› ‹t ≤ 1› ‹t ≠ 0›
        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) ∩ closed_segment (a - d) (a + e) ⊆ {a + e, a - d}"
        using qt paq_Int_cs  ‹simple_path q› ‹0 ≤ t› ‹t ≤ 1›
        by (force simp: dest: rev_subsetD [OF _ path_image_subpath_subset] intro: simple_path_imp_path)
    qed
  qed (auto simp: ‹0 < d› ‹0 < e› qt)
  have pa01_Un: "path_image (subpath 0 t q) ∪ path_image (subpath 1 t q) = path_image q"
    unfolding path_image_subpath
    using ‹0 ≤ t› ‹t ≤ 1› by (force simp: path_image_def image_iff)
  with paq_Int_cs have pa_01q:
        "(path_image (subpath 0 t q) ∪ path_image (subpath 1 t q)) ∩ closed_segment (a - d) (a + e) = {a - d, a + e}"
    by metis
  have z_notin_ed: "z ∉ 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 ∉ 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 ‹0 ≤ t› ‹simple_path q› ‹t ≤ 1› 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 ∈ 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: ‹0 ≤ t› ‹simple_path q› ‹t ≤ 1› ‹t ≠ 0› ‹t ≠ 1› simple_path_subpath)
    show "simple_path (linepath (a - d) (a + e))"
      using ad_not_ae by blast
    show "path_image (subpath 0 t q) ∩ path_image (subpath 1 t q) = {a - d, a + e}"  (is "?lhs = ?rhs")
    proof
      show "?lhs ⊆ ?rhs"
        using ‹0 ≤ t› ‹simple_path q› ‹t ≤ 1› ‹t ≠ 1› q_ends qt q01
        by (force simp: pathfinish_def qt simple_path_def path_image_subpath)
      show "?rhs ⊆ ?lhs"
        using ‹0 ≤ t› ‹t ≤ 1› q01 qt by (force simp: path_image_subpath)
    qed
    show "path_image (subpath 0 t q) ∩ closed_segment (a - d) (a + e) = {a - d, a + e}" (is "?lhs = ?rhs")
    proof
      show "?lhs ⊆ ?rhs"  using paq_Int_cs pa01_Un by fastforce
      show "?rhs ⊆ ?lhs"  using ‹0 ≤ t› ‹t ≤ 1› q01 qt by (force simp: path_image_subpath)
    qed
    show "path_image (subpath 1 t q) ∩ closed_segment (a - d) (a + e) = {a - d, a + e}" (is "?lhs = ?rhs")
    proof
      show "?lhs ⊆ ?rhs"  by (auto simp: pa_01q [symmetric])
      show "?rhs ⊆ ?lhs"  using ‹0 ≤ t› ‹t ≤ 1› q01 qt by (force simp: path_image_subpath)
    qed
    show "closed_segment (a - d) (a + e) ∩ inside (path_image q) ≠ {}"
      using a a_in_de open_closed_segment pa01_Un q_eq_p by fastforce
    show "z ∈ inside (path_image (subpath 0 t q) ∪ 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 ‹0 ≤ t› ‹simple_path q› ‹t ≤ 1›
      by (simp add: simple_path_imp_path qt q01 path_image_subpath_commute closed_segment_commute winding_number_join winding_number_reversepath [symmetric])
    show "- d ≠ e"
      using ad_not_ae by auto
    show "winding_number (subpath t 0 q +++ linepath (a - d) (a + e)) z ≠ 0"
      using z1 by auto
  qed
  show ?thesis
  proof
    show "z ∈ inside (path_image p)"
      using q_eq_p z_in_q by auto
    then have [simp]: "z ∉ path_image q"
      by (metis disjoint_iff_not_equal inside_no_overlap q_eq_p)
    have [simp]: "z ∉ 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 ‹0 ≤ t› ‹simple_path q› ‹t ≤ 1›
      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: ‹z ∈ inside (path_image p)›)
    qed
qed


theorem simple_closed_path_winding_number_inside:
  assumes "simple_path γ"
  obtains "⋀z. z ∈ inside(path_image γ) ⟹ winding_number γ z = 1"
        | "⋀z. z ∈ inside(path_image γ) ⟹ winding_number γ z = -1"
proof (cases "pathfinish γ = pathstart γ")
  case True
  have "path γ"
    by (simp add: assms simple_path_imp_path)
  then have const: "winding_number γ constant_on inside(path_image γ)"
  proof (rule winding_number_constant)
    show "connected (inside(path_image γ))"
      by (simp add: Jordan_inside_outside True assms)
  qed (use inside_no_overlap True in auto)
  obtain z where zin: "z ∈ inside (path_image γ)" and z1: "cmod (winding_number γ z) = 1"
    using simple_closed_path_wn3 [of γ] True assms by blast
  have "winding_number γ z ∈ ℤ"
    using zin integer_winding_number [OF ‹path γ› True] inside_def by blast
  with z1 consider "winding_number γ z = 1" | "winding_number γ 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)
  with that const zin show ?thesis
    unfolding constant_on_def by metis
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 γ" "z ∈ inside(path_image γ)"
    shows "¦Re (winding_number γ z)¦ = 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 γ" "z ∈ inside(path_image γ)"
  shows "norm (winding_number γ z) = 1"
proof -
  have "pathfinish γ = pathstart γ"
    using assms inside_simple_curve_imp_closed by blast
  with assms integer_winding_number have "winding_number γ z ∈ ℤ"
    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:
   "⟦simple_path γ; pathfinish γ = pathstart γ; z ∉ path_image γ⟧ ⟹ winding_number γ z ∈ {-1,0,1}"
apply (simp add: inside_Un_outside [of "path_image γ", 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:
   "⟦simple_path γ; pathfinish γ = pathstart γ; z ∉ path_image γ; 0 < Re(winding_number γ z)⟧
    ⟹ winding_number γ z = 1"
using simple_closed_path_winding_number_cases
  by fastforce


subsection ‹Winding number for rectangular paths›

(* TODO: Move *)
lemma closed_segmentI:
  "u ∈ {0..1} ⟹ z = (1 - u) *R a + u *R b ⟹ z ∈ closed_segment a b"
  by (auto simp: closed_segment_def)

lemma in_cbox_complex_iff:
  "x ∈ cbox a b ⟷ Re x ∈ {Re a..Re b} ∧ Im x ∈ {Im a..Im b}"
  by (cases x; cases a; cases b) (auto simp: cbox_Complex_eq)

lemma box_Complex_eq:
  "box (Complex a c) (Complex b d) = (λ(x,y). Complex x y) ` (box a b × box c d)"
  by (auto simp: box_def Basis_complex_def image_iff complex_eq_iff)

lemma in_box_complex_iff:
  "x ∈ box a b ⟷ Re x ∈ {Re a<..<Re b} ∧ Im x ∈ {Im a<..<Im b}"
  by (cases x; cases a; cases b) (auto simp: box_Complex_eq)
(* END TODO *)

lemma closed_segment_same_Re:
  assumes "Re a = Re b"
  shows   "closed_segment a b = {z. Re z = Re a ∧ Im z ∈ closed_segment (Im a) (Im b)}"
proof safe
  fix z assume "z ∈ closed_segment a b"
  then obtain u where u: "u ∈ {0..1}" "z = a + of_real u * (b - a)"
    by (auto simp: closed_segment_def scaleR_conv_of_real algebra_simps)
  from assms show "Re z = Re a" by (auto simp: u)
  from u(1) show "Im z ∈ closed_segment (Im a) (Im b)"
    by (intro closed_segmentI[of u]) (auto simp: u algebra_simps)
next
  fix z assume [simp]: "Re z = Re a" and "Im z ∈ closed_segment (Im a) (Im b)"
  then obtain u where u: "u ∈ {0..1}" "Im z = Im a + of_real u * (Im b - Im a)"
    by (auto simp: closed_segment_def scaleR_conv_of_real algebra_simps)
  from u(1) show "z ∈ closed_segment a b" using assms
    by (intro closed_segmentI[of u]) (auto simp: u algebra_simps scaleR_conv_of_real complex_eq_iff)
qed

lemma closed_segment_same_Im:
  assumes "Im a = Im b"
  shows   "closed_segment a b = {z. Im z = Im a ∧ Re z ∈ closed_segment (Re a) (Re b)}"
proof safe
  fix z assume "z ∈ closed_segment a b"
  then obtain u where u: "u ∈ {0..1}" "z = a + of_real u * (b - a)"
    by (auto simp: closed_segment_def scaleR_conv_of_real algebra_simps)
  from assms show "Im z = Im a" by (auto simp: u)
  from u(1) show "Re z ∈ closed_segment (Re a) (Re b)"
    by (intro closed_segmentI[of u]) (auto simp: u algebra_simps)
next
  fix z assume [simp]: "Im z = Im a" and "Re z ∈ closed_segment (Re a) (Re b)"
  then obtain u where u: "u ∈ {0..1}" "Re z = Re a + of_real u * (Re b - Re a)"
    by (auto simp: closed_segment_def scaleR_conv_of_real algebra_simps)
  from u(1) show "z ∈ closed_segment a b" using assms
    by (intro closed_segmentI[of u]) (auto simp: u algebra_simps scaleR_conv_of_real complex_eq_iff)
qed


definition rectpath where
  "rectpath a1 a3 = (let a2 = Complex (Re a3) (Im a1); a4 = Complex (Re a1) (Im a3)
                      in linepath a1 a2 +++ linepath a2 a3 +++ linepath a3 a4 +++ linepath a4 a1)"

lemma path_rectpath [simp, intro]: "path (rectpath a b)"
  by (simp add: Let_def rectpath_def)

lemma valid_path_rectpath [simp, intro]: "valid_path (rectpath a b)"
  by (simp add: Let_def rectpath_def)

lemma pathstart_rectpath [simp]: "pathstart (rectpath a1 a3) = a1"
  by (simp add: rectpath_def Let_def)

lemma pathfinish_rectpath [simp]: "pathfinish (rectpath a1 a3) = a1"
  by (simp add: rectpath_def Let_def)

lemma simple_path_rectpath [simp, intro]:
  assumes "Re a1 ≠ Re a3" "Im a1 ≠ Im a3"
  shows   "simple_path (rectpath a1 a3)"
  unfolding rectpath_def Let_def using assms
  by (intro simple_path_join_loop arc_join arc_linepath)
     (auto simp: complex_eq_iff path_image_join closed_segment_same_Re closed_segment_same_Im)

lemma path_image_rectpath:
  assumes "Re a1 ≤ Re a3" "Im a1 ≤ Im a3"
  shows "path_image (rectpath a1 a3) =
           {z. Re z ∈ {Re a1, Re a3} ∧ Im z ∈ {Im a1..Im a3}} ∪
           {z. Im z ∈ {Im a1, Im a3} ∧ Re z ∈ {Re a1..Re a3}}" (is "?lhs = ?rhs")
proof -
  define a2 a4 where "a2 = Complex (Re a3) (Im a1)" and "a4 = Complex (Re a1) (Im a3)"
  have "?lhs = closed_segment a1 a2 ∪ closed_segment a2 a3 ∪
                  closed_segment a4 a3 ∪ closed_segment a1 a4"
    by (simp_all add: rectpath_def Let_def path_image_join closed_segment_commute
                      a2_def a4_def Un_assoc)
  also have "… = ?rhs" using assms
    by (auto simp: rectpath_def Let_def path_image_join a2_def a4_def
          closed_segment_same_Re closed_segment_same_Im closed_segment_eq_real_ivl)
  finally show ?thesis .
qed

lemma path_image_rectpath_subset_cbox:
  assumes "Re a ≤ Re b" "Im a ≤ Im b"
  shows   "path_image (rectpath a b) ⊆ cbox a b"
  using assms by (auto simp: path_image_rectpath in_cbox_complex_iff)

lemma path_image_rectpath_inter_box:
  assumes "Re a ≤ Re b" "Im a ≤ Im b"
  shows   "path_image (rectpath a b) ∩ box a b = {}"
  using assms by (auto simp: path_image_rectpath in_box_complex_iff)

lemma path_image_rectpath_cbox_minus_box:
  assumes "Re a ≤ Re b" "Im a ≤ Im b"
  shows   "path_image (rectpath a b) = cbox a b - box a b"
  using assms by (auto simp: path_image_rectpath in_cbox_complex_iff
                             in_box_complex_iff)

lemma winding_number_rectpath:
  assumes "z ∈ box a1 a3"
  shows   "winding_number (rectpath a1 a3) z = 1"
proof -
  from assms have less: "Re a1 < Re a3" "Im a1 < Im a3"
    by (auto simp: in_box_complex_iff)
  define a2 a4 where "a2 = Complex (Re a3) (Im a1)" and "a4 = Complex (Re a1) (Im a3)"
  let ?l1 = "linepath a1 a2" and ?l2 = "linepath a2 a3"
  and ?l3 = "linepath a3 a4" and ?l4 = "linepath a4 a1"
  from assms and less have "z ∉ path_image (rectpath a1 a3)"
    by (auto simp: path_image_rectpath_cbox_minus_box)
  also have "path_image (rectpath a1 a3) =
               path_image ?l1 ∪ path_image ?l2 ∪ path_image ?l3 ∪ path_image ?l4"
    by (simp add: rectpath_def Let_def path_image_join Un_assoc a2_def a4_def)
  finally have "z ∉ …" .
  moreover have "∀l∈{?l1,?l2,?l3,?l4}. Re (winding_number l z) > 0"
    unfolding ball_simps HOL.simp_thms a2_def a4_def
    by (intro conjI; (rule winding_number_linepath_pos_lt;
          (insert assms, auto simp: a2_def a4_def in_box_complex_iff mult_neg_neg))+)
  ultimately have "Re (winding_number (rectpath a1 a3) z) > 0"
    by (simp add: winding_number_join path_image_join rectpath_def Let_def a2_def a4_def)
  thus "winding_number (rectpath a1 a3) z = 1" using assms less
    by (intro simple_closed_path_winding_number_pos simple_path_rectpath)
       (auto simp: path_image_rectpath_cbox_minus_box)
qed

lemma winding_number_rectpath_outside:
  assumes "Re a1 ≤ Re a3" "Im a1 ≤ Im a3"
  assumes "z ∉ cbox a1 a3"
  shows   "winding_number (rectpath a1 a3) z = 0"
  using assms by (intro winding_number_zero_outside[OF _ _ _ assms(3)]
                     path_image_rectpath_subset_cbox) simp_all


text‹A per-function version for continuous logs, a kind of monodromy›

proposition winding_number_compose_exp:
  assumes "path p"
  shows "winding_number (exp ∘ p) 0 = (pathfinish p - pathstart p) / (2 * of_real pi * 𝗂)"
proof -
  obtain e where "0 < e" and e: "⋀t. t ∈ {0..1} ⟹ e ≤ norm(exp(p t))"
  proof
     have "closed (path_image (exp ∘ p))"
       by (simp add: assms closed_path_image holomorphic_on_exp holomorphic_on_imp_continuous_on path_continuous_image)
    then show "0 < setdist {0} (path_image (exp ∘ p))"
      by (metis (mono_tags, lifting) compact_sing exp_not_eq_zero imageE path_image_compose
               path_image_nonempty setdist_eq_0_compact_closed setdist_gt_0_compact_closed setdist_eq_0_closed)
  next
    fix t::real
    assume "t ∈ {0..1}"
    have "setdist {0} (path_image (exp ∘ p)) ≤ dist 0 (exp (p t))"
      apply (rule setdist_le_dist)
      using ‹t ∈ {0..1}› path_image_def by fastforce+
    then show "setdist {0} (path_image (exp ∘ p)) ≤ cmod (exp (p t))"
      by simp
  qed
  have "bounded (path_image p)"
    by (simp add: assms bounded_path_image)
  then obtain B where "0 < B" and B: "path_image p ⊆ cball 0 B"
    by (meson bounded_pos mem_cball_0 subsetI)
  let ?B = "cball (0::complex) (B+1)"
  have "uniformly_continuous_on ?B exp"
    using holomorphic_on_exp holomorphic_on_imp_continuous_on
    by (force intro: compact_uniformly_continuous)
  then obtain d where "d > 0"
        and d: "⋀x x'. ⟦x∈?B; x'∈?B; dist x' x < d⟧ ⟹ norm (exp x' - exp x) < e"
    using ‹e > 0› by (auto simp: uniformly_continuous_on_def dist_norm)
  then have "min 1 d > 0"
    by force
  then obtain g where pfg: "polynomial_function g"  and "g 0 = p 0" "g 1 = p 1"
           and gless: "⋀t. t ∈ {0..1} ⟹ norm(g t - p t) < min 1 d"
    using path_approx_polynomial_function [OF ‹path p›] ‹d > 0› ‹0 < e›
    unfolding pathfinish_def pathstart_def by meson
  have "winding_number (exp ∘ p) 0 = winding_number (exp ∘ g) 0"
  proof (rule winding_number_nearby_paths_eq [symmetric])
    show "path (exp ∘ p)" "path (exp ∘ g)"
      by (simp_all add: pfg assms holomorphic_on_exp holomorphic_on_imp_continuous_on path_continuous_image path_polynomial_function)
  next
    fix t :: "real"
    assume t: "t ∈ {0..1}"
    with gless have "norm(g t - p t) < 1"
      using min_less_iff_conj by blast
    moreover have ptB: "norm (p t) ≤ B"
      using B t by (force simp: path_image_def)
    ultimately have "cmod (g t) ≤ B + 1"
      by (meson add_mono_thms_linordered_field(4) le_less_trans less_imp_le norm_triangle_sub)
    with ptB gless t have "cmod ((exp ∘ g) t - (exp ∘ p) t) < e"
      by (auto simp: dist_norm d)
    with e t show "cmod ((exp ∘ g) t - (exp ∘ p) t) < cmod ((exp ∘ p) t - 0)"
      by fastforce
  qed (use ‹g 0 = p 0› ‹g 1 = p 1› in ‹auto simp: pathfinish_def pathstart_def›)
  also have "... = 1 / (of_real (2 * pi) * 𝗂) * contour_integral (exp ∘ g) (λw. 1 / (w - 0))"
  proof (rule winding_number_valid_path)
    have "continuous_on (path_image g) (deriv exp)"
      by (metis DERIV_exp DERIV_imp_deriv continuous_on_cong holomorphic_on_exp holomorphic_on_imp_continuous_on)
    then show "valid_path (exp ∘ g)"
      by (simp add: field_differentiable_within_exp pfg valid_path_compose valid_path_polynomial_function)
    show "0 ∉ path_image (exp ∘ g)"
      by (auto simp: path_image_def)
  qed
  also have "... = 1 / (of_real (2 * pi) * 𝗂) * integral {0..1} (λx. vector_derivative g (at x))"
  proof (simp add: contour_integral_integral, rule integral_cong)
    fix t :: "real"
    assume t: "t ∈ {0..1}"
    show "vector_derivative (exp ∘ g) (at t) / exp (g t) = vector_derivative g (at t)"
    proof (simp add: divide_simps, rule vector_derivative_unique_at)
      show "(exp ∘ g has_vector_derivative vector_derivative (exp ∘ g) (at t)) (at t)"
        by (meson DERIV_exp differentiable_def field_vector_diff_chain_at has_vector_derivative_def
            has_vector_derivative_polynomial_function pfg vector_derivative_works)
      show "(exp ∘ g has_vector_derivative vector_derivative g (at t) * exp (g t)) (at t)"
        apply (rule field_vector_diff_chain_at)
        apply (metis has_vector_derivative_polynomial_function pfg vector_derivative_at)
        using DERIV_exp has_field_derivative_def apply blast
        done
    qed
  qed
  also have "... = (pathfinish p - pathstart p) / (2 * of_real pi * 𝗂)"
  proof -
    have "((λx. vector_derivative g (at x)) has_integral g 1 - g 0) {0..1}"
      apply (rule fundamental_theorem_of_calculus [OF zero_le_one])
      by (metis has_vector_derivative_at_within has_vector_derivative_polynomial_function pfg vector_derivative_at)
    then show ?thesis
    apply (simp add: pathfinish_def pathstart_def)
      using ‹g 0 = p 0› ‹g 1 = p 1› by auto
  qed
  finally show ?thesis .
qed



subsection‹The winding number defines a continuous logarithm for the path itself›

lemma winding_number_as_continuous_log:
  assumes "path p" and ζ: "ζ ∉ path_image p"
  obtains q where "path q"
                  "pathfinish q - pathstart q = 2 * of_real pi * 𝗂 * winding_number p ζ"
                  "⋀t. t ∈ {0..1} ⟹ p t = ζ + exp(q t)"
proof -
  let ?q = "λt. 2 * of_real pi * 𝗂 * winding_number(subpath 0 t p) ζ + Ln(pathstart p - ζ)"
  show ?thesis
  proof
    have *: "continuous (at t within {0..1}) (λx. winding_number (subpath 0 x p) ζ)"
      if t: "t ∈ {0..1}" for t
    proof -
      let ?B = "ball (p t) (norm(p t - ζ))"
      have "p t ≠ ζ"
        using path_image_def that ζ by blast
      then have "simply_connected ?B"
        by (simp add: convex_imp_simply_connected)
      then have "⋀f::complex⇒complex. continuous_on ?B f ∧ (∀ζ ∈ ?B. f ζ ≠ 0)
                  ⟶ (∃g. continuous_on ?B g ∧ (∀ζ ∈ ?B. f ζ = exp (g ζ)))"
        by (simp add: simply_connected_eq_continuous_log)
      moreover have "continuous_on ?B (λw. w - ζ)"
        by (intro continuous_intros)
      moreover have "(∀z ∈ ?B. z - ζ ≠ 0)"
        by (auto simp: dist_norm)
      ultimately obtain g where contg: "continuous_on ?B g"
        and geq: "⋀z. z ∈ ?B ⟹ z - ζ = exp (g z)" by blast
      obtain d where "0 < d" and d:
        "⋀x. ⟦x ∈ {0..1}; dist x t < d⟧ ⟹ dist (p x) (p t) < cmod (p t - ζ)"
        using ‹path p› t unfolding path_def continuous_on_iff
        by (metis ‹p t ≠ ζ› right_minus_eq zero_less_norm_iff)
      have "((λx. winding_number (λw. subpath 0 x p w - ζ) 0 -
                  winding_number (λw. subpath 0 t p w - ζ) 0) ⤏ 0)
            (at t within {0..1})"
      proof (rule Lim_transform_within [OF _ ‹d > 0›])
        have "continuous (at t within {0..1}) (g o p)"
        proof (rule continuous_within_compose)
          show "continuous (at t within {0..1}) p"
            using ‹path p› continuous_on_eq_continuous_within path_def that by blast
          show "continuous (at (p t) within p ` {0..1}) g"
            by (metis (no_types, lifting) open_ball UNIV_I ‹p t ≠ ζ› centre_in_ball contg continuous_on_eq_continuous_at continuous_within_topological right_minus_eq zero_less_norm_iff)
        qed
        with LIM_zero have "((λu. (g (subpath t u p 1) - g (subpath t u p 0))) ⤏ 0) (at t within {0..1})"
          by (auto simp: subpath_def continuous_within o_def)
        then show "((λu.  (g (subpath t u p 1) - g (subpath t u p 0)) / (2 * of_real pi * 𝗂)) ⤏ 0)
           (at t within {0..1})"
          by (simp add: tendsto_divide_zero)
        show "(g (subpath t u p 1) - g (subpath t u p 0)) / (2 * of_real pi * 𝗂) =
              winding_number (λw. subpath 0 u p w - ζ) 0 - winding_number (λw. subpath 0 t p w - ζ) 0"
          if "u ∈ {0..1}" "0 < dist u t" "dist u t < d" for u
        proof -
          have "closed_segment t u ⊆ {0..1}"
            using closed_segment_eq_real_ivl t that by auto
          then have piB: "path_image(subpath t u p) ⊆ ?B"
            apply (clarsimp simp add: path_image_subpath_gen)
            by (metis subsetD le_less_trans ‹dist u t < d› d dist_commute dist_in_closed_segment)
          have *: "path (g ∘ subpath t u p)"
            apply (rule path_continuous_image)
            using ‹path p› t that apply auto[1]
            using piB contg continuous_on_subset by blast
          have "(g (subpath t u p 1) - g (subpath t u p 0)) / (2 * of_real pi * 𝗂)
              =  winding_number (exp ∘ g ∘ subpath t u p) 0"
            using winding_number_compose_exp [OF *]
            by (simp add: pathfinish_def pathstart_def o_assoc)
          also have "... = winding_number (λw. subpath t u p w - ζ) 0"
          proof (rule winding_number_cong)
            have "exp(g y) = y - ζ" if "y ∈ (subpath t u p) ` {0..1}" for y
              by (metis that geq path_image_def piB subset_eq)
            then show "⋀x. ⟦0 ≤ x; x ≤ 1⟧ ⟹ (exp ∘ g ∘ subpath t u p) x = subpath t u p x - ζ"
              by auto
          qed
          also have "... = winding_number (λw. subpath 0 u p w - ζ) 0 -
                           winding_number (λw. subpath 0 t p w - ζ) 0"
            apply (simp add: winding_number_offset [symmetric])
            using winding_number_subpath_combine [OF ‹path p› ζ, of 0 t u] ‹t ∈ {0..1}› ‹u ∈ {0..1}›
            by (simp add: add.commute eq_diff_eq)
          finally show ?thesis .
        qed
      qed
      then show ?thesis
        by (subst winding_number_offset) (simp add: continuous_within LIM_zero_iff)
    qed
    show "path ?q"
      unfolding path_def
      by (intro continuous_intros) (simp add: continuous_on_eq_continuous_within *)

    have "ζ ≠ p 0"
      by (metis ζ pathstart_def pathstart_in_path_image)
    then show "pathfinish ?q - pathstart ?q = 2 * of_real pi * 𝗂 * winding_number p ζ"
      by (simp add: pathfinish_def pathstart_def)
    show "p t = ζ + exp (?q t)" if "t ∈ {0..1}" for t
    proof -
      have "path (subpath 0 t p)"
        using ‹path p› that by auto
      moreover
      have "ζ ∉ path_image (subpath 0 t p)"
        using ζ [unfolded path_image_def] that by (auto simp: path_image_subpath)
      ultimately show ?thesis
        using winding_number_exp_2pi [of "subpath 0 t p" ζ] ‹ζ ≠ p 0›
        by (auto simp: exp_add algebra_simps pathfinish_def pathstart_def subpath_def)
    qed
  qed
qed


subsection‹Winding number equality is the same as path/loop homotopy in C - {0}›

lemma winding_number_homotopic_loops_null_eq:
  assumes "path p" and ζ: "ζ ∉ path_image p"
  shows "winding_number p ζ = 0 ⟷ (∃a. homotopic_loops (-{ζ}) p (λt. a))"
    (is "?lhs = ?rhs")
proof
  assume [simp]: ?lhs
  obtain q where "path q"
             and qeq:  "pathfinish q - pathstart q = 2 * of_real pi * 𝗂 * winding_number p ζ"
             and peq: "⋀t. t ∈ {0..1} ⟹ p t = ζ + exp(q t)"
    using winding_number_as_continuous_log [OF assms] by blast
  have *: "homotopic_with (λr. pathfinish r = pathstart r)
                       {0..1} (-{ζ}) ((λw. ζ + exp w) ∘ q) ((λw. ζ + exp w) ∘ (λt. 0))"
  proof (rule homotopic_with_compose_continuous_left)
    show "homotopic_with (λf. pathfinish ((λw. ζ + exp w) ∘ f) = pathstart ((λw. ζ + exp w) ∘ f))
              {0..1} UNIV q (λt. 0)"
    proof (rule homotopic_with_mono, simp_all add: pathfinish_def pathstart_def)
      have "homotopic_loops UNIV q (λt. 0)"
        by (rule homotopic_loops_linear) (use qeq ‹path q› in ‹auto simp: continuous_on_const path_defs›)
      then show "homotopic_with (λh. exp (h 1) = exp (h 0)) {0..1} UNIV q (λt. 0)"
        by (simp add: homotopic_loops_def homotopic_with_mono pathfinish_def pathstart_def)
    qed
    show "continuous_on UNIV (λw. ζ + exp w)"
      by (rule continuous_intros)+
    show "range (λw. ζ + exp w) ⊆ -{ζ}"
      by auto
  qed
  then have "homotopic_with (λr. pathfinish r = pathstart r) {0..1} (-{ζ}) p (λx. ζ + 1)"
    by (rule homotopic_with_eq) (auto simp: o_def peq pathfinish_def pathstart_def)
  then have "homotopic_loops (-{ζ}) p (λt. ζ + 1)"
    by (simp add: homotopic_loops_def)
  then show ?rhs ..
next
  assume ?rhs
  then obtain a where "homotopic_loops (-{ζ}) p (λt. a)" ..
  then have "winding_number p ζ = winding_number (λt. a) ζ" "a ≠ ζ"
    using winding_number_homotopic_loops homotopic_loops_imp_subset by (force simp:)+
  moreover have "winding_number (λt. a) ζ = 0"
    by (metis winding_number_zero_const ‹a ≠ ζ›)
  ultimately show ?lhs by metis
qed


lemma winding_number_homotopic_paths_null_explicit_eq:
  assumes "path p" and ζ: "ζ ∉ path_image p"
  shows "winding_number p ζ = 0 ⟷ homotopic_paths (-{ζ}) p (linepath (pathstart p) (pathstart p))"
        (is "?lhs = ?rhs")
proof
  assume ?lhs
  then show ?rhs
    apply (auto simp: winding_number_homotopic_loops_null_eq [OF assms])
    apply (rule homotopic_loops_imp_homotopic_paths_null)
    apply (simp add: linepath_refl)
    done
next
  assume ?rhs
  then show ?lhs
    by (metis ζ pathstart_in_path_image winding_number_homotopic_paths winding_number_trivial)
qed


lemma winding_number_homotopic_paths_null_eq:
  assumes "path p" and ζ: "ζ ∉ path_image p"
  shows "winding_number p ζ = 0 ⟷ (∃a. homotopic_paths (-{ζ}) p (λt. a))"
    (is "?lhs = ?rhs")
proof
  assume ?lhs
  then show ?rhs
    by (auto simp: winding_number_homotopic_paths_null_explicit_eq [OF assms] linepath_refl)
next
  assume ?rhs
  then show ?lhs
    by (metis ζ homotopic_paths_imp_pathfinish pathfinish_def pathfinish_in_path_image winding_number_homotopic_paths winding_number_zero_const)
qed


lemma winding_number_homotopic_paths_eq:
  assumes "path p" and ζp: "ζ ∉ path_image p"
      and "path q" and ζq: "ζ ∉ path_image q"
      and qp: "pathstart q = pathstart p" "pathfinish q = pathfinish p"
    shows "winding_number p ζ = winding_number q ζ ⟷ homotopic_paths (-{ζ}) p q"
    (is "?lhs = ?rhs")
proof
  assume ?lhs
  then have "winding_number (p +++ reversepath q) ζ = 0"
    using assms by (simp add: winding_number_join winding_number_reversepath)
  moreover
  have "path (p +++ reversepath q)" "ζ ∉ path_image (p +++ reversepath q)"
    using assms by (auto simp: not_in_path_image_join)
  ultimately obtain a where "homotopic_paths (- {ζ}) (p +++ reversepath q) (linepath a a)"
    using winding_number_homotopic_paths_null_explicit_eq by blast
  then show ?rhs
    using homotopic_paths_imp_pathstart assms
    by (fastforce simp add: dest: homotopic_paths_imp_homotopic_loops homotopic_paths_loop_parts)
next
  assume ?rhs
  then show ?lhs
    by (simp add: winding_number_homotopic_paths)
qed


lemma winding_number_homotopic_loops_eq:
  assumes "path p" and ζp: "ζ ∉ path_image p"
      and "path q" and ζq: "ζ ∉ path_image q"
      and loops: "pathfinish p = pathstart p" "pathfinish q = pathstart q"
    shows "winding_number p ζ = winding_number q ζ ⟷ homotopic_loops (-{ζ}) p q"
    (is "?lhs = ?rhs")
proof
  assume L: ?lhs
  have "pathstart p ≠ ζ" "pathstart q ≠ ζ"
    using ζp ζq by blast+
  moreover have "path_connected (-{ζ})"
    by (simp add: path_connected_punctured_universe)
  ultimately obtain r where "path r" and rim: "path_image r ⊆ -{ζ}"
                        and pas: "pathstart r = pathstart p" and paf: "pathfinish r = pathstart q"
    by (auto simp: path_connected_def)
  then have "pathstart r ≠ ζ" by blast
  have "homotopic_loops (- {ζ}) p (r +++ q +++ reversepath r)"
  proof (rule homotopic_paths_imp_homotopic_loops)
    show "homotopic_paths (- {ζ}) p (r +++ q +++ reversepath r)"
      by (metis (mono_tags, hide_lams) ‹path r› L ζp ζq ‹path p› ‹path q› homotopic_loops_conjugate loops not_in_path_image_join paf pas path_image_reversepath path_imp_reversepath path_join_eq pathfinish_join pathfinish_reversepath  pathstart_join pathstart_reversepath rim subset_Compl_singleton winding_number_homotopic_loops winding_number_homotopic_paths_eq)
  qed (use loops pas in auto)
  moreover have "homotopic_loops (- {ζ}) (r +++ q +++ reversepath r) q"
    using rim ζq by (auto simp: homotopic_loops_conjugate paf ‹path q› ‹path r› loops)
  ultimately show ?rhs
    using homotopic_loops_trans by metis
next
  assume ?rhs
  then show ?lhs
    by (simp add: winding_number_homotopic_loops)
qed

end