src/HOL/Analysis/Winding_Numbers.thy
 author wenzelm Mon Mar 25 17:21:26 2019 +0100 (2 months ago) changeset 69981 3dced198b9ec parent 69918 eddcc7c726f3 child 69986 f2d327275065 permissions -rw-r--r--
more strict AFP properties;
```     1 section \<open>Winding Numbers\<close>
```
```     2
```
```     3 text\<open>By John Harrison et al.  Ported from HOL Light by L C Paulson (2017)\<close>
```
```     4
```
```     5 theory Winding_Numbers
```
```     6 imports Polytope Jordan_Curve Riemann_Mapping
```
```     7 begin
```
```     8
```
```     9 lemma simply_connected_inside_simple_path:
```
```    10   fixes p :: "real \<Rightarrow> complex"
```
```    11   shows "simple_path p \<Longrightarrow> simply_connected(inside(path_image p))"
```
```    12   using Jordan_inside_outside connected_simple_path_image inside_simple_curve_imp_closed simply_connected_eq_frontier_properties
```
```    13   by fastforce
```
```    14
```
```    15 lemma simply_connected_Int:
```
```    16   fixes S :: "complex set"
```
```    17   assumes "open S" "open T" "simply_connected S" "simply_connected T" "connected (S \<inter> T)"
```
```    18   shows "simply_connected (S \<inter> T)"
```
```    19   using assms by (force simp: simply_connected_eq_winding_number_zero open_Int)
```
```    20
```
```    21 subsection\<open>Winding number for a triangle\<close>
```
```    22
```
```    23 lemma wn_triangle1:
```
```    24   assumes "0 \<in> interior(convex hull {a,b,c})"
```
```    25     shows "\<not> (Im(a/b) \<le> 0 \<and> 0 \<le> Im(b/c))"
```
```    26 proof -
```
```    27   { assume 0: "Im(a/b) \<le> 0" "0 \<le> Im(b/c)"
```
```    28     have "0 \<notin> interior (convex hull {a,b,c})"
```
```    29     proof (cases "a=0 \<or> b=0 \<or> c=0")
```
```    30       case True then show ?thesis
```
```    31         by (auto simp: not_in_interior_convex_hull_3)
```
```    32     next
```
```    33       case False
```
```    34       then have "b \<noteq> 0" by blast
```
```    35       { fix x y::complex and u::real
```
```    36         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"
```
```    37         then have "((1 - u) * Im x) * Re b \<le> Im b * ((1 - u) * Re x)"
```
```    38           by (simp add: mult_left_mono mult.assoc mult.left_commute [of "Im b"])
```
```    39         then have "((1 - u) * Im x + u * Im y) * Re b \<le> Im b * ((1 - u) * Re x + u * Re y)"
```
```    40           using eq_f' ordered_comm_semiring_class.comm_mult_left_mono
```
```    41           by (fastforce simp add: algebra_simps)
```
```    42       }
```
```    43       with False 0 have "convex hull {a,b,c} \<le> {z. Im z * Re b \<le> Im b * Re z}"
```
```    44         apply (simp add: Complex.Im_divide divide_simps complex_neq_0 [symmetric])
```
```    45         apply (simp add: algebra_simps)
```
```    46         apply (rule hull_minimal)
```
```    47         apply (auto simp: algebra_simps convex_alt)
```
```    48         done
```
```    49       moreover have "0 \<notin> interior({z. Im z * Re b \<le> Im b * Re z})"
```
```    50       proof
```
```    51         assume "0 \<in> interior {z. Im z * Re b \<le> Im b * Re z}"
```
```    52         then obtain e where "e>0" and e: "ball 0 e \<subseteq> {z. Im z * Re b \<le> Im b * Re z}"
```
```    53           by (meson mem_interior)
```
```    54         define z where "z \<equiv> - sgn (Im b) * (e/3) + sgn (Re b) * (e/3) * \<i>"
```
```    55         have "z \<in> ball 0 e"
```
```    56           using \<open>e>0\<close>
```
```    57           apply (simp add: z_def dist_norm)
```
```    58           apply (rule le_less_trans [OF norm_triangle_ineq4])
```
```    59           apply (simp add: norm_mult abs_sgn_eq)
```
```    60           done
```
```    61         then have "z \<in> {z. Im z * Re b \<le> Im b * Re z}"
```
```    62           using e by blast
```
```    63         then show False
```
```    64           using \<open>e>0\<close> \<open>b \<noteq> 0\<close>
```
```    65           apply (simp add: z_def dist_norm sgn_if less_eq_real_def mult_less_0_iff complex.expand split: if_split_asm)
```
```    66           apply (auto simp: algebra_simps)
```
```    67           apply (meson less_asym less_trans mult_pos_pos neg_less_0_iff_less)
```
```    68           by (metis less_asym mult_pos_pos neg_less_0_iff_less)
```
```    69       qed
```
```    70       ultimately show ?thesis
```
```    71         using interior_mono by blast
```
```    72     qed
```
```    73   } with assms show ?thesis by blast
```
```    74 qed
```
```    75
```
```    76 lemma wn_triangle2_0:
```
```    77   assumes "0 \<in> interior(convex hull {a,b,c})"
```
```    78   shows
```
```    79        "0 < Im((b - a) * cnj (b)) \<and>
```
```    80         0 < Im((c - b) * cnj (c)) \<and>
```
```    81         0 < Im((a - c) * cnj (a))
```
```    82         \<or>
```
```    83         Im((b - a) * cnj (b)) < 0 \<and>
```
```    84         0 < Im((b - c) * cnj (b)) \<and>
```
```    85         0 < Im((a - b) * cnj (a)) \<and>
```
```    86         0 < Im((c - a) * cnj (c))"
```
```    87 proof -
```
```    88   have [simp]: "{b,c,a} = {a,b,c}" "{c,a,b} = {a,b,c}" by auto
```
```    89   show ?thesis
```
```    90     using wn_triangle1 [OF assms] wn_triangle1 [of b c a] wn_triangle1 [of c a b] assms
```
```    91     by (auto simp: algebra_simps Im_complex_div_gt_0 Im_complex_div_lt_0 not_le not_less)
```
```    92 qed
```
```    93
```
```    94 lemma wn_triangle2:
```
```    95   assumes "z \<in> interior(convex hull {a,b,c})"
```
```    96    shows "0 < Im((b - a) * cnj (b - z)) \<and>
```
```    97           0 < Im((c - b) * cnj (c - z)) \<and>
```
```    98           0 < Im((a - c) * cnj (a - z))
```
```    99           \<or>
```
```   100           Im((b - a) * cnj (b - z)) < 0 \<and>
```
```   101           0 < Im((b - c) * cnj (b - z)) \<and>
```
```   102           0 < Im((a - b) * cnj (a - z)) \<and>
```
```   103           0 < Im((c - a) * cnj (c - z))"
```
```   104 proof -
```
```   105   have 0: "0 \<in> interior(convex hull {a-z, b-z, c-z})"
```
```   106     using assms convex_hull_translation [of "-z" "{a,b,c}"]
```
```   107                 interior_translation [of "-z"]
```
```   108     by (simp cong: image_cong_simp)
```
```   109   show ?thesis using wn_triangle2_0 [OF 0]
```
```   110     by simp
```
```   111 qed
```
```   112
```
```   113 lemma wn_triangle3:
```
```   114   assumes z: "z \<in> interior(convex hull {a,b,c})"
```
```   115       and "0 < Im((b-a) * cnj (b-z))"
```
```   116           "0 < Im((c-b) * cnj (c-z))"
```
```   117           "0 < Im((a-c) * cnj (a-z))"
```
```   118     shows "winding_number (linepath a b +++ linepath b c +++ linepath c a) z = 1"
```
```   119 proof -
```
```   120   have znot[simp]: "z \<notin> closed_segment a b" "z \<notin> closed_segment b c" "z \<notin> closed_segment c a"
```
```   121     using z interior_of_triangle [of a b c]
```
```   122     by (auto simp: closed_segment_def)
```
```   123   have gt0: "0 < Re (winding_number (linepath a b +++ linepath b c +++ linepath c a) z)"
```
```   124     using assms
```
```   125     by (simp add: winding_number_linepath_pos_lt path_image_join winding_number_join_pos_combined)
```
```   126   have lt2: "Re (winding_number (linepath a b +++ linepath b c +++ linepath c a) z) < 2"
```
```   127     using winding_number_lt_half_linepath [of _ a b]
```
```   128     using winding_number_lt_half_linepath [of _ b c]
```
```   129     using winding_number_lt_half_linepath [of _ c a] znot
```
```   130     apply (fastforce simp add: winding_number_join path_image_join)
```
```   131     done
```
```   132   show ?thesis
```
```   133     by (rule winding_number_eq_1) (simp_all add: path_image_join gt0 lt2)
```
```   134 qed
```
```   135
```
```   136 proposition winding_number_triangle:
```
```   137   assumes z: "z \<in> interior(convex hull {a,b,c})"
```
```   138     shows "winding_number(linepath a b +++ linepath b c +++ linepath c a) z =
```
```   139            (if 0 < Im((b - a) * cnj (b - z)) then 1 else -1)"
```
```   140 proof -
```
```   141   have [simp]: "{a,c,b} = {a,b,c}"  by auto
```
```   142   have znot[simp]: "z \<notin> closed_segment a b" "z \<notin> closed_segment b c" "z \<notin> closed_segment c a"
```
```   143     using z interior_of_triangle [of a b c]
```
```   144     by (auto simp: closed_segment_def)
```
```   145   then have [simp]: "z \<notin> closed_segment b a" "z \<notin> closed_segment c b" "z \<notin> closed_segment a c"
```
```   146     using closed_segment_commute by blast+
```
```   147   have *: "winding_number (linepath a b +++ linepath b c +++ linepath c a) z =
```
```   148             winding_number (reversepath (linepath a c +++ linepath c b +++ linepath b a)) z"
```
```   149     by (simp add: reversepath_joinpaths winding_number_join not_in_path_image_join)
```
```   150   show ?thesis
```
```   151     using wn_triangle2 [OF z] apply (rule disjE)
```
```   152     apply (simp add: wn_triangle3 z)
```
```   153     apply (simp add: path_image_join winding_number_reversepath * wn_triangle3 z)
```
```   154     done
```
```   155 qed
```
```   156
```
```   157 subsection\<open>Winding numbers for simple closed paths\<close>
```
```   158
```
```   159 lemma winding_number_from_innerpath:
```
```   160   assumes "simple_path c1" and c1: "pathstart c1 = a" "pathfinish c1 = b"
```
```   161       and "simple_path c2" and c2: "pathstart c2 = a" "pathfinish c2 = b"
```
```   162       and "simple_path c" and c: "pathstart c = a" "pathfinish c = b"
```
```   163       and c1c2: "path_image c1 \<inter> path_image c2 = {a,b}"
```
```   164       and c1c:  "path_image c1 \<inter> path_image c = {a,b}"
```
```   165       and c2c:  "path_image c2 \<inter> path_image c = {a,b}"
```
```   166       and ne_12: "path_image c \<inter> inside(path_image c1 \<union> path_image c2) \<noteq> {}"
```
```   167       and z: "z \<in> inside(path_image c1 \<union> path_image c)"
```
```   168       and wn_d: "winding_number (c1 +++ reversepath c) z = d"
```
```   169       and "a \<noteq> b" "d \<noteq> 0"
```
```   170   obtains "z \<in> inside(path_image c1 \<union> path_image c2)" "winding_number (c1 +++ reversepath c2) z = d"
```
```   171 proof -
```
```   172   obtain 0: "inside(path_image c1 \<union> path_image c) \<inter> inside(path_image c2 \<union> path_image c) = {}"
```
```   173      and 1: "inside(path_image c1 \<union> path_image c) \<union> inside(path_image c2 \<union> path_image c) \<union>
```
```   174              (path_image c - {a,b}) = inside(path_image c1 \<union> path_image c2)"
```
```   175     by (rule split_inside_simple_closed_curve
```
```   176               [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])
```
```   177   have znot: "z \<notin> path_image c"  "z \<notin> path_image c1" "z \<notin> path_image c2"
```
```   178     using union_with_outside z 1 by auto
```
```   179   have wn_cc2: "winding_number (c +++ reversepath c2) z = 0"
```
```   180     apply (rule winding_number_zero_in_outside)
```
```   181     apply (simp_all add: \<open>simple_path c2\<close> c c2 \<open>simple_path c\<close> simple_path_imp_path path_image_join)
```
```   182     by (metis "0" ComplI UnE disjoint_iff_not_equal sup.commute union_with_inside z znot)
```
```   183   show ?thesis
```
```   184   proof
```
```   185     show "z \<in> inside (path_image c1 \<union> path_image c2)"
```
```   186       using "1" z by blast
```
```   187     have "winding_number c1 z - winding_number c z = d "
```
```   188       using assms znot
```
```   189       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)
```
```   190     then show "winding_number (c1 +++ reversepath c2) z = d"
```
```   191       using wn_cc2 by (simp add: winding_number_join simple_path_imp_path assms znot winding_number_reversepath)
```
```   192   qed
```
```   193 qed
```
```   194
```
```   195 lemma simple_closed_path_wn1:
```
```   196   fixes a::complex and e::real
```
```   197   assumes "0 < e"
```
```   198     and sp_pl: "simple_path(p +++ linepath (a - e) (a + e))"
```
```   199     and psp:   "pathstart p = a + e"
```
```   200     and pfp:   "pathfinish p = a - e"
```
```   201     and disj:  "ball a e \<inter> path_image p = {}"
```
```   202 obtains z where "z \<in> inside (path_image (p +++ linepath (a - e) (a + e)))"
```
```   203                 "cmod (winding_number (p +++ linepath (a - e) (a + e)) z) = 1"
```
```   204 proof -
```
```   205   have "arc p" and arc_lp: "arc (linepath (a - e) (a + e))"
```
```   206     and pap: "path_image p \<inter> path_image (linepath (a - e) (a + e)) \<subseteq> {pathstart p, a-e}"
```
```   207     using simple_path_join_loop_eq [of "linepath (a - e) (a + e)" p] assms by auto
```
```   208   have mid_eq_a: "midpoint (a - e) (a + e) = a"
```
```   209     by (simp add: midpoint_def)
```
```   210   then have "a \<in> path_image(p +++ linepath (a - e) (a + e))"
```
```   211     apply (simp add: assms path_image_join)
```
```   212     by (metis midpoint_in_closed_segment)
```
```   213   have "a \<in> frontier(inside (path_image(p +++ linepath (a - e) (a + e))))"
```
```   214     apply (simp add: assms Jordan_inside_outside)
```
```   215     apply (simp_all add: assms path_image_join)
```
```   216     by (metis mid_eq_a midpoint_in_closed_segment)
```
```   217   with \<open>0 < e\<close> obtain c where c: "c \<in> inside (path_image(p +++ linepath (a - e) (a + e)))"
```
```   218                   and dac: "dist a c < e"
```
```   219     by (auto simp: frontier_straddle)
```
```   220   then have "c \<notin> path_image(p +++ linepath (a - e) (a + e))"
```
```   221     using inside_no_overlap by blast
```
```   222   then have "c \<notin> path_image p"
```
```   223             "c \<notin> closed_segment (a - of_real e) (a + of_real e)"
```
```   224     by (simp_all add: assms path_image_join)
```
```   225   with \<open>0 < e\<close> dac have "c \<notin> affine hull {a - of_real e, a + of_real e}"
```
```   226     by (simp add: segment_as_ball not_le)
```
```   227   with \<open>0 < e\<close> have *: "\<not> collinear {a - e, c,a + e}"
```
```   228     using collinear_3_affine_hull [of "a-e" "a+e"] by (auto simp: insert_commute)
```
```   229   have 13: "1/3 + 1/3 + 1/3 = (1::real)" by simp
```
```   230   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})"
```
```   231     using interior_convex_hull_3_minimal [OF * DIM_complex]
```
```   232     by clarsimp (metis 13 zero_less_divide_1_iff zero_less_numeral)
```
```   233   then obtain z where z: "z \<in> interior(convex hull {a - e, c, a + e})" by force
```
```   234   have [simp]: "z \<notin> closed_segment (a - e) c"
```
```   235     by (metis DIM_complex Diff_iff IntD2 inf_sup_absorb interior_of_triangle z)
```
```   236   have [simp]: "z \<notin> closed_segment (a + e) (a - e)"
```
```   237     by (metis DIM_complex DiffD2 Un_iff interior_of_triangle z)
```
```   238   have [simp]: "z \<notin> closed_segment c (a + e)"
```
```   239     by (metis (no_types, lifting) DIM_complex DiffD2 Un_insert_right inf_sup_aci(5) insertCI interior_of_triangle mk_disjoint_insert z)
```
```   240   show thesis
```
```   241   proof
```
```   242     have "norm (winding_number (linepath (a - e) c +++ linepath c (a + e) +++ linepath (a + e) (a - e)) z) = 1"
```
```   243       using winding_number_triangle [OF z] by simp
```
```   244     have zin: "z \<in> inside (path_image (linepath (a + e) (a - e)) \<union> path_image p)"
```
```   245       and zeq: "winding_number (linepath (a + e) (a - e) +++ reversepath p) z =
```
```   246                 winding_number (linepath (a - e) c +++ linepath c (a + e) +++ linepath (a + e) (a - e)) z"
```
```   247     proof (rule winding_number_from_innerpath
```
```   248         [of "linepath (a + e) (a - e)" "a+e" "a-e" p
```
```   249           "linepath (a + e) c +++ linepath c (a - e)" z
```
```   250           "winding_number (linepath (a - e)  c +++ linepath  c (a + e) +++ linepath (a + e) (a - e)) z"])
```
```   251       show sp_aec: "simple_path (linepath (a + e) c +++ linepath c (a - e))"
```
```   252       proof (rule arc_imp_simple_path [OF arc_join])
```
```   253         show "arc (linepath (a + e) c)"
```
```   254           by (metis \<open>c \<notin> path_image p\<close> arc_linepath pathstart_in_path_image psp)
```
```   255         show "arc (linepath c (a - e))"
```
```   256           by (metis \<open>c \<notin> path_image p\<close> arc_linepath pathfinish_in_path_image pfp)
```
```   257         show "path_image (linepath (a + e) c) \<inter> path_image (linepath c (a - e)) \<subseteq> {pathstart (linepath c (a - e))}"
```
```   258           by clarsimp (metis "*" IntI Int_closed_segment closed_segment_commute singleton_iff)
```
```   259       qed auto
```
```   260       show "simple_path p"
```
```   261         using \<open>arc p\<close> arc_simple_path by blast
```
```   262       show sp_ae2: "simple_path (linepath (a + e) (a - e))"
```
```   263         using \<open>arc p\<close> arc_distinct_ends pfp psp by fastforce
```
```   264       show pa: "pathfinish (linepath (a + e) (a - e)) = a - e"
```
```   265            "pathstart (linepath (a + e) c +++ linepath c (a - e)) = a + e"
```
```   266            "pathfinish (linepath (a + e) c +++ linepath c (a - e)) = a - e"
```
```   267            "pathstart p = a + e" "pathfinish p = a - e"
```
```   268            "pathstart (linepath (a + e) (a - e)) = a + e"
```
```   269         by (simp_all add: assms)
```
```   270       show 1: "path_image (linepath (a + e) (a - e)) \<inter> path_image p = {a + e, a - e}"
```
```   271       proof
```
```   272         show "path_image (linepath (a + e) (a - e)) \<inter> path_image p \<subseteq> {a + e, a - e}"
```
```   273           using pap closed_segment_commute psp segment_convex_hull by fastforce
```
```   274         show "{a + e, a - e} \<subseteq> path_image (linepath (a + e) (a - e)) \<inter> path_image p"
```
```   275           using pap pathfinish_in_path_image pathstart_in_path_image pfp psp by fastforce
```
```   276       qed
```
```   277       show 2: "path_image (linepath (a + e) (a - e)) \<inter> path_image (linepath (a + e) c +++ linepath c (a - e)) =
```
```   278                {a + e, a - e}"  (is "?lhs = ?rhs")
```
```   279       proof
```
```   280         have "\<not> collinear {c, a + e, a - e}"
```
```   281           using * by (simp add: insert_commute)
```
```   282         then have "convex hull {a + e, a - e} \<inter> convex hull {a + e, c} = {a + e}"
```
```   283                   "convex hull {a + e, a - e} \<inter> convex hull {c, a - e} = {a - e}"
```
```   284           by (metis (full_types) Int_closed_segment insert_commute segment_convex_hull)+
```
```   285         then show "?lhs \<subseteq> ?rhs"
```
```   286           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)
```
```   287         show "?rhs \<subseteq> ?lhs"
```
```   288           using segment_convex_hull by (simp add: path_image_join)
```
```   289       qed
```
```   290       have "path_image p \<inter> path_image (linepath (a + e) c) \<subseteq> {a + e}"
```
```   291       proof (clarsimp simp: path_image_join)
```
```   292         fix x
```
```   293         assume "x \<in> path_image p" and x_ac: "x \<in> closed_segment (a + e) c"
```
```   294         then have "dist x a \<ge> e"
```
```   295           by (metis IntI all_not_in_conv disj dist_commute mem_ball not_less)
```
```   296         with x_ac dac \<open>e > 0\<close> show "x = a + e"
```
```   297           by (auto simp: norm_minus_commute dist_norm closed_segment_eq_open dest: open_segment_furthest_le [where y=a])
```
```   298       qed
```
```   299       moreover
```
```   300       have "path_image p \<inter> path_image (linepath c (a - e)) \<subseteq> {a - e}"
```
```   301       proof (clarsimp simp: path_image_join)
```
```   302         fix x
```
```   303         assume "x \<in> path_image p" and x_ac: "x \<in> closed_segment c (a - e)"
```
```   304         then have "dist x a \<ge> e"
```
```   305           by (metis IntI all_not_in_conv disj dist_commute mem_ball not_less)
```
```   306         with x_ac dac \<open>e > 0\<close> show "x = a - e"
```
```   307           by (auto simp: norm_minus_commute dist_norm closed_segment_eq_open dest: open_segment_furthest_le [where y=a])
```
```   308       qed
```
```   309       ultimately
```
```   310       have "path_image p \<inter> path_image (linepath (a + e) c +++ linepath c (a - e)) \<subseteq> {a + e, a - e}"
```
```   311         by (force simp: path_image_join)
```
```   312       then show 3: "path_image p \<inter> path_image (linepath (a + e) c +++ linepath c (a - e)) = {a + e, a - e}"
```
```   313         apply (rule equalityI)
```
```   314         apply (clarsimp simp: path_image_join)
```
```   315         apply (metis pathstart_in_path_image psp pathfinish_in_path_image pfp)
```
```   316         done
```
```   317       show 4: "path_image (linepath (a + e) c +++ linepath c (a - e)) \<inter>
```
```   318                inside (path_image (linepath (a + e) (a - e)) \<union> path_image p) \<noteq> {}"
```
```   319         apply (clarsimp simp: path_image_join segment_convex_hull disjoint_iff_not_equal)
```
```   320         by (metis (no_types, hide_lams) UnI1 Un_commute c closed_segment_commute ends_in_segment(1) path_image_join
```
```   321                   path_image_linepath pathstart_linepath pfp segment_convex_hull)
```
```   322       show zin_inside: "z \<in> inside (path_image (linepath (a + e) (a - e)) \<union>
```
```   323                                     path_image (linepath (a + e) c +++ linepath c (a - e)))"
```
```   324         apply (simp add: path_image_join)
```
```   325         by (metis z inside_of_triangle DIM_complex Un_commute closed_segment_commute)
```
```   326       show 5: "winding_number
```
```   327              (linepath (a + e) (a - e) +++ reversepath (linepath (a + e) c +++ linepath c (a - e))) z =
```
```   328             winding_number (linepath (a - e) c +++ linepath c (a + e) +++ linepath (a + e) (a - e)) z"
```
```   329         by (simp add: reversepath_joinpaths path_image_join winding_number_join)
```
```   330       show 6: "winding_number (linepath (a - e) c +++ linepath c (a + e) +++ linepath (a + e) (a - e)) z \<noteq> 0"
```
```   331         by (simp add: winding_number_triangle z)
```
```   332       show "winding_number (linepath (a + e) (a - e) +++ reversepath p) z =
```
```   333             winding_number (linepath (a - e) c +++ linepath c (a + e) +++ linepath (a + e) (a - e)) z"
```
```   334         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)
```
```   335     qed (use assms \<open>e > 0\<close> in auto)
```
```   336     show "z \<in> inside (path_image (p +++ linepath (a - e) (a + e)))"
```
```   337       using zin by (simp add: assms path_image_join Un_commute closed_segment_commute)
```
```   338     then have "cmod (winding_number (p +++ linepath (a - e) (a + e)) z) =
```
```   339                cmod ((winding_number(reversepath (p +++ linepath (a - e) (a + e))) z))"
```
```   340       apply (subst winding_number_reversepath)
```
```   341       using simple_path_imp_path sp_pl apply blast
```
```   342        apply (metis IntI emptyE inside_no_overlap)
```
```   343       by (simp add: inside_def)
```
```   344     also have "... = cmod (winding_number(linepath (a + e) (a - e) +++ reversepath p) z)"
```
```   345       by (simp add: pfp reversepath_joinpaths)
```
```   346     also have "... = cmod (winding_number (linepath (a - e) c +++ linepath c (a + e) +++ linepath (a + e) (a - e)) z)"
```
```   347       by (simp add: zeq)
```
```   348     also have "... = 1"
```
```   349       using z by (simp add: interior_of_triangle winding_number_triangle)
```
```   350     finally show "cmod (winding_number (p +++ linepath (a - e) (a + e)) z) = 1" .
```
```   351   qed
```
```   352 qed
```
```   353
```
```   354 lemma simple_closed_path_wn2:
```
```   355   fixes a::complex and d e::real
```
```   356   assumes "0 < d" "0 < e"
```
```   357     and sp_pl: "simple_path(p +++ linepath (a - d) (a + e))"
```
```   358     and psp:   "pathstart p = a + e"
```
```   359     and pfp:   "pathfinish p = a - d"
```
```   360 obtains z where "z \<in> inside (path_image (p +++ linepath (a - d) (a + e)))"
```
```   361                 "cmod (winding_number (p +++ linepath (a - d) (a + e)) z) = 1"
```
```   362 proof -
```
```   363   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
```
```   364     using closed_segment_translation_eq [of a]
```
```   365     by (metis (no_types, hide_lams) add_uminus_conv_diff of_real_minus of_real_closed_segment)
```
```   366   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
```
```   367     by (metis closed_segment_translation_eq diff_conv_add_uminus of_real_closed_segment of_real_minus)
```
```   368   have "arc p" and arc_lp: "arc (linepath (a - d) (a + e))" and "path p"
```
```   369     and pap: "path_image p \<inter> closed_segment (a - d) (a + e) \<subseteq> {a+e, a-d}"
```
```   370     using simple_path_join_loop_eq [of "linepath (a - d) (a + e)" p] assms arc_imp_path  by auto
```
```   371   have "0 \<in> closed_segment (-d) e"
```
```   372     using \<open>0 < d\<close> \<open>0 < e\<close> closed_segment_eq_real_ivl by auto
```
```   373   then have "a \<in> path_image (linepath (a - d) (a + e))"
```
```   374     using of_real_closed_segment [THEN iffD2]
```
```   375     by (force dest: closed_segment_translation_eq [of a, THEN iffD2] simp del: of_real_closed_segment)
```
```   376   then have "a \<notin> path_image p"
```
```   377     using \<open>0 < d\<close> \<open>0 < e\<close> pap by auto
```
```   378   then obtain k where "0 < k" and k: "ball a k \<inter> (path_image p) = {}"
```
```   379     using \<open>0 < e\<close> \<open>path p\<close> not_on_path_ball by blast
```
```   380   define kde where "kde \<equiv> (min k (min d e)) / 2"
```
```   381   have "0 < kde" "kde < k" "kde < d" "kde < e"
```
```   382     using \<open>0 < k\<close> \<open>0 < d\<close> \<open>0 < e\<close> by (auto simp: kde_def)
```
```   383   let ?q = "linepath (a + kde) (a + e) +++ p +++ linepath (a - d) (a - kde)"
```
```   384   have "- kde \<in> closed_segment (-d) e"
```
```   385     using \<open>0 < kde\<close> \<open>kde < d\<close> \<open>kde < e\<close> closed_segment_eq_real_ivl by auto
```
```   386   then have a_diff_kde: "a - kde \<in> closed_segment (a - d) (a + e)"
```
```   387     using of_real_closed_segment [THEN iffD2]
```
```   388     by (force dest: closed_segment_translation_eq [of a, THEN iffD2] simp del: of_real_closed_segment)
```
```   389   then have clsub2: "closed_segment (a - d) (a - kde) \<subseteq> closed_segment (a - d) (a + e)"
```
```   390     by (simp add: subset_closed_segment)
```
```   391   then have "path_image p \<inter> closed_segment (a - d) (a - kde) \<subseteq> {a + e, a - d}"
```
```   392     using pap by force
```
```   393   moreover
```
```   394   have "a + e \<notin> path_image p \<inter> closed_segment (a - d) (a - kde)"
```
```   395     using \<open>0 < kde\<close> \<open>kde < d\<close> \<open>0 < e\<close> by (auto simp: closed_segment_eq_real_ivl)
```
```   396   ultimately have sub_a_diff_d: "path_image p \<inter> closed_segment (a - d) (a - kde) \<subseteq> {a - d}"
```
```   397     by blast
```
```   398   have "kde \<in> closed_segment (-d) e"
```
```   399     using \<open>0 < kde\<close> \<open>kde < d\<close> \<open>kde < e\<close> closed_segment_eq_real_ivl by auto
```
```   400   then have a_diff_kde: "a + kde \<in> closed_segment (a - d) (a + e)"
```
```   401     using of_real_closed_segment [THEN iffD2]
```
```   402     by (force dest: closed_segment_translation_eq [of "a", THEN iffD2] simp del: of_real_closed_segment)
```
```   403   then have clsub1: "closed_segment (a + kde) (a + e) \<subseteq> closed_segment (a - d) (a + e)"
```
```   404     by (simp add: subset_closed_segment)
```
```   405   then have "closed_segment (a + kde) (a + e) \<inter> path_image p \<subseteq> {a + e, a - d}"
```
```   406     using pap by force
```
```   407   moreover
```
```   408   have "closed_segment (a + kde) (a + e) \<inter> closed_segment (a - d) (a - kde) = {}"
```
```   409   proof (clarsimp intro!: equals0I)
```
```   410     fix y
```
```   411     assume y1: "y \<in> closed_segment (a + kde) (a + e)"
```
```   412        and y2: "y \<in> closed_segment (a - d) (a - kde)"
```
```   413     obtain u where u: "y = a + of_real u" and "0 < u"
```
```   414       using y1 \<open>0 < kde\<close> \<open>kde < e\<close> \<open>0 < e\<close> apply (clarsimp simp: in_segment)
```
```   415       apply (rule_tac u = "(1 - u)*kde + u*e" in that)
```
```   416        apply (auto simp: scaleR_conv_of_real algebra_simps)
```
```   417       by (meson le_less_trans less_add_same_cancel2 less_eq_real_def mult_left_mono)
```
```   418     moreover
```
```   419     obtain v where v: "y = a + of_real v" and "v \<le> 0"
```
```   420       using y2 \<open>0 < kde\<close> \<open>0 < d\<close> \<open>0 < e\<close> apply (clarsimp simp: in_segment)
```
```   421       apply (rule_tac v = "- ((1 - u)*d + u*kde)" in that)
```
```   422        apply (force simp: scaleR_conv_of_real algebra_simps)
```
```   423       by (meson less_eq_real_def neg_le_0_iff_le segment_bound_lemma)
```
```   424     ultimately show False
```
```   425       by auto
```
```   426   qed
```
```   427   moreover have "a - d \<notin> closed_segment (a + kde) (a + e)"
```
```   428     using \<open>0 < kde\<close> \<open>kde < d\<close> \<open>0 < e\<close> by (auto simp: closed_segment_eq_real_ivl)
```
```   429   ultimately have sub_a_plus_e:
```
```   430     "closed_segment (a + kde) (a + e) \<inter> (path_image p \<union> closed_segment (a - d) (a - kde))
```
```   431        \<subseteq> {a + e}"
```
```   432     by auto
```
```   433   have "kde \<in> closed_segment (-kde) e"
```
```   434     using \<open>0 < kde\<close> \<open>kde < d\<close> \<open>kde < e\<close> closed_segment_eq_real_ivl by auto
```
```   435   then have a_add_kde: "a + kde \<in> closed_segment (a - kde) (a + e)"
```
```   436     using of_real_closed_segment [THEN iffD2]
```
```   437     by (force dest: closed_segment_translation_eq [of "a", THEN iffD2] simp del: of_real_closed_segment)
```
```   438   have "closed_segment (a - kde) (a + kde) \<inter> closed_segment (a + kde) (a + e) = {a + kde}"
```
```   439     by (metis a_add_kde Int_closed_segment)
```
```   440   moreover
```
```   441   have "path_image p \<inter> closed_segment (a - kde) (a + kde) = {}"
```
```   442   proof (rule equals0I, clarify)
```
```   443     fix y  assume "y \<in> path_image p" "y \<in> closed_segment (a - kde) (a + kde)"
```
```   444     with equals0D [OF k, of y] \<open>0 < kde\<close> \<open>kde < k\<close> show False
```
```   445       by (auto simp: dist_norm dest: dist_decreases_closed_segment [where c=a])
```
```   446   qed
```
```   447   moreover
```
```   448   have "- kde \<in> closed_segment (-d) kde"
```
```   449     using \<open>0 < kde\<close> \<open>kde < d\<close> \<open>kde < e\<close> closed_segment_eq_real_ivl by auto
```
```   450   then have a_diff_kde': "a - kde \<in> closed_segment (a - d) (a + kde)"
```
```   451     using of_real_closed_segment [THEN iffD2]
```
```   452     by (force dest: closed_segment_translation_eq [of a, THEN iffD2] simp del: of_real_closed_segment)
```
```   453   then have "closed_segment (a - d) (a - kde) \<inter> closed_segment (a - kde) (a + kde) = {a - kde}"
```
```   454     by (metis Int_closed_segment)
```
```   455   ultimately
```
```   456   have pa_subset_pm_kde: "path_image ?q \<inter> closed_segment (a - kde) (a + kde) \<subseteq> {a - kde, a + kde}"
```
```   457     by (auto simp: path_image_join assms)
```
```   458   have ge_kde1: "\<exists>y. x = a + y \<and> y \<ge> kde" if "x \<in> closed_segment (a + kde) (a + e)" for x
```
```   459     using that \<open>kde < e\<close> mult_le_cancel_left
```
```   460     apply (auto simp: in_segment)
```
```   461     apply (rule_tac x="(1-u)*kde + u*e" in exI)
```
```   462     apply (fastforce simp: algebra_simps scaleR_conv_of_real)
```
```   463     done
```
```   464   have ge_kde2: "\<exists>y. x = a + y \<and> y \<le> -kde" if "x \<in> closed_segment (a - d) (a - kde)" for x
```
```   465     using that \<open>kde < d\<close> affine_ineq
```
```   466     apply (auto simp: in_segment)
```
```   467     apply (rule_tac x="- ((1-u)*d + u*kde)" in exI)
```
```   468     apply (fastforce simp: algebra_simps scaleR_conv_of_real)
```
```   469     done
```
```   470   have notin_paq: "x \<notin> path_image ?q" if "dist a x < kde" for x
```
```   471     using that using \<open>0 < kde\<close> \<open>kde < d\<close> \<open>kde < k\<close>
```
```   472     apply (auto simp: path_image_join assms dist_norm dest!: ge_kde1 ge_kde2)
```
```   473     by (meson k disjoint_iff_not_equal le_less_trans less_eq_real_def mem_ball that)
```
```   474   obtain z where zin: "z \<in> inside (path_image (?q +++ linepath (a - kde) (a + kde)))"
```
```   475            and z1: "cmod (winding_number (?q +++ linepath (a - kde) (a + kde)) z) = 1"
```
```   476   proof (rule simple_closed_path_wn1 [of kde ?q a])
```
```   477     show "simple_path (?q +++ linepath (a - kde) (a + kde))"
```
```   478     proof (intro simple_path_join_loop conjI)
```
```   479       show "arc ?q"
```
```   480       proof (rule arc_join)
```
```   481         show "arc (linepath (a + kde) (a + e))"
```
```   482           using \<open>kde < e\<close> \<open>arc p\<close> by (force simp: pfp)
```
```   483         show "arc (p +++ linepath (a - d) (a - kde))"
```
```   484           using \<open>kde < d\<close> \<open>kde < e\<close> \<open>arc p\<close> sub_a_diff_d by (force simp: pfp intro: arc_join)
```
```   485       qed (auto simp: psp pfp path_image_join sub_a_plus_e)
```
```   486       show "arc (linepath (a - kde) (a + kde))"
```
```   487         using \<open>0 < kde\<close> by auto
```
```   488     qed (use pa_subset_pm_kde in auto)
```
```   489   qed (use \<open>0 < kde\<close> notin_paq in auto)
```
```   490   have eq: "path_image (?q +++ linepath (a - kde) (a + kde)) = path_image (p +++ linepath (a - d) (a + e))"
```
```   491             (is "?lhs = ?rhs")
```
```   492   proof
```
```   493     show "?lhs \<subseteq> ?rhs"
```
```   494       using clsub1 clsub2 apply (auto simp: path_image_join assms)
```
```   495       by (meson subsetCE subset_closed_segment)
```
```   496     show "?rhs \<subseteq> ?lhs"
```
```   497       apply (simp add: path_image_join assms Un_ac)
```
```   498         by (metis Un_closed_segment Un_assoc a_diff_kde a_diff_kde' le_supI2 subset_refl)
```
```   499     qed
```
```   500   show thesis
```
```   501   proof
```
```   502     show zzin: "z \<in> inside (path_image (p +++ linepath (a - d) (a + e)))"
```
```   503       by (metis eq zin)
```
```   504     then have znotin: "z \<notin> path_image p"
```
```   505       by (metis ComplD Un_iff inside_Un_outside path_image_join pathfinish_linepath pathstart_reversepath pfp reversepath_linepath)
```
```   506     have znotin_de: "z \<notin> closed_segment (a - d) (a + kde)"
```
```   507       by (metis ComplD Un_iff Un_closed_segment a_diff_kde inside_Un_outside path_image_join path_image_linepath pathstart_linepath pfp zzin)
```
```   508     have "winding_number (linepath (a - d) (a + e)) z =
```
```   509           winding_number (linepath (a - d) (a + kde)) z + winding_number (linepath (a + kde) (a + e)) z"
```
```   510       apply (rule winding_number_split_linepath)
```
```   511       apply (simp add: a_diff_kde)
```
```   512       by (metis ComplD Un_iff inside_Un_outside path_image_join path_image_linepath pathstart_linepath pfp zzin)
```
```   513     also have "... = winding_number (linepath (a + kde) (a + e)) z +
```
```   514                      (winding_number (linepath (a - d) (a - kde)) z +
```
```   515                       winding_number (linepath (a - kde) (a + kde)) z)"
```
```   516       by (simp add: winding_number_split_linepath [of "a-kde", symmetric] znotin_de a_diff_kde')
```
```   517     finally have "winding_number (p +++ linepath (a - d) (a + e)) z =
```
```   518                     winding_number p z + winding_number (linepath (a + kde) (a + e)) z +
```
```   519                    (winding_number (linepath (a - d) (a - kde)) z +
```
```   520                     winding_number (linepath (a - kde) (a + kde)) z)"
```
```   521       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)
```
```   522     also have "... = winding_number ?q z + winding_number (linepath (a - kde) (a + kde)) z"
```
```   523       using \<open>path p\<close> znotin assms zzin clsub1
```
```   524       apply (subst winding_number_join, auto)
```
```   525       apply (metis (no_types, hide_lams) ComplD Un_iff contra_subsetD inside_Un_outside path_image_join path_image_linepath pathstart_linepath)
```
```   526       apply (metis Un_iff Un_closed_segment a_diff_kde' not_in_path_image_join path_image_linepath znotin_de)
```
```   527       by (metis Un_iff Un_closed_segment a_diff_kde' path_image_linepath path_linepath pathstart_linepath winding_number_join znotin_de)
```
```   528     also have "... = winding_number (?q +++ linepath (a - kde) (a + kde)) z"
```
```   529       using \<open>path p\<close> assms zin
```
```   530       apply (subst winding_number_join [symmetric], auto)
```
```   531       apply (metis ComplD Un_iff path_image_join pathfinish_join pathfinish_linepath pathstart_linepath union_with_outside)
```
```   532       by (metis Un_iff Un_closed_segment a_diff_kde' znotin_de)
```
```   533     finally have "winding_number (p +++ linepath (a - d) (a + e)) z =
```
```   534                   winding_number (?q +++ linepath (a - kde) (a + kde)) z" .
```
```   535     then show "cmod (winding_number (p +++ linepath (a - d) (a + e)) z) = 1"
```
```   536       by (simp add: z1)
```
```   537   qed
```
```   538 qed
```
```   539
```
```   540 lemma simple_closed_path_wn3:
```
```   541   fixes p :: "real \<Rightarrow> complex"
```
```   542   assumes "simple_path p" and loop: "pathfinish p = pathstart p"
```
```   543   obtains z where "z \<in> inside (path_image p)" "cmod (winding_number p z) = 1"
```
```   544 proof -
```
```   545   have ins: "inside(path_image p) \<noteq> {}" "open(inside(path_image p))"
```
```   546             "connected(inside(path_image p))"
```
```   547    and out: "outside(path_image p) \<noteq> {}" "open(outside(path_image p))"
```
```   548             "connected(outside(path_image p))"
```
```   549    and bo:  "bounded(inside(path_image p))" "\<not> bounded(outside(path_image p))"
```
```   550    and ins_out: "inside(path_image p) \<inter> outside(path_image p) = {}"
```
```   551                 "inside(path_image p) \<union> outside(path_image p) = - path_image p"
```
```   552    and fro: "frontier(inside(path_image p)) = path_image p"
```
```   553             "frontier(outside(path_image p)) = path_image p"
```
```   554     using Jordan_inside_outside [OF assms] by auto
```
```   555   obtain a where a: "a \<in> inside(path_image p)"
```
```   556     using \<open>inside (path_image p) \<noteq> {}\<close> by blast
```
```   557   obtain d::real where "0 < d" and d_fro: "a - d \<in> frontier (inside (path_image p))"
```
```   558                  and d_int: "\<And>\<epsilon>. \<lbrakk>0 \<le> \<epsilon>; \<epsilon> < d\<rbrakk> \<Longrightarrow> (a - \<epsilon>) \<in> inside (path_image p)"
```
```   559     apply (rule ray_to_frontier [of "inside (path_image p)" a "-1"])
```
```   560     using \<open>bounded (inside (path_image p))\<close> \<open>open (inside (path_image p))\<close> a interior_eq
```
```   561        apply (auto simp: of_real_def)
```
```   562     done
```
```   563   obtain e::real where "0 < e" and e_fro: "a + e \<in> frontier (inside (path_image p))"
```
```   564     and e_int: "\<And>\<epsilon>. \<lbrakk>0 \<le> \<epsilon>; \<epsilon> < e\<rbrakk> \<Longrightarrow> (a + \<epsilon>) \<in> inside (path_image p)"
```
```   565     apply (rule ray_to_frontier [of "inside (path_image p)" a 1])
```
```   566     using \<open>bounded (inside (path_image p))\<close> \<open>open (inside (path_image p))\<close> a interior_eq
```
```   567        apply (auto simp: of_real_def)
```
```   568     done
```
```   569   obtain t0 where "0 \<le> t0" "t0 \<le> 1" and pt: "p t0 = a - d"
```
```   570     using a d_fro fro by (auto simp: path_image_def)
```
```   571   obtain q where "simple_path q" and q_ends: "pathstart q = a - d" "pathfinish q = a - d"
```
```   572     and q_eq_p: "path_image q = path_image p"
```
```   573     and wn_q_eq_wn_p: "\<And>z. z \<in> inside(path_image p) \<Longrightarrow> winding_number q z = winding_number p z"
```
```   574   proof
```
```   575     show "simple_path (shiftpath t0 p)"
```
```   576       by (simp add: pathstart_shiftpath pathfinish_shiftpath
```
```   577           simple_path_shiftpath path_image_shiftpath \<open>0 \<le> t0\<close> \<open>t0 \<le> 1\<close> assms)
```
```   578     show "pathstart (shiftpath t0 p) = a - d"
```
```   579       using pt by (simp add: \<open>t0 \<le> 1\<close> pathstart_shiftpath)
```
```   580     show "pathfinish (shiftpath t0 p) = a - d"
```
```   581       by (simp add: \<open>0 \<le> t0\<close> loop pathfinish_shiftpath pt)
```
```   582     show "path_image (shiftpath t0 p) = path_image p"
```
```   583       by (simp add: \<open>0 \<le> t0\<close> \<open>t0 \<le> 1\<close> loop path_image_shiftpath)
```
```   584     show "winding_number (shiftpath t0 p) z = winding_number p z"
```
```   585       if "z \<in> inside (path_image p)" for z
```
```   586       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
```
```   587           loop simple_path_imp_path that winding_number_shiftpath)
```
```   588   qed
```
```   589   have ad_not_ae: "a - d \<noteq> a + e"
```
```   590     by (metis \<open>0 < d\<close> \<open>0 < e\<close> add.left_inverse add_left_cancel add_uminus_conv_diff
```
```   591         le_add_same_cancel2 less_eq_real_def not_less of_real_add of_real_def of_real_eq_0_iff pt)
```
```   592   have ad_ae_q: "{a - d, a + e} \<subseteq> path_image q"
```
```   593     using \<open>path_image q = path_image p\<close> d_fro e_fro fro(1) by auto
```
```   594   have ada: "open_segment (a - d) a \<subseteq> inside (path_image p)"
```
```   595   proof (clarsimp simp: in_segment)
```
```   596     fix u::real assume "0 < u" "u < 1"
```
```   597     with d_int have "a - (1 - u) * d \<in> inside (path_image p)"
```
```   598       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)
```
```   599     then show "(1 - u) *\<^sub>R (a - d) + u *\<^sub>R a \<in> inside (path_image p)"
```
```   600       by (simp add: diff_add_eq of_real_def real_vector.scale_right_diff_distrib)
```
```   601   qed
```
```   602   have aae: "open_segment a (a + e) \<subseteq> inside (path_image p)"
```
```   603   proof (clarsimp simp: in_segment)
```
```   604     fix u::real assume "0 < u" "u < 1"
```
```   605     with e_int have "a + u * e \<in> inside (path_image p)"
```
```   606       by (meson \<open>0 < e\<close> less_eq_real_def mult_less_cancel_right2 not_less zero_less_mult_iff)
```
```   607     then show "(1 - u) *\<^sub>R a + u *\<^sub>R (a + e) \<in> inside (path_image p)"
```
```   608       apply (simp add: algebra_simps)
```
```   609       by (simp add: diff_add_eq of_real_def real_vector.scale_right_diff_distrib)
```
```   610   qed
```
```   611   have "complex_of_real (d * d + (e * e + d * (e + e))) \<noteq> 0"
```
```   612     using ad_not_ae
```
```   613     by (metis \<open>0 < d\<close> \<open>0 < e\<close> add_strict_left_mono less_add_same_cancel1 not_sum_squares_lt_zero
```
```   614         of_real_eq_0_iff zero_less_double_add_iff_zero_less_single_add zero_less_mult_iff)
```
```   615   then have a_in_de: "a \<in> open_segment (a - d) (a + e)"
```
```   616     using ad_not_ae \<open>0 < d\<close> \<open>0 < e\<close>
```
```   617     apply (auto simp: in_segment algebra_simps scaleR_conv_of_real)
```
```   618     apply (rule_tac x="d / (d+e)" in exI)
```
```   619     apply (auto simp: field_simps)
```
```   620     done
```
```   621   then have "open_segment (a - d) (a + e) \<subseteq> inside (path_image p)"
```
```   622     using ada a aae Un_open_segment [of a "a-d" "a+e"] by blast
```
```   623   then have "path_image q \<inter> open_segment (a - d) (a + e) = {}"
```
```   624     using inside_no_overlap by (fastforce simp: q_eq_p)
```
```   625   with ad_ae_q have paq_Int_cs: "path_image q \<inter> closed_segment (a - d) (a + e) = {a - d, a + e}"
```
```   626     by (simp add: closed_segment_eq_open)
```
```   627   obtain t where "0 \<le> t" "t \<le> 1" and qt: "q t = a + e"
```
```   628     using a e_fro fro ad_ae_q by (auto simp: path_defs)
```
```   629   then have "t \<noteq> 0"
```
```   630     by (metis ad_not_ae pathstart_def q_ends(1))
```
```   631   then have "t \<noteq> 1"
```
```   632     by (metis ad_not_ae pathfinish_def q_ends(2) qt)
```
```   633   have q01: "q 0 = a - d" "q 1 = a - d"
```
```   634     using q_ends by (auto simp: pathstart_def pathfinish_def)
```
```   635   obtain z where zin: "z \<in> inside (path_image (subpath t 0 q +++ linepath (a - d) (a + e)))"
```
```   636              and z1: "cmod (winding_number (subpath t 0 q +++ linepath (a - d) (a + e)) z) = 1"
```
```   637   proof (rule simple_closed_path_wn2 [of d e "subpath t 0 q" a], simp_all add: q01)
```
```   638     show "simple_path (subpath t 0 q +++ linepath (a - d) (a + e))"
```
```   639     proof (rule simple_path_join_loop, simp_all add: qt q01)
```
```   640       have "inj_on q (closed_segment t 0)"
```
```   641         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>
```
```   642         by (fastforce simp: simple_path_def inj_on_def closed_segment_eq_real_ivl)
```
```   643       then show "arc (subpath t 0 q)"
```
```   644         using \<open>0 \<le> t\<close> \<open>simple_path q\<close> \<open>t \<le> 1\<close> \<open>t \<noteq> 0\<close>
```
```   645         by (simp add: arc_subpath_eq simple_path_imp_path)
```
```   646       show "arc (linepath (a - d) (a + e))"
```
```   647         by (simp add: ad_not_ae)
```
```   648       show "path_image (subpath t 0 q) \<inter> closed_segment (a - d) (a + e) \<subseteq> {a + e, a - d}"
```
```   649         using qt paq_Int_cs  \<open>simple_path q\<close> \<open>0 \<le> t\<close> \<open>t \<le> 1\<close>
```
```   650         by (force simp: dest: rev_subsetD [OF _ path_image_subpath_subset] intro: simple_path_imp_path)
```
```   651     qed
```
```   652   qed (auto simp: \<open>0 < d\<close> \<open>0 < e\<close> qt)
```
```   653   have pa01_Un: "path_image (subpath 0 t q) \<union> path_image (subpath 1 t q) = path_image q"
```
```   654     unfolding path_image_subpath
```
```   655     using \<open>0 \<le> t\<close> \<open>t \<le> 1\<close> by (force simp: path_image_def image_iff)
```
```   656   with paq_Int_cs have pa_01q:
```
```   657         "(path_image (subpath 0 t q) \<union> path_image (subpath 1 t q)) \<inter> closed_segment (a - d) (a + e) = {a - d, a + e}"
```
```   658     by metis
```
```   659   have z_notin_ed: "z \<notin> closed_segment (a + e) (a - d)"
```
```   660     using zin q01 by (simp add: path_image_join closed_segment_commute inside_def)
```
```   661   have z_notin_0t: "z \<notin> path_image (subpath 0 t q)"
```
```   662     by (metis (no_types, hide_lams) IntI Un_upper1 subsetD empty_iff inside_no_overlap path_image_join
```
```   663         path_image_subpath_commute pathfinish_subpath pathstart_def pathstart_linepath q_ends(1) qt subpath_trivial zin)
```
```   664   have [simp]: "- winding_number (subpath t 0 q) z = winding_number (subpath 0 t q) z"
```
```   665     by (metis \<open>0 \<le> t\<close> \<open>simple_path q\<close> \<open>t \<le> 1\<close> atLeastAtMost_iff zero_le_one
```
```   666               path_image_subpath_commute path_subpath real_eq_0_iff_le_ge_0
```
```   667               reversepath_subpath simple_path_imp_path winding_number_reversepath z_notin_0t)
```
```   668   obtain z_in_q: "z \<in> inside(path_image q)"
```
```   669      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"
```
```   670   proof (rule winding_number_from_innerpath
```
```   671           [of "subpath 0 t q" "a-d" "a+e" "subpath 1 t q" "linepath (a - d) (a + e)"
```
```   672             z "- winding_number (subpath t 0 q +++ linepath (a - d) (a + e)) z"],
```
```   673          simp_all add: q01 qt pa01_Un reversepath_subpath)
```
```   674     show "simple_path (subpath 0 t q)" "simple_path (subpath 1 t q)"
```
```   675       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)
```
```   676     show "simple_path (linepath (a - d) (a + e))"
```
```   677       using ad_not_ae by blast
```
```   678     show "path_image (subpath 0 t q) \<inter> path_image (subpath 1 t q) = {a - d, a + e}"  (is "?lhs = ?rhs")
```
```   679     proof
```
```   680       show "?lhs \<subseteq> ?rhs"
```
```   681         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
```
```   682         by (force simp: pathfinish_def qt simple_path_def path_image_subpath)
```
```   683       show "?rhs \<subseteq> ?lhs"
```
```   684         using \<open>0 \<le> t\<close> \<open>t \<le> 1\<close> q01 qt by (force simp: path_image_subpath)
```
```   685     qed
```
```   686     show "path_image (subpath 0 t q) \<inter> closed_segment (a - d) (a + e) = {a - d, a + e}" (is "?lhs = ?rhs")
```
```   687     proof
```
```   688       show "?lhs \<subseteq> ?rhs"  using paq_Int_cs pa01_Un by fastforce
```
```   689       show "?rhs \<subseteq> ?lhs"  using \<open>0 \<le> t\<close> \<open>t \<le> 1\<close> q01 qt by (force simp: path_image_subpath)
```
```   690     qed
```
```   691     show "path_image (subpath 1 t q) \<inter> closed_segment (a - d) (a + e) = {a - d, a + e}" (is "?lhs = ?rhs")
```
```   692     proof
```
```   693       show "?lhs \<subseteq> ?rhs"  by (auto simp: pa_01q [symmetric])
```
```   694       show "?rhs \<subseteq> ?lhs"  using \<open>0 \<le> t\<close> \<open>t \<le> 1\<close> q01 qt by (force simp: path_image_subpath)
```
```   695     qed
```
```   696     show "closed_segment (a - d) (a + e) \<inter> inside (path_image q) \<noteq> {}"
```
```   697       using a a_in_de open_closed_segment pa01_Un q_eq_p by fastforce
```
```   698     show "z \<in> inside (path_image (subpath 0 t q) \<union> closed_segment (a - d) (a + e))"
```
```   699       by (metis path_image_join path_image_linepath path_image_subpath_commute pathfinish_subpath pathstart_linepath q01(1) zin)
```
```   700     show "winding_number (subpath 0 t q +++ linepath (a + e) (a - d)) z =
```
```   701       - winding_number (subpath t 0 q +++ linepath (a - d) (a + e)) z"
```
```   702       using z_notin_ed z_notin_0t \<open>0 \<le> t\<close> \<open>simple_path q\<close> \<open>t \<le> 1\<close>
```
```   703       by (simp add: simple_path_imp_path qt q01 path_image_subpath_commute closed_segment_commute winding_number_join winding_number_reversepath [symmetric])
```
```   704     show "- d \<noteq> e"
```
```   705       using ad_not_ae by auto
```
```   706     show "winding_number (subpath t 0 q +++ linepath (a - d) (a + e)) z \<noteq> 0"
```
```   707       using z1 by auto
```
```   708   qed
```
```   709   show ?thesis
```
```   710   proof
```
```   711     show "z \<in> inside (path_image p)"
```
```   712       using q_eq_p z_in_q by auto
```
```   713     then have [simp]: "z \<notin> path_image q"
```
```   714       by (metis disjoint_iff_not_equal inside_no_overlap q_eq_p)
```
```   715     have [simp]: "z \<notin> path_image (subpath 1 t q)"
```
```   716       using inside_def pa01_Un z_in_q by fastforce
```
```   717     have "winding_number(subpath 0 t q +++ subpath t 1 q) z = winding_number(subpath 0 1 q) z"
```
```   718       using z_notin_0t \<open>0 \<le> t\<close> \<open>simple_path q\<close> \<open>t \<le> 1\<close>
```
```   719       by (simp add: simple_path_imp_path qt path_image_subpath_commute winding_number_join winding_number_subpath_combine)
```
```   720     with wn_q have "winding_number (subpath t 0 q +++ linepath (a - d) (a + e)) z = - winding_number q z"
```
```   721       by auto
```
```   722     with z1 have "cmod (winding_number q z) = 1"
```
```   723       by simp
```
```   724     with z1 wn_q_eq_wn_p show "cmod (winding_number p z) = 1"
```
```   725       using z1 wn_q_eq_wn_p  by (simp add: \<open>z \<in> inside (path_image p)\<close>)
```
```   726     qed
```
```   727 qed
```
```   728
```
```   729 proposition simple_closed_path_winding_number_inside:
```
```   730   assumes "simple_path \<gamma>"
```
```   731   obtains "\<And>z. z \<in> inside(path_image \<gamma>) \<Longrightarrow> winding_number \<gamma> z = 1"
```
```   732         | "\<And>z. z \<in> inside(path_image \<gamma>) \<Longrightarrow> winding_number \<gamma> z = -1"
```
```   733 proof (cases "pathfinish \<gamma> = pathstart \<gamma>")
```
```   734   case True
```
```   735   have "path \<gamma>"
```
```   736     by (simp add: assms simple_path_imp_path)
```
```   737   then have const: "winding_number \<gamma> constant_on inside(path_image \<gamma>)"
```
```   738   proof (rule winding_number_constant)
```
```   739     show "connected (inside(path_image \<gamma>))"
```
```   740       by (simp add: Jordan_inside_outside True assms)
```
```   741   qed (use inside_no_overlap True in auto)
```
```   742   obtain z where zin: "z \<in> inside (path_image \<gamma>)" and z1: "cmod (winding_number \<gamma> z) = 1"
```
```   743     using simple_closed_path_wn3 [of \<gamma>] True assms by blast
```
```   744   have "winding_number \<gamma> z \<in> \<int>"
```
```   745     using zin integer_winding_number [OF \<open>path \<gamma>\<close> True] inside_def by blast
```
```   746   with z1 consider "winding_number \<gamma> z = 1" | "winding_number \<gamma> z = -1"
```
```   747     apply (auto simp: Ints_def abs_if split: if_split_asm)
```
```   748     by (metis of_int_1 of_int_eq_iff of_int_minus)
```
```   749   with that const zin show ?thesis
```
```   750     unfolding constant_on_def by metis
```
```   751 next
```
```   752   case False
```
```   753   then show ?thesis
```
```   754     using inside_simple_curve_imp_closed assms that(2) by blast
```
```   755 qed
```
```   756
```
```   757 lemma simple_closed_path_abs_winding_number_inside:
```
```   758   assumes "simple_path \<gamma>" "z \<in> inside(path_image \<gamma>)"
```
```   759     shows "\<bar>Re (winding_number \<gamma> z)\<bar> = 1"
```
```   760   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))
```
```   761
```
```   762 lemma simple_closed_path_norm_winding_number_inside:
```
```   763   assumes "simple_path \<gamma>" "z \<in> inside(path_image \<gamma>)"
```
```   764   shows "norm (winding_number \<gamma> z) = 1"
```
```   765 proof -
```
```   766   have "pathfinish \<gamma> = pathstart \<gamma>"
```
```   767     using assms inside_simple_curve_imp_closed by blast
```
```   768   with assms integer_winding_number have "winding_number \<gamma> z \<in> \<int>"
```
```   769     by (simp add: inside_def simple_path_def)
```
```   770   then show ?thesis
```
```   771     by (metis assms norm_minus_cancel norm_one simple_closed_path_winding_number_inside)
```
```   772 qed
```
```   773
```
```   774 lemma simple_closed_path_winding_number_cases:
```
```   775    "\<lbrakk>simple_path \<gamma>; pathfinish \<gamma> = pathstart \<gamma>; z \<notin> path_image \<gamma>\<rbrakk> \<Longrightarrow> winding_number \<gamma> z \<in> {-1,0,1}"
```
```   776 apply (simp add: inside_Un_outside [of "path_image \<gamma>", symmetric, unfolded set_eq_iff Set.Compl_iff] del: inside_Un_outside)
```
```   777    apply (rule simple_closed_path_winding_number_inside)
```
```   778   using simple_path_def winding_number_zero_in_outside by blast+
```
```   779
```
```   780 lemma simple_closed_path_winding_number_pos:
```
```   781    "\<lbrakk>simple_path \<gamma>; pathfinish \<gamma> = pathstart \<gamma>; z \<notin> path_image \<gamma>; 0 < Re(winding_number \<gamma> z)\<rbrakk>
```
```   782     \<Longrightarrow> winding_number \<gamma> z = 1"
```
```   783 using simple_closed_path_winding_number_cases
```
```   784   by fastforce
```
```   785
```
```   786 subsection \<open>Winding number for rectangular paths\<close>
```
```   787
```
```   788 (* TODO: Move *)
```
```   789 lemma closed_segmentI:
```
```   790   "u \<in> {0..1} \<Longrightarrow> z = (1 - u) *\<^sub>R a + u *\<^sub>R b \<Longrightarrow> z \<in> closed_segment a b"
```
```   791   by (auto simp: closed_segment_def)
```
```   792
```
```   793 lemma in_cbox_complex_iff:
```
```   794   "x \<in> cbox a b \<longleftrightarrow> Re x \<in> {Re a..Re b} \<and> Im x \<in> {Im a..Im b}"
```
```   795   by (cases x; cases a; cases b) (auto simp: cbox_Complex_eq)
```
```   796
```
```   797 lemma box_Complex_eq:
```
```   798   "box (Complex a c) (Complex b d) = (\<lambda>(x,y). Complex x y) ` (box a b \<times> box c d)"
```
```   799   by (auto simp: box_def Basis_complex_def image_iff complex_eq_iff)
```
```   800
```
```   801 lemma in_box_complex_iff:
```
```   802   "x \<in> box a b \<longleftrightarrow> Re x \<in> {Re a<..<Re b} \<and> Im x \<in> {Im a<..<Im b}"
```
```   803   by (cases x; cases a; cases b) (auto simp: box_Complex_eq)
```
```   804 (* END TODO *)
```
```   805
```
```   806 lemma closed_segment_same_Re:
```
```   807   assumes "Re a = Re b"
```
```   808   shows   "closed_segment a b = {z. Re z = Re a \<and> Im z \<in> closed_segment (Im a) (Im b)}"
```
```   809 proof safe
```
```   810   fix z assume "z \<in> closed_segment a b"
```
```   811   then obtain u where u: "u \<in> {0..1}" "z = a + of_real u * (b - a)"
```
```   812     by (auto simp: closed_segment_def scaleR_conv_of_real algebra_simps)
```
```   813   from assms show "Re z = Re a" by (auto simp: u)
```
```   814   from u(1) show "Im z \<in> closed_segment (Im a) (Im b)"
```
```   815     by (intro closed_segmentI[of u]) (auto simp: u algebra_simps)
```
```   816 next
```
```   817   fix z assume [simp]: "Re z = Re a" and "Im z \<in> closed_segment (Im a) (Im b)"
```
```   818   then obtain u where u: "u \<in> {0..1}" "Im z = Im a + of_real u * (Im b - Im a)"
```
```   819     by (auto simp: closed_segment_def scaleR_conv_of_real algebra_simps)
```
```   820   from u(1) show "z \<in> closed_segment a b" using assms
```
```   821     by (intro closed_segmentI[of u]) (auto simp: u algebra_simps scaleR_conv_of_real complex_eq_iff)
```
```   822 qed
```
```   823
```
```   824 lemma closed_segment_same_Im:
```
```   825   assumes "Im a = Im b"
```
```   826   shows   "closed_segment a b = {z. Im z = Im a \<and> Re z \<in> closed_segment (Re a) (Re b)}"
```
```   827 proof safe
```
```   828   fix z assume "z \<in> closed_segment a b"
```
```   829   then obtain u where u: "u \<in> {0..1}" "z = a + of_real u * (b - a)"
```
```   830     by (auto simp: closed_segment_def scaleR_conv_of_real algebra_simps)
```
```   831   from assms show "Im z = Im a" by (auto simp: u)
```
```   832   from u(1) show "Re z \<in> closed_segment (Re a) (Re b)"
```
```   833     by (intro closed_segmentI[of u]) (auto simp: u algebra_simps)
```
```   834 next
```
```   835   fix z assume [simp]: "Im z = Im a" and "Re z \<in> closed_segment (Re a) (Re b)"
```
```   836   then obtain u where u: "u \<in> {0..1}" "Re z = Re a + of_real u * (Re b - Re a)"
```
```   837     by (auto simp: closed_segment_def scaleR_conv_of_real algebra_simps)
```
```   838   from u(1) show "z \<in> closed_segment a b" using assms
```
```   839     by (intro closed_segmentI[of u]) (auto simp: u algebra_simps scaleR_conv_of_real complex_eq_iff)
```
```   840 qed
```
```   841
```
```   842 definition%important rectpath where
```
```   843   "rectpath a1 a3 = (let a2 = Complex (Re a3) (Im a1); a4 = Complex (Re a1) (Im a3)
```
```   844                       in linepath a1 a2 +++ linepath a2 a3 +++ linepath a3 a4 +++ linepath a4 a1)"
```
```   845
```
```   846 lemma path_rectpath [simp, intro]: "path (rectpath a b)"
```
```   847   by (simp add: Let_def rectpath_def)
```
```   848
```
```   849 lemma valid_path_rectpath [simp, intro]: "valid_path (rectpath a b)"
```
```   850   by (simp add: Let_def rectpath_def)
```
```   851
```
```   852 lemma pathstart_rectpath [simp]: "pathstart (rectpath a1 a3) = a1"
```
```   853   by (simp add: rectpath_def Let_def)
```
```   854
```
```   855 lemma pathfinish_rectpath [simp]: "pathfinish (rectpath a1 a3) = a1"
```
```   856   by (simp add: rectpath_def Let_def)
```
```   857
```
```   858 lemma simple_path_rectpath [simp, intro]:
```
```   859   assumes "Re a1 \<noteq> Re a3" "Im a1 \<noteq> Im a3"
```
```   860   shows   "simple_path (rectpath a1 a3)"
```
```   861   unfolding rectpath_def Let_def using assms
```
```   862   by (intro simple_path_join_loop arc_join arc_linepath)
```
```   863      (auto simp: complex_eq_iff path_image_join closed_segment_same_Re closed_segment_same_Im)
```
```   864
```
```   865 lemma path_image_rectpath:
```
```   866   assumes "Re a1 \<le> Re a3" "Im a1 \<le> Im a3"
```
```   867   shows "path_image (rectpath a1 a3) =
```
```   868            {z. Re z \<in> {Re a1, Re a3} \<and> Im z \<in> {Im a1..Im a3}} \<union>
```
```   869            {z. Im z \<in> {Im a1, Im a3} \<and> Re z \<in> {Re a1..Re a3}}" (is "?lhs = ?rhs")
```
```   870 proof -
```
```   871   define a2 a4 where "a2 = Complex (Re a3) (Im a1)" and "a4 = Complex (Re a1) (Im a3)"
```
```   872   have "?lhs = closed_segment a1 a2 \<union> closed_segment a2 a3 \<union>
```
```   873                   closed_segment a4 a3 \<union> closed_segment a1 a4"
```
```   874     by (simp_all add: rectpath_def Let_def path_image_join closed_segment_commute
```
```   875                       a2_def a4_def Un_assoc)
```
```   876   also have "\<dots> = ?rhs" using assms
```
```   877     by (auto simp: rectpath_def Let_def path_image_join a2_def a4_def
```
```   878           closed_segment_same_Re closed_segment_same_Im closed_segment_eq_real_ivl)
```
```   879   finally show ?thesis .
```
```   880 qed
```
```   881
```
```   882 lemma path_image_rectpath_subset_cbox:
```
```   883   assumes "Re a \<le> Re b" "Im a \<le> Im b"
```
```   884   shows   "path_image (rectpath a b) \<subseteq> cbox a b"
```
```   885   using assms by (auto simp: path_image_rectpath in_cbox_complex_iff)
```
```   886
```
```   887 lemma path_image_rectpath_inter_box:
```
```   888   assumes "Re a \<le> Re b" "Im a \<le> Im b"
```
```   889   shows   "path_image (rectpath a b) \<inter> box a b = {}"
```
```   890   using assms by (auto simp: path_image_rectpath in_box_complex_iff)
```
```   891
```
```   892 lemma path_image_rectpath_cbox_minus_box:
```
```   893   assumes "Re a \<le> Re b" "Im a \<le> Im b"
```
```   894   shows   "path_image (rectpath a b) = cbox a b - box a b"
```
```   895   using assms by (auto simp: path_image_rectpath in_cbox_complex_iff
```
```   896                              in_box_complex_iff)
```
```   897
```
```   898 proposition winding_number_rectpath:
```
```   899   assumes "z \<in> box a1 a3"
```
```   900   shows   "winding_number (rectpath a1 a3) z = 1"
```
```   901 proof -
```
```   902   from assms have less: "Re a1 < Re a3" "Im a1 < Im a3"
```
```   903     by (auto simp: in_box_complex_iff)
```
```   904   define a2 a4 where "a2 = Complex (Re a3) (Im a1)" and "a4 = Complex (Re a1) (Im a3)"
```
```   905   let ?l1 = "linepath a1 a2" and ?l2 = "linepath a2 a3"
```
```   906   and ?l3 = "linepath a3 a4" and ?l4 = "linepath a4 a1"
```
```   907   from assms and less have "z \<notin> path_image (rectpath a1 a3)"
```
```   908     by (auto simp: path_image_rectpath_cbox_minus_box)
```
```   909   also have "path_image (rectpath a1 a3) =
```
```   910                path_image ?l1 \<union> path_image ?l2 \<union> path_image ?l3 \<union> path_image ?l4"
```
```   911     by (simp add: rectpath_def Let_def path_image_join Un_assoc a2_def a4_def)
```
```   912   finally have "z \<notin> \<dots>" .
```
```   913   moreover have "\<forall>l\<in>{?l1,?l2,?l3,?l4}. Re (winding_number l z) > 0"
```
```   914     unfolding ball_simps HOL.simp_thms a2_def a4_def
```
```   915     by (intro conjI; (rule winding_number_linepath_pos_lt;
```
```   916           (insert assms, auto simp: a2_def a4_def in_box_complex_iff mult_neg_neg))+)
```
```   917   ultimately have "Re (winding_number (rectpath a1 a3) z) > 0"
```
```   918     by (simp add: winding_number_join path_image_join rectpath_def Let_def a2_def a4_def)
```
```   919   thus "winding_number (rectpath a1 a3) z = 1" using assms less
```
```   920     by (intro simple_closed_path_winding_number_pos simple_path_rectpath)
```
```   921        (auto simp: path_image_rectpath_cbox_minus_box)
```
```   922 qed
```
```   923
```
```   924 proposition winding_number_rectpath_outside:
```
```   925   assumes "Re a1 \<le> Re a3" "Im a1 \<le> Im a3"
```
```   926   assumes "z \<notin> cbox a1 a3"
```
```   927   shows   "winding_number (rectpath a1 a3) z = 0"
```
```   928   using assms by (intro winding_number_zero_outside[OF _ _ _ assms(3)]
```
```   929                      path_image_rectpath_subset_cbox) simp_all
```
```   930
```
```   931 text\<open>A per-function version for continuous logs, a kind of monodromy\<close>
```
```   932 proposition%unimportant winding_number_compose_exp:
```
```   933   assumes "path p"
```
```   934   shows "winding_number (exp \<circ> p) 0 = (pathfinish p - pathstart p) / (2 * of_real pi * \<i>)"
```
```   935 proof -
```
```   936   obtain e where "0 < e" and e: "\<And>t. t \<in> {0..1} \<Longrightarrow> e \<le> norm(exp(p t))"
```
```   937   proof
```
```   938     have "closed (path_image (exp \<circ> p))"
```
```   939       by (simp add: assms closed_path_image holomorphic_on_exp holomorphic_on_imp_continuous_on path_continuous_image)
```
```   940     then show "0 < setdist {0} (path_image (exp \<circ> p))"
```
```   941       by (metis exp_not_eq_zero imageE image_comp infdist_eq_setdist infdist_pos_not_in_closed path_defs(4) path_image_nonempty)
```
```   942   next
```
```   943     fix t::real
```
```   944     assume "t \<in> {0..1}"
```
```   945     have "setdist {0} (path_image (exp \<circ> p)) \<le> dist 0 (exp (p t))"
```
```   946       apply (rule setdist_le_dist)
```
```   947       using \<open>t \<in> {0..1}\<close> path_image_def by fastforce+
```
```   948     then show "setdist {0} (path_image (exp \<circ> p)) \<le> cmod (exp (p t))"
```
```   949       by simp
```
```   950   qed
```
```   951   have "bounded (path_image p)"
```
```   952     by (simp add: assms bounded_path_image)
```
```   953   then obtain B where "0 < B" and B: "path_image p \<subseteq> cball 0 B"
```
```   954     by (meson bounded_pos mem_cball_0 subsetI)
```
```   955   let ?B = "cball (0::complex) (B+1)"
```
```   956   have "uniformly_continuous_on ?B exp"
```
```   957     using holomorphic_on_exp holomorphic_on_imp_continuous_on
```
```   958     by (force intro: compact_uniformly_continuous)
```
```   959   then obtain d where "d > 0"
```
```   960         and d: "\<And>x x'. \<lbrakk>x\<in>?B; x'\<in>?B; dist x' x < d\<rbrakk> \<Longrightarrow> norm (exp x' - exp x) < e"
```
```   961     using \<open>e > 0\<close> by (auto simp: uniformly_continuous_on_def dist_norm)
```
```   962   then have "min 1 d > 0"
```
```   963     by force
```
```   964   then obtain g where pfg: "polynomial_function g"  and "g 0 = p 0" "g 1 = p 1"
```
```   965            and gless: "\<And>t. t \<in> {0..1} \<Longrightarrow> norm(g t - p t) < min 1 d"
```
```   966     using path_approx_polynomial_function [OF \<open>path p\<close>] \<open>d > 0\<close> \<open>0 < e\<close>
```
```   967     unfolding pathfinish_def pathstart_def by meson
```
```   968   have "winding_number (exp \<circ> p) 0 = winding_number (exp \<circ> g) 0"
```
```   969   proof (rule winding_number_nearby_paths_eq [symmetric])
```
```   970     show "path (exp \<circ> p)" "path (exp \<circ> g)"
```
```   971       by (simp_all add: pfg assms holomorphic_on_exp holomorphic_on_imp_continuous_on path_continuous_image path_polynomial_function)
```
```   972   next
```
```   973     fix t :: "real"
```
```   974     assume t: "t \<in> {0..1}"
```
```   975     with gless have "norm(g t - p t) < 1"
```
```   976       using min_less_iff_conj by blast
```
```   977     moreover have ptB: "norm (p t) \<le> B"
```
```   978       using B t by (force simp: path_image_def)
```
```   979     ultimately have "cmod (g t) \<le> B + 1"
```
```   980       by (meson add_mono_thms_linordered_field(4) le_less_trans less_imp_le norm_triangle_sub)
```
```   981     with ptB gless t have "cmod ((exp \<circ> g) t - (exp \<circ> p) t) < e"
```
```   982       by (auto simp: dist_norm d)
```
```   983     with e t show "cmod ((exp \<circ> g) t - (exp \<circ> p) t) < cmod ((exp \<circ> p) t - 0)"
```
```   984       by fastforce
```
```   985   qed (use \<open>g 0 = p 0\<close> \<open>g 1 = p 1\<close> in \<open>auto simp: pathfinish_def pathstart_def\<close>)
```
```   986   also have "... = 1 / (of_real (2 * pi) * \<i>) * contour_integral (exp \<circ> g) (\<lambda>w. 1 / (w - 0))"
```
```   987   proof (rule winding_number_valid_path)
```
```   988     have "continuous_on (path_image g) (deriv exp)"
```
```   989       by (metis DERIV_exp DERIV_imp_deriv continuous_on_cong holomorphic_on_exp holomorphic_on_imp_continuous_on)
```
```   990     then show "valid_path (exp \<circ> g)"
```
```   991       by (simp add: field_differentiable_within_exp pfg valid_path_compose valid_path_polynomial_function)
```
```   992     show "0 \<notin> path_image (exp \<circ> g)"
```
```   993       by (auto simp: path_image_def)
```
```   994   qed
```
```   995   also have "... = 1 / (of_real (2 * pi) * \<i>) * integral {0..1} (\<lambda>x. vector_derivative g (at x))"
```
```   996   proof (simp add: contour_integral_integral, rule integral_cong)
```
```   997     fix t :: "real"
```
```   998     assume t: "t \<in> {0..1}"
```
```   999     show "vector_derivative (exp \<circ> g) (at t) / exp (g t) = vector_derivative g (at t)"
```
```  1000     proof (simp add: divide_simps, rule vector_derivative_unique_at)
```
```  1001       show "(exp \<circ> g has_vector_derivative vector_derivative (exp \<circ> g) (at t)) (at t)"
```
```  1002         by (meson DERIV_exp differentiable_def field_vector_diff_chain_at has_vector_derivative_def
```
```  1003             has_vector_derivative_polynomial_function pfg vector_derivative_works)
```
```  1004       show "(exp \<circ> g has_vector_derivative vector_derivative g (at t) * exp (g t)) (at t)"
```
```  1005         apply (rule field_vector_diff_chain_at)
```
```  1006         apply (metis has_vector_derivative_polynomial_function pfg vector_derivative_at)
```
```  1007         using DERIV_exp has_field_derivative_def apply blast
```
```  1008         done
```
```  1009     qed
```
```  1010   qed
```
```  1011   also have "... = (pathfinish p - pathstart p) / (2 * of_real pi * \<i>)"
```
```  1012   proof -
```
```  1013     have "((\<lambda>x. vector_derivative g (at x)) has_integral g 1 - g 0) {0..1}"
```
```  1014       apply (rule fundamental_theorem_of_calculus [OF zero_le_one])
```
```  1015       by (metis has_vector_derivative_at_within has_vector_derivative_polynomial_function pfg vector_derivative_at)
```
```  1016     then show ?thesis
```
```  1017     apply (simp add: pathfinish_def pathstart_def)
```
```  1018       using \<open>g 0 = p 0\<close> \<open>g 1 = p 1\<close> by auto
```
```  1019   qed
```
```  1020   finally show ?thesis .
```
```  1021 qed
```
```  1022
```
```  1023 subsection%unimportant \<open>The winding number defines a continuous logarithm for the path itself\<close>
```
```  1024
```
```  1025 lemma winding_number_as_continuous_log:
```
```  1026   assumes "path p" and \<zeta>: "\<zeta> \<notin> path_image p"
```
```  1027   obtains q where "path q"
```
```  1028                   "pathfinish q - pathstart q = 2 * of_real pi * \<i> * winding_number p \<zeta>"
```
```  1029                   "\<And>t. t \<in> {0..1} \<Longrightarrow> p t = \<zeta> + exp(q t)"
```
```  1030 proof -
```
```  1031   let ?q = "\<lambda>t. 2 * of_real pi * \<i> * winding_number(subpath 0 t p) \<zeta> + Ln(pathstart p - \<zeta>)"
```
```  1032   show ?thesis
```
```  1033   proof
```
```  1034     have *: "continuous (at t within {0..1}) (\<lambda>x. winding_number (subpath 0 x p) \<zeta>)"
```
```  1035       if t: "t \<in> {0..1}" for t
```
```  1036     proof -
```
```  1037       let ?B = "ball (p t) (norm(p t - \<zeta>))"
```
```  1038       have "p t \<noteq> \<zeta>"
```
```  1039         using path_image_def that \<zeta> by blast
```
```  1040       then have "simply_connected ?B"
```
```  1041         by (simp add: convex_imp_simply_connected)
```
```  1042       then have "\<And>f::complex\<Rightarrow>complex. continuous_on ?B f \<and> (\<forall>\<zeta> \<in> ?B. f \<zeta> \<noteq> 0)
```
```  1043                   \<longrightarrow> (\<exists>g. continuous_on ?B g \<and> (\<forall>\<zeta> \<in> ?B. f \<zeta> = exp (g \<zeta>)))"
```
```  1044         by (simp add: simply_connected_eq_continuous_log)
```
```  1045       moreover have "continuous_on ?B (\<lambda>w. w - \<zeta>)"
```
```  1046         by (intro continuous_intros)
```
```  1047       moreover have "(\<forall>z \<in> ?B. z - \<zeta> \<noteq> 0)"
```
```  1048         by (auto simp: dist_norm)
```
```  1049       ultimately obtain g where contg: "continuous_on ?B g"
```
```  1050         and geq: "\<And>z. z \<in> ?B \<Longrightarrow> z - \<zeta> = exp (g z)" by blast
```
```  1051       obtain d where "0 < d" and d:
```
```  1052         "\<And>x. \<lbrakk>x \<in> {0..1}; dist x t < d\<rbrakk> \<Longrightarrow> dist (p x) (p t) < cmod (p t - \<zeta>)"
```
```  1053         using \<open>path p\<close> t unfolding path_def continuous_on_iff
```
```  1054         by (metis \<open>p t \<noteq> \<zeta>\<close> right_minus_eq zero_less_norm_iff)
```
```  1055       have "((\<lambda>x. winding_number (\<lambda>w. subpath 0 x p w - \<zeta>) 0 -
```
```  1056                   winding_number (\<lambda>w. subpath 0 t p w - \<zeta>) 0) \<longlongrightarrow> 0)
```
```  1057             (at t within {0..1})"
```
```  1058       proof (rule Lim_transform_within [OF _ \<open>d > 0\<close>])
```
```  1059         have "continuous (at t within {0..1}) (g o p)"
```
```  1060         proof (rule continuous_within_compose)
```
```  1061           show "continuous (at t within {0..1}) p"
```
```  1062             using \<open>path p\<close> continuous_on_eq_continuous_within path_def that by blast
```
```  1063           show "continuous (at (p t) within p ` {0..1}) g"
```
```  1064             by (metis (no_types, lifting) open_ball UNIV_I \<open>p t \<noteq> \<zeta>\<close> centre_in_ball contg continuous_on_eq_continuous_at continuous_within_topological right_minus_eq zero_less_norm_iff)
```
```  1065         qed
```
```  1066         with LIM_zero have "((\<lambda>u. (g (subpath t u p 1) - g (subpath t u p 0))) \<longlongrightarrow> 0) (at t within {0..1})"
```
```  1067           by (auto simp: subpath_def continuous_within o_def)
```
```  1068         then show "((\<lambda>u.  (g (subpath t u p 1) - g (subpath t u p 0)) / (2 * of_real pi * \<i>)) \<longlongrightarrow> 0)
```
```  1069            (at t within {0..1})"
```
```  1070           by (simp add: tendsto_divide_zero)
```
```  1071         show "(g (subpath t u p 1) - g (subpath t u p 0)) / (2 * of_real pi * \<i>) =
```
```  1072               winding_number (\<lambda>w. subpath 0 u p w - \<zeta>) 0 - winding_number (\<lambda>w. subpath 0 t p w - \<zeta>) 0"
```
```  1073           if "u \<in> {0..1}" "0 < dist u t" "dist u t < d" for u
```
```  1074         proof -
```
```  1075           have "closed_segment t u \<subseteq> {0..1}"
```
```  1076             using closed_segment_eq_real_ivl t that by auto
```
```  1077           then have piB: "path_image(subpath t u p) \<subseteq> ?B"
```
```  1078             apply (clarsimp simp add: path_image_subpath_gen)
```
```  1079             by (metis subsetD le_less_trans \<open>dist u t < d\<close> d dist_commute dist_in_closed_segment)
```
```  1080           have *: "path (g \<circ> subpath t u p)"
```
```  1081             apply (rule path_continuous_image)
```
```  1082             using \<open>path p\<close> t that apply auto[1]
```
```  1083             using piB contg continuous_on_subset by blast
```
```  1084           have "(g (subpath t u p 1) - g (subpath t u p 0)) / (2 * of_real pi * \<i>)
```
```  1085               =  winding_number (exp \<circ> g \<circ> subpath t u p) 0"
```
```  1086             using winding_number_compose_exp [OF *]
```
```  1087             by (simp add: pathfinish_def pathstart_def o_assoc)
```
```  1088           also have "... = winding_number (\<lambda>w. subpath t u p w - \<zeta>) 0"
```
```  1089           proof (rule winding_number_cong)
```
```  1090             have "exp(g y) = y - \<zeta>" if "y \<in> (subpath t u p) ` {0..1}" for y
```
```  1091               by (metis that geq path_image_def piB subset_eq)
```
```  1092             then show "\<And>x. \<lbrakk>0 \<le> x; x \<le> 1\<rbrakk> \<Longrightarrow> (exp \<circ> g \<circ> subpath t u p) x = subpath t u p x - \<zeta>"
```
```  1093               by auto
```
```  1094           qed
```
```  1095           also have "... = winding_number (\<lambda>w. subpath 0 u p w - \<zeta>) 0 -
```
```  1096                            winding_number (\<lambda>w. subpath 0 t p w - \<zeta>) 0"
```
```  1097             apply (simp add: winding_number_offset [symmetric])
```
```  1098             using winding_number_subpath_combine [OF \<open>path p\<close> \<zeta>, of 0 t u] \<open>t \<in> {0..1}\<close> \<open>u \<in> {0..1}\<close>
```
```  1099             by (simp add: add.commute eq_diff_eq)
```
```  1100           finally show ?thesis .
```
```  1101         qed
```
```  1102       qed
```
```  1103       then show ?thesis
```
```  1104         by (subst winding_number_offset) (simp add: continuous_within LIM_zero_iff)
```
```  1105     qed
```
```  1106     show "path ?q"
```
```  1107       unfolding path_def
```
```  1108       by (intro continuous_intros) (simp add: continuous_on_eq_continuous_within *)
```
```  1109
```
```  1110     have "\<zeta> \<noteq> p 0"
```
```  1111       by (metis \<zeta> pathstart_def pathstart_in_path_image)
```
```  1112     then show "pathfinish ?q - pathstart ?q = 2 * of_real pi * \<i> * winding_number p \<zeta>"
```
```  1113       by (simp add: pathfinish_def pathstart_def)
```
```  1114     show "p t = \<zeta> + exp (?q t)" if "t \<in> {0..1}" for t
```
```  1115     proof -
```
```  1116       have "path (subpath 0 t p)"
```
```  1117         using \<open>path p\<close> that by auto
```
```  1118       moreover
```
```  1119       have "\<zeta> \<notin> path_image (subpath 0 t p)"
```
```  1120         using \<zeta> [unfolded path_image_def] that by (auto simp: path_image_subpath)
```
```  1121       ultimately show ?thesis
```
```  1122         using winding_number_exp_2pi [of "subpath 0 t p" \<zeta>] \<open>\<zeta> \<noteq> p 0\<close>
```
```  1123         by (auto simp: exp_add algebra_simps pathfinish_def pathstart_def subpath_def)
```
```  1124     qed
```
```  1125   qed
```
```  1126 qed
```
```  1127
```
```  1128 subsection \<open>Winding number equality is the same as path/loop homotopy in C - {0}\<close>
```
```  1129
```
```  1130 lemma winding_number_homotopic_loops_null_eq:
```
```  1131   assumes "path p" and \<zeta>: "\<zeta> \<notin> path_image p"
```
```  1132   shows "winding_number p \<zeta> = 0 \<longleftrightarrow> (\<exists>a. homotopic_loops (-{\<zeta>}) p (\<lambda>t. a))"
```
```  1133     (is "?lhs = ?rhs")
```
```  1134 proof
```
```  1135   assume [simp]: ?lhs
```
```  1136   obtain q where "path q"
```
```  1137              and qeq:  "pathfinish q - pathstart q = 2 * of_real pi * \<i> * winding_number p \<zeta>"
```
```  1138              and peq: "\<And>t. t \<in> {0..1} \<Longrightarrow> p t = \<zeta> + exp(q t)"
```
```  1139     using winding_number_as_continuous_log [OF assms] by blast
```
```  1140   have *: "homotopic_with (\<lambda>r. pathfinish r = pathstart r)
```
```  1141                        {0..1} (-{\<zeta>}) ((\<lambda>w. \<zeta> + exp w) \<circ> q) ((\<lambda>w. \<zeta> + exp w) \<circ> (\<lambda>t. 0))"
```
```  1142   proof (rule homotopic_with_compose_continuous_left)
```
```  1143     show "homotopic_with (\<lambda>f. pathfinish ((\<lambda>w. \<zeta> + exp w) \<circ> f) = pathstart ((\<lambda>w. \<zeta> + exp w) \<circ> f))
```
```  1144               {0..1} UNIV q (\<lambda>t. 0)"
```
```  1145     proof (rule homotopic_with_mono, simp_all add: pathfinish_def pathstart_def)
```
```  1146       have "homotopic_loops UNIV q (\<lambda>t. 0)"
```
```  1147         by (rule homotopic_loops_linear) (use qeq \<open>path q\<close> in \<open>auto simp: continuous_on_const path_defs\<close>)
```
```  1148       then show "homotopic_with (\<lambda>h. exp (h 1) = exp (h 0)) {0..1} UNIV q (\<lambda>t. 0)"
```
```  1149         by (simp add: homotopic_loops_def homotopic_with_mono pathfinish_def pathstart_def)
```
```  1150     qed
```
```  1151     show "continuous_on UNIV (\<lambda>w. \<zeta> + exp w)"
```
```  1152       by (rule continuous_intros)+
```
```  1153     show "range (\<lambda>w. \<zeta> + exp w) \<subseteq> -{\<zeta>}"
```
```  1154       by auto
```
```  1155   qed
```
```  1156   then have "homotopic_with (\<lambda>r. pathfinish r = pathstart r) {0..1} (-{\<zeta>}) p (\<lambda>x. \<zeta> + 1)"
```
```  1157     by (rule homotopic_with_eq) (auto simp: o_def peq pathfinish_def pathstart_def)
```
```  1158   then have "homotopic_loops (-{\<zeta>}) p (\<lambda>t. \<zeta> + 1)"
```
```  1159     by (simp add: homotopic_loops_def)
```
```  1160   then show ?rhs ..
```
```  1161 next
```
```  1162   assume ?rhs
```
```  1163   then obtain a where "homotopic_loops (-{\<zeta>}) p (\<lambda>t. a)" ..
```
```  1164   then have "winding_number p \<zeta> = winding_number (\<lambda>t. a) \<zeta>" "a \<noteq> \<zeta>"
```
```  1165     using winding_number_homotopic_loops homotopic_loops_imp_subset by (force simp:)+
```
```  1166   moreover have "winding_number (\<lambda>t. a) \<zeta> = 0"
```
```  1167     by (metis winding_number_zero_const \<open>a \<noteq> \<zeta>\<close>)
```
```  1168   ultimately show ?lhs by metis
```
```  1169 qed
```
```  1170
```
```  1171 lemma winding_number_homotopic_paths_null_explicit_eq:
```
```  1172   assumes "path p" and \<zeta>: "\<zeta> \<notin> path_image p"
```
```  1173   shows "winding_number p \<zeta> = 0 \<longleftrightarrow> homotopic_paths (-{\<zeta>}) p (linepath (pathstart p) (pathstart p))"
```
```  1174         (is "?lhs = ?rhs")
```
```  1175 proof
```
```  1176   assume ?lhs
```
```  1177   then show ?rhs
```
```  1178     apply (auto simp: winding_number_homotopic_loops_null_eq [OF assms])
```
```  1179     apply (rule homotopic_loops_imp_homotopic_paths_null)
```
```  1180     apply (simp add: linepath_refl)
```
```  1181     done
```
```  1182 next
```
```  1183   assume ?rhs
```
```  1184   then show ?lhs
```
```  1185     by (metis \<zeta> pathstart_in_path_image winding_number_homotopic_paths winding_number_trivial)
```
```  1186 qed
```
```  1187
```
```  1188 lemma winding_number_homotopic_paths_null_eq:
```
```  1189   assumes "path p" and \<zeta>: "\<zeta> \<notin> path_image p"
```
```  1190   shows "winding_number p \<zeta> = 0 \<longleftrightarrow> (\<exists>a. homotopic_paths (-{\<zeta>}) p (\<lambda>t. a))"
```
```  1191     (is "?lhs = ?rhs")
```
```  1192 proof
```
```  1193   assume ?lhs
```
```  1194   then show ?rhs
```
```  1195     by (auto simp: winding_number_homotopic_paths_null_explicit_eq [OF assms] linepath_refl)
```
```  1196 next
```
```  1197   assume ?rhs
```
```  1198   then show ?lhs
```
```  1199     by (metis \<zeta> homotopic_paths_imp_pathfinish pathfinish_def pathfinish_in_path_image winding_number_homotopic_paths winding_number_zero_const)
```
```  1200 qed
```
```  1201
```
```  1202 proposition winding_number_homotopic_paths_eq:
```
```  1203   assumes "path p" and \<zeta>p: "\<zeta> \<notin> path_image p"
```
```  1204       and "path q" and \<zeta>q: "\<zeta> \<notin> path_image q"
```
```  1205       and qp: "pathstart q = pathstart p" "pathfinish q = pathfinish p"
```
```  1206     shows "winding_number p \<zeta> = winding_number q \<zeta> \<longleftrightarrow> homotopic_paths (-{\<zeta>}) p q"
```
```  1207     (is "?lhs = ?rhs")
```
```  1208 proof
```
```  1209   assume ?lhs
```
```  1210   then have "winding_number (p +++ reversepath q) \<zeta> = 0"
```
```  1211     using assms by (simp add: winding_number_join winding_number_reversepath)
```
```  1212   moreover
```
```  1213   have "path (p +++ reversepath q)" "\<zeta> \<notin> path_image (p +++ reversepath q)"
```
```  1214     using assms by (auto simp: not_in_path_image_join)
```
```  1215   ultimately obtain a where "homotopic_paths (- {\<zeta>}) (p +++ reversepath q) (linepath a a)"
```
```  1216     using winding_number_homotopic_paths_null_explicit_eq by blast
```
```  1217   then show ?rhs
```
```  1218     using homotopic_paths_imp_pathstart assms
```
```  1219     by (fastforce simp add: dest: homotopic_paths_imp_homotopic_loops homotopic_paths_loop_parts)
```
```  1220 next
```
```  1221   assume ?rhs
```
```  1222   then show ?lhs
```
```  1223     by (simp add: winding_number_homotopic_paths)
```
```  1224 qed
```
```  1225
```
```  1226 lemma winding_number_homotopic_loops_eq:
```
```  1227   assumes "path p" and \<zeta>p: "\<zeta> \<notin> path_image p"
```
```  1228       and "path q" and \<zeta>q: "\<zeta> \<notin> path_image q"
```
```  1229       and loops: "pathfinish p = pathstart p" "pathfinish q = pathstart q"
```
```  1230     shows "winding_number p \<zeta> = winding_number q \<zeta> \<longleftrightarrow> homotopic_loops (-{\<zeta>}) p q"
```
```  1231     (is "?lhs = ?rhs")
```
```  1232 proof
```
```  1233   assume L: ?lhs
```
```  1234   have "pathstart p \<noteq> \<zeta>" "pathstart q \<noteq> \<zeta>"
```
```  1235     using \<zeta>p \<zeta>q by blast+
```
```  1236   moreover have "path_connected (-{\<zeta>})"
```
```  1237     by (simp add: path_connected_punctured_universe)
```
```  1238   ultimately obtain r where "path r" and rim: "path_image r \<subseteq> -{\<zeta>}"
```
```  1239                         and pas: "pathstart r = pathstart p" and paf: "pathfinish r = pathstart q"
```
```  1240     by (auto simp: path_connected_def)
```
```  1241   then have "pathstart r \<noteq> \<zeta>" by blast
```
```  1242   have "homotopic_loops (- {\<zeta>}) p (r +++ q +++ reversepath r)"
```
```  1243   proof (rule homotopic_paths_imp_homotopic_loops)
```
```  1244     show "homotopic_paths (- {\<zeta>}) p (r +++ q +++ reversepath r)"
```
```  1245       by (metis (mono_tags, hide_lams) \<open>path r\<close> L \<zeta>p \<zeta>q \<open>path p\<close> \<open>path q\<close> 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)
```
```  1246   qed (use loops pas in auto)
```
```  1247   moreover have "homotopic_loops (- {\<zeta>}) (r +++ q +++ reversepath r) q"
```
```  1248     using rim \<zeta>q by (auto simp: homotopic_loops_conjugate paf \<open>path q\<close> \<open>path r\<close> loops)
```
```  1249   ultimately show ?rhs
```
```  1250     using homotopic_loops_trans by metis
```
```  1251 next
```
```  1252   assume ?rhs
```
```  1253   then show ?lhs
```
```  1254     by (simp add: winding_number_homotopic_loops)
```
```  1255 qed
```
```  1256
```
```  1257 end
```
```  1258
```