Theory Winding_Number_Eval.Winding_Number_Eval

(*
    Author:     Wenda Li <wl302@cam.ac.uk / liwenda1990@hotmail.com>
*)

section ‹Evaluate winding numbers by calculating Cauchy indices›

theory Winding_Number_Eval imports 
  Cauchy_Index_Theorem 
  "HOL-Eisbach.Eisbach_Tools"
begin
  
subsection ‹Misc›

lemma not_on_closed_segmentI:
  fixes z::"'a::euclidean_space"
  assumes "norm (z - a) *R (b - z)  norm (b - z) *R (z - a)"
  shows "z  closed_segment a b"
  using assms by (auto simp add:between_mem_segment[symmetric] between_norm)

lemma not_on_closed_segmentI_complex:    
  fixes z::"complex"
  assumes "(Re b - Re z) * (Im z - Im a)  (Im b - Im z) * (Re z - Re a)"
  shows "z  closed_segment a b"
proof (cases "za  zb")
  case True
  then have "cmod (z - a)0" "cmod (b - z)0" by auto
  then have "(Re b - Re z) * (Im z - Im a) = (Im b - Im z) * (Re z - Re a)" when 
    "cmod (z - a) * (Re b - Re z) = cmod (b - z) * (Re z - Re a)"
    "cmod (z - a) * (Im b - Im z) = cmod (b - z) * (Im z - Im a)"
    using that by algebra
  then show ?thesis using assms
    apply (intro not_on_closed_segmentI)
    by (auto simp add:scaleR_complex.ctr simp del:Complex_eq)
next
  case False
  then have "(Re b - Re z) * (Im z - Im a) = (Im b - Im z) * (Re z - Re a)" by auto
  then have False using assms by auto
  then show ?thesis by auto
qed

subsection ‹finite intersection with the two axes›

definition finite_axes_cross::"(real  complex)  complex  bool" where
  "finite_axes_cross g z = finite {t. (Re (g t-z) = 0  Im (g t-z) = 0)  0  t  t  1}"

lemma finite_cross_intros:
  "Re aRe z  Re b Re z; Im aIm z  Im bIm zfinite_axes_cross (linepath a b) z"
  "st  tt; r  0  finite_axes_cross (part_circlepath z0 r st tt) z"
  "finite_axes_cross g1 z;finite_axes_cross g2 z  finite_axes_cross (g1+++g2) z"
proof -
  assume asm:"Re aRe z  Re b Re z" "Im aIm z  Im bIm z"
  let ?S1="{t. Re (linepath a b t-z) = 0  0  t  t  1}"
  and ?S2="{t. Im (linepath a b t-z) = 0  0  t  t  1}"
  have "finite ?S1" 
    using linepath_half_finite_inter[of a "Complex 1 0" "Re z" b] asm(1) 
    by (auto simp add:inner_complex_def)
  moreover have "finite ?S2"
    using linepath_half_finite_inter[of a "Complex 0 1" "Im z" b] asm(2) 
    by (auto simp add:inner_complex_def)
  moreover have "{t. (Re (linepath a b t-z) = 0  Im (linepath a b t-z) = 0)  0  t  t  1} 
      = ?S1  ?S2"
    by fast
  ultimately show "finite_axes_cross (linepath a b) z"
    unfolding finite_axes_cross_def by force
next
  assume asm: "st tt" "r0"
  let ?S1="{t. Re (part_circlepath z0 r st tt t-z) = 0  0  t  t  1}"
  and ?S2="{t. Im (part_circlepath z0 r st tt t-z) = 0  0  t  t  1}"
  have "finite ?S1"
    using part_circlepath_half_finite_inter[of st tt r "Complex 1 0" z0 "Re z"] asm 
    by (auto simp add:inner_complex_def Complex_eq_0)
  moreover have "finite ?S2"
    using part_circlepath_half_finite_inter[of st tt r "Complex 0 1" z0 "Im z"] asm 
    by (auto simp add:inner_complex_def Complex_eq_0)
  moreover have "{t. (Re (part_circlepath z0 r st tt t-z) = 0 
       Im (part_circlepath z0 r st tt t-z) = 0)  0  t  t  1} = ?S1  ?S2"
    by fast
  ultimately show "finite_axes_cross (part_circlepath z0 r st tt) z" 
    unfolding finite_axes_cross_def by auto
next
  assume asm:"finite_axes_cross g1 z" "finite_axes_cross g2 z"
  let ?g1R="{t. Re (g1 t-z) = 0  0  t  t  1}"
  and ?g1I="{t. Im (g1 t-z) = 0  0  t  t  1}"
  and ?g2R="{t. Re (g2 t-z) = 0  0  t  t  1}"
  and ?g2I="{t. Im (g2 t-z) = 0  0  t  t  1}"
  have "finite ?g1R" "finite ?g1I"
  proof -
    have "{t. (Re (g1 t - z) = 0  Im (g1 t - z) = 0)  0  t  t  1} = ?g1R  ?g1I"
      by force
    then have "finite (?g1R  ?g1I)"
      using asm(1) unfolding finite_axes_cross_def by auto
    then show "finite ?g1R" "finite ?g1I" by blast+
  qed
  have "finite ?g2R" "finite ?g2I" 
  proof -
    have "{t. (Re (g2 t - z) = 0  Im (g2 t - z) = 0)  0  t  t  1} = ?g2R  ?g2I"
      by force
    then have "finite (?g2R  ?g2I)"
      using asm(2) unfolding finite_axes_cross_def by auto
    then show "finite ?g2R" "finite ?g2I" by blast+
  qed
  let ?S1 = "{t. Re ((g1 +++ g2) t - z) = 0  0  t  t  1}"
  and ?S2 = "{t. Im ((g1 +++ g2) t - z) = 0  0  t  t  1}"
  have "finite ?S1"  
    using finite_half_joinpaths_inter[of g1 "Complex 1 0" "Re z" g2,simplified] 
      finite ?g1R finite ?g2R
    by (auto simp add:inner_complex_def)
  moreover have "finite ?S2"  
    using finite_half_joinpaths_inter[of g1 "Complex 0 1" "Im z" g2,simplified] 
      finite ?g1I finite ?g2I
    by (auto simp add:inner_complex_def)
  moreover have "{t. (Re ((g1 +++ g2) t - z) = 0  Im ((g1 +++ g2) t - z) = 0)  0  t  t  1}
        = ?S1  ?S2" 
    by force
  ultimately show "finite_axes_cross (g1 +++ g2) z"
    unfolding finite_axes_cross_def 
    by auto
qed

lemma cindex_path_joinpaths:
  assumes "finite_axes_cross g1 z" "finite_axes_cross g2 z"
    and "path g1" "path g2" "pathfinish g1 = pathstart g2" "pathfinish g1z" 
  shows "cindex_path (g1+++g2) z = cindex_path g1 z + jumpF_pathstart g2 z 
            - jumpF_pathfinish g1 z  + cindex_path g2 z"
proof -
  define h12 where "h12 = (λt. Im ((g1+++g2) t - z) / Re ((g1+++g2) t - z))"
  let ?h = "λg. λt. Im (g t - z) / Re (g t - z)"
  have "cindex_path (g1+++g2) z = cindex 0 1 h12"
    unfolding cindex_path_def h12_def by simp
  also have "... = cindex 0 (1/2) h12 + jump h12 (1/2) + cindex (1/2) 1 h12"
  proof (rule cindex_combine)
    have "finite_axes_cross (g1+++g2) z" using assms by (auto intro:finite_cross_intros)
    then have "finite {t. Re ((g1+++g2) t - z) = 0  0t  t1}" 
      unfolding finite_axes_cross_def by (auto elim:rev_finite_subset)
    moreover have " jump h12 t = 0" when "Re ((g1 +++ g2) t - z)  0" "0 < t" "t < 1" for t 
      apply (rule jump_Im_divide_Re_0[of "λt. (g1+++g2) t- z",folded h12_def,OF _ that])
      using assms by (auto intro:path_offset)
    ultimately show "finite {x. jump h12 x  0  0 < x  x < 1}" 
      apply (elim rev_finite_subset)
      by auto
  qed auto
  also have "... = cindex_path g1 z + jumpF_pathstart g2 z  
      - jumpF_pathfinish g1 z  + cindex_path g2 z"
  proof -
    have "jump h12 (1/2) =  jumpF_pathstart g2 z -  jumpF_pathfinish g1 z  "
    proof -
      have "jump h12 (1 / 2) = jumpF h12 (at_right (1 / 2)) - jumpF h12 (at_left (1 / 2))"
      proof (cases "Re ((g1+++g2) (1/2) - z) = 0")
        case False
        have "jump h12 (1 / 2) = 0"
          unfolding h12_def
          apply (rule jump_Im_divide_Re_0)
          using assms False by (auto intro:path_offset)
        moreover have "jumpF h12 (at_right (1/2)) = 0"
          unfolding h12_def 
          apply (intro jumpF_im_divide_Re_0)
          subgoal using assms by (auto intro:path_offset)
          subgoal using assms(5-6) False unfolding joinpaths_def pathfinish_def pathstart_def by auto
          by auto
        moreover have "jumpF h12 (at_left (1/2)) = 0"
          unfolding h12_def 
          apply (intro jumpF_im_divide_Re_0)
          subgoal using assms by (auto intro:path_offset)
          subgoal using assms(5-6) False unfolding joinpaths_def pathfinish_def pathstart_def by auto
          by auto    
        ultimately show ?thesis by auto
      next
        case True
        then have "Im ((g1 +++ g2) (1 / 2) - z)  0"
          using assms(5,6)
          by (metis (no_types, opaque_lifting) Re_divide_numeral complex_Re_numeral complex_eq 
              divide_self_if joinpaths_def  minus_complex.simps mult.commute mult.left_neutral
              numeral_One pathfinish_def pathstart_def right_minus_eq times_divide_eq_left zero_neq_numeral)
        show ?thesis
        proof (rule jump_jumpF[of _ h12 "sgnx h12 (at_left (1/2))" "sgnx h12 (at_right (1/2))"])
          define g where "g=(λt. (g1 +++ g2) t - z)"
          have h12_def:"h12 = (λt. Im(g t)/Re(g t))" unfolding h12_def g_def by simp  
          have "path g" using assms unfolding g_def by (auto intro!:path_offset)
          then have "isCont (λt. Im (g t)) (1 / 2)" "isCont (λt. Re (g t)) (1 / 2)" 
            unfolding path_def by (auto intro!:continuous_intros continuous_on_interior)
          moreover have "Im (g (1/2)) 0"
            using Im ((g1 +++ g2) (1 / 2) - z)  0 unfolding g_def .
          ultimately show "isCont (inverse  h12) (1 / 2)" 
            unfolding h12_def comp_def 
            by (auto intro!: continuous_intros)
              
          define l where "l  sgnx h12 (at_left (1/2))"
          define r where "r  sgnx h12 (at_right (1/2))"
          have *:"continuous_on ({0<..<1}- {t. h12 t = 0  0 < t  t < 1}) h12"
            using path g[unfolded path_def] unfolding h12_def
            apply (auto intro!: continuous_intros)
            by (auto elim:continuous_on_subset)   
          have **:"finite {t. h12 t = 0  0 < t  t < 1}" 
          proof -
            have "finite_axes_cross (g1 +++ g2) z" 
              using assms(1,2) finite_cross_intros(3)[of g1 z g2] by auto
            then have "finite {t. (Re (g t) = 0  Im (g t) = 0)  0 < t  t < 1}" 
              unfolding finite_axes_cross_def g_def 
              apply (elim rev_finite_subset)
              by auto
            then show ?thesis unfolding h12_def 
              by (simp add:disj_commute)
          qed 
          have "h12 sgnx_able at_left (1/2)" "l  0" "h12 sgnx_able at_right (1/2)" "r  0"
            unfolding l_def r_def using finite_sgnx_at_left_at_right[OF ** * **] 
            by auto
          then show "(h12 has_sgnx l) (at_left (1/2))" "(h12 has_sgnx r) (at_right (1/2))" "l0" "r0"
            unfolding l_def r_def by (auto elim:sgnx_able_sgnx)
        qed 
      qed
      moreover have "jumpF h12 (at_right (1/2)) = jumpF_pathstart g2 z"
      proof -
        have " jumpF h12 (at_right (1 / 2)) = jumpF (h12  (λx. x / 2 + 1 / 2)) (at_right 0)"
          using jumpF_linear_comp[of "1/2" h12 "1/2" 0,simplified] by simp
        also have "jumpF (h12  (λx. x / 2 + 1 / 2)) (at_right 0) = jumpF_pathstart g2 z"
          unfolding h12_def jumpF_pathstart_def
        proof (rule jumpF_cong)
          show "F x in at_right 0. ((λt. Im ((g1 +++ g2) t - z) / Re ((g1 +++ g2) t - z)) 
                   (λx. x / 2 + 1 / 2)) x = Im (g2 x - z) / Re (g2 x - z)"
            unfolding eventually_at_right
            apply (intro exI[where x="1/2"])
            unfolding joinpaths_def by auto
        qed simp
        finally show ?thesis .
      qed
      moreover have "jumpF h12 (at_left (1 / 2)) = jumpF_pathfinish g1 z" 
      proof -
        have "jumpF h12 (at_left (1 / 2)) = jumpF (h12  (λx. x / 2)) (at_left 1)"
          using jumpF_linear_comp[of "1/2" h12 0 1,simplified] by simp
        also have "jumpF (h12  (λx. x / 2 )) (at_left 1) = jumpF_pathfinish g1 z"
          unfolding h12_def jumpF_pathfinish_def
        proof (rule jumpF_cong)
          show " F x in at_left 1. ((λt. Im ((g1 +++ g2) t - z) / Re ((g1 +++ g2) t - z)) 
               (λx. x / 2)) x = Im (g1 x - z) / Re (g1 x - z)"
            unfolding eventually_at_left
            apply (intro exI[where x="1/2"])
            unfolding joinpaths_def by auto
        qed simp
        finally show ?thesis .
      qed
      ultimately show ?thesis by auto
    qed
    moreover have "cindex 0 (1 / 2) h12 = cindex_path g1 z"
    proof -
      have "cindex 0 (1 / 2) h12 = cindex 0 1 (h12  (λx. x / 2))"
        using cindex_linear_comp[of "1/2" 0 1 h12 0,simplified,symmetric] .
      also have "... = cindex_path g1 z"
      proof -
        let ?g = " (λt. Im (g1 t - z) / Re (g1 t - z))"
        have *:"jump (h12  (λx. x / 2)) x = jump ?g x" when "0<x" "x<1" for x 
          unfolding h12_def   
        proof (rule jump_cong)
          show "F x in at x. ((λt. Im ((g1 +++ g2) t - z) / Re ((g1 +++ g2) t - z)) 
               (λx. x / 2)) x = Im (g1 x - z) / Re (g1 x - z)"
            unfolding eventually_at joinpaths_def comp_def using that
            apply (intro exI[where x="(1-x)/2"])
            by (auto simp add: dist_norm)
        qed simp
        then have "{x. jump (h12  (λx. x / 2)) x  0  0 < x  x < 1} 
            = {x. jump ?g x  0  0 < x  x < 1}"
          by auto
        then show ?thesis
          unfolding cindex_def cindex_path_def 
          apply (elim sum.cong)
          by (auto simp add:*)
      qed
      finally show ?thesis .
    qed
    moreover have "cindex (1 / 2) 1 h12 = cindex_path g2 z"
    proof -
      have "cindex (1 / 2) 1 h12 = cindex 0 1 (h12  (λx. x / 2 + 1 / 2))"
        using cindex_linear_comp[of "1/2" 0 1 h12 "1/2",simplified,symmetric] . 
      also have "... = cindex_path g2 z"
      proof -
        let ?g = " (λt. Im (g2 t - z) / Re (g2 t - z))"
        have *:"jump (h12  (λx. x / 2+1/2)) x = jump ?g x" when "0<x" "x<1" for x 
          unfolding h12_def   
        proof (rule jump_cong)
          show "F x in at x. ((λt. Im ((g1 +++ g2) t - z) / Re ((g1 +++ g2) t - z)) 
               (λx. x / 2+1/2)) x = Im (g2 x - z) / Re (g2 x - z)"
            unfolding eventually_at joinpaths_def comp_def using that
            apply (intro exI[where x="x/2"])
            by (auto simp add: dist_norm)
        qed simp
        then have "{x. jump (h12  (λx. x / 2+1/2)) x  0  0 < x  x < 1} 
            = {x. jump ?g x  0  0 < x  x < 1}"
          by auto
        then show ?thesis
          unfolding cindex_def cindex_path_def 
          apply (elim sum.cong)
          by (auto simp add:*)
      qed
      finally show ?thesis .
    qed     
    ultimately show ?thesis by simp
  qed
  finally show ?thesis .
qed  
    
subsection ‹More lemmas related @{term cindex_pathE} / @{term jumpF_pathstart} / @{term jumpF_pathfinish}
    
lemma cindex_pathE_linepath:
  assumes "zclosed_segment a b"
  shows "cindex_pathE (linepath a b) z = (
    let c1 = Re a - Re z; 
        c2 = Re b - Re z; 
        c3 = Im a * Re b + Re z * Im b + Im z * Re a - Im z * Re b - Im b * Re a - Re z * Im a;
        d1 = Im a - Im z;
        d2 = Im b - Im z
    in if (c1>0  c2<0)  (c1<0  c2>0) then 
          (if c3>0 then 1 else -1) 
       else 
          (if (c1=0  c20)  (c1=0 d10)  (c2=0  d20) then 
            if (c1=0  (c2 >0  d1>0))  (c2=0  (c1 >0  d2<0))  then 1/2 else -1/2
          else 0))"
proof -
  define c1 c2 where "c1=Re a - Re z" and "c2=Re b - Re z"
  define d1 d2 where "d1=Im a - Im z" and "d2=Im b - Im z"
  let ?g = "linepath a b"
  have ?thesis when "¬ ((c1>0  c2<0)  (c1<0  c2>0))"   
  proof -
    have "Re a= Re z  Re b=Re z"
      when "0<t" "t<1" and asm:"(1-t)*Re a + t * Re b = Re z" for t
      unfolding c1_def c2_def using that  
    proof -
      have ?thesis when "c10" "c10"
      proof -
        have "Re a=Re z" using that unfolding c1_def by auto
        then show ?thesis using 0<t t<1 asm
          apply (cases "Re b" "Re z" rule:linorder_cases)
            apply (auto simp add:field_simps)
          done
      qed
      moreover have ?thesis when "c10" "c20"
      proof -  
        have False when "c1<0"
        proof -
          have "(1 - t) * Re a < (1 - t) * Re z"
            using t<1 c1<0 unfolding c1_def by auto
          moreover have "t * Re b  t* Re z" using t>0 c20 unfolding c2_def by auto
          ultimately have "(1 - t) * Re a + t * Re b < (1 - t) * Re z + t * Re z"
            by auto
          thus False using asm by (auto simp add:algebra_simps)
        qed
        moreover have False when "c2<0"
        proof -
          have "(1 - t) * Re a  (1 - t) * Re z"
            using t<1 c10 unfolding c1_def by auto
          moreover have "t * Re b < t* Re z" using t>0 c2<0 unfolding c2_def by auto
          ultimately have "(1 - t) * Re a + t * Re b < (1 - t) * Re z + t * Re z"
            by auto
          thus False using asm by (auto simp add:algebra_simps)
        qed
        ultimately show ?thesis using that unfolding c1_def c2_def by argo
      qed
      moreover have ?thesis when "c20" "c20"
      proof -
        have "Re b=Re z" using that unfolding c2_def by auto
        then have "(1 - t) * Re a = (1-t)*Re z" using asm by (auto simp add:field_simps)
        then have "Re a= Re z" using t<1 by auto
        then show ?thesis using Re b=Re z by auto
      qed
      moreover have ?thesis when "c10" "c20"
      proof -  
        have False when "c1>0"
        proof -
          have "(1 - t) * Re a > (1 - t) * Re z"
            using t<1 c1>0 unfolding c1_def by auto
          moreover have "t * Re b  t* Re z" using t>0 c20 unfolding c2_def by auto
          ultimately have "(1 - t) * Re a + t * Re b > (1 - t) * Re z + t * Re z"
            by auto
          thus False using asm by (auto simp add:algebra_simps)
        qed
        moreover have False when "c2>0"
        proof -
          have "(1 - t) * Re a  (1 - t) * Re z"
            using t<1 c10 unfolding c1_def by auto
          moreover have "t * Re b > t* Re z" using t>0 c2>0 unfolding c2_def by auto
          ultimately have "(1 - t) * Re a + t * Re b > (1 - t) * Re z + t * Re z"
            by auto
          thus False using asm by (auto simp add:algebra_simps)
        qed
        ultimately show ?thesis using that unfolding c1_def c2_def by argo
      qed
      moreover have "c10  c20" "c10  c20" using ¬ ((c1>0  c2<0)  (c1<0  c2>0)) by auto
      ultimately show ?thesis by fast
    qed
    then have "(t. 0<t  t<1  Re(linepath a b t - z)  0)  (c1=0  c2=0)" 
      using that unfolding linepath_def c1_def c2_def by auto
    moreover have ?thesis when asm:"t. 0<t  t<1  Re(linepath a b t - z)  0"
      and "¬ (c1=0  c2=0)"
    proof -
      have cindex_ends:"cindex_pathE ?g z = jumpF_pathstart ?g z - jumpF_pathfinish ?g z"
      proof -
        define f where "f=(λt. Im (linepath a b t - z) / Re (linepath a b t - z))"
        define left where "left = {x. jumpF f (at_left x)  0  0 < x  x  1}"
        define right where "right = {x. jumpF f (at_right x)  0  0  x  x < 1}"
        have jumpF_nz:"jumpF f (at_left x) = 0" "jumpF f (at_right x) = 0"
          when "0<x" "x<1" for x
        proof -
          have "isCont f x" unfolding f_def 
            using asm[rule_format,of x] that
            by (auto intro!:continuous_intros isCont_Im isCont_Re)
          then have "continuous (at_left x) f" "continuous (at_right x) f"
            using continuous_at_split by blast+
          then show "jumpF f (at_left x) = 0" "jumpF f (at_right x) = 0"
            using jumpF_not_infinity by auto
        qed
        have "cindex_pathE ?g z = sum (λx. jumpF f (at_right x)) right 
            - sum (λx. jumpF f (at_left x)) left"
          unfolding cindex_pathE_def cindexE_def right_def left_def 
          by (fold f_def,simp)
        moreover have "sum (λx. jumpF f (at_right x)) right = jumpF_pathstart ?g z"
        proof (cases " jumpF f (at_right 0) = 0")
          case True
          hence False if "x  right" for x using that
            by (cases "x = 0") (auto simp: jumpF_nz right_def)
          then have "right = {}" by blast
          then show ?thesis 
            unfolding jumpF_pathstart_def using True
            apply (fold f_def)
            by auto  
        next
          case False
          hence "x  right  x = 0" for x using that
            by (cases "x = 0") (auto simp: jumpF_nz right_def)
          then have "right = {0}" by blast
          then show ?thesis 
            unfolding jumpF_pathstart_def using False
            apply (fold f_def)
            by auto
        qed
        moreover have "sum (λx. jumpF f (at_left x)) left = jumpF_pathfinish ?g z"
        proof (cases " jumpF f (at_left 1) = 0")
          case True
          then have "left = {}"
            unfolding left_def using jumpF_nz by force
          then show ?thesis 
            unfolding jumpF_pathfinish_def using True
            apply (fold f_def)
            by auto  
        next
          case False
          then have "left = {1}"
            unfolding left_def using jumpF_nz by force
          then show ?thesis 
            unfolding jumpF_pathfinish_def using False
            apply (fold f_def)
            by auto
        qed
        ultimately show ?thesis by auto
      qed
      moreover have jF_start:"jumpF_pathstart ?g z = 
          (if c1=0  c2 0  d1 0 then 
            if c2 >0  d1 > 0 then 1/2 else -1/2
          else 
            0)"
      proof -
        define f where "f=(λt. (Im b - Im a )* t + d1)"
        define g where "g=(λt. (Re b - Re a )* t + c1)"
        have jump_eq:"jumpF_pathstart (linepath a b) z = jumpF (λt. f t/g t) (at_right 0)"
          unfolding jumpF_pathstart_def f_def linepath_def g_def d1_def c1_def
          by (auto simp add:algebra_simps)
        have ?thesis when "¬ (c1 =0  c2 0  d1 0)"
        proof -
          have "c2=0  c10" using ¬ (c1=0  c2=0) by auto
          moreover have "d1 =0  c10" 
          proof (rule ccontr)
            assume "¬ (d1 = 0  c1  0)"
            then have "a=z" unfolding d1_def c1_def by (simp add: complex_eqI)  
            then have "zpath_image (linepath a b)" by auto
            then show False using zclosed_segment a b by auto
          qed    
          moreover have ?thesis when "c10" 
          proof -
            have "jumpF (λt. f t/g t) (at_right 0) = 0" 
              apply (rule jumpF_not_infinity)
               apply (unfold f_def g_def)
              using that by (auto intro!: continuous_intros) 
            then show ?thesis using jump_eq using that by auto
          qed
          ultimately show ?thesis using that by blast
        qed
        moreover have ?thesis when "c1=0" "c2 0" "d1 0" "c2 >0  d1 > 0"  
        proof -
          have "(LIM x at_right 0. f x / g x :> at_top)"
          proof -
            have "(f  d1) (at_right 0)"
              unfolding f_def by (auto intro!: tendsto_eq_intros)
            moreover have "(g  0) (at_right 0)" 
              unfolding g_def using c1=0 by (auto intro!: tendsto_eq_intros)
            moreover have "(g has_sgnx sgn d1) (at_right 0)"
            proof -  
              have "(g has_sgnx sgn (c2-c1)) (at_right 0)"
                unfolding g_def 
                apply (rule has_sgnx_derivative_at_right)
                subgoal unfolding c2_def c1_def d1_def by (auto intro!: derivative_eq_intros)
                subgoal using c1=0 by auto
                subgoal using c1=0 c20 by auto
                done    
              moreover have "sgn (c2-c1) = sgn d1" using that by fastforce
              ultimately show ?thesis by auto
            qed
            ultimately show ?thesis   
              using filterlim_divide_at_bot_at_top_iff[of f d1 "at_right 0" g] d10 by auto
          qed
          then have "jumpF (λt. f t/g t) (at_right 0) = 1/2" unfolding jumpF_def by auto
          then show ?thesis using that jump_eq by auto
        qed
        moreover have ?thesis when "c1=0" "c2 0" "d1 0" "¬ c2 >0  d1 > 0"  
        proof -
          have "(LIM x at_right 0. f x / g x :> at_bot)"
          proof -
            have "(f  d1) (at_right 0)"
              unfolding f_def by (auto intro!: tendsto_eq_intros)
            moreover have "(g  0) (at_right 0)" 
              unfolding g_def using c1=0 by (auto intro!: tendsto_eq_intros)
            moreover have "(g has_sgnx - sgn d1) (at_right 0)"
            proof -  
              have "(g has_sgnx sgn (c2-c1)) (at_right 0)"
                unfolding g_def 
                apply (rule has_sgnx_derivative_at_right)
                subgoal unfolding c2_def c1_def d1_def by (auto intro!: derivative_eq_intros)
                subgoal using c1=0 by auto
                subgoal using c1=0 c20 by auto
                done    
              moreover have "sgn (c2-c1) = - sgn d1" using that by fastforce
              ultimately show ?thesis by auto
            qed
            ultimately show ?thesis   
              using filterlim_divide_at_bot_at_top_iff[of f d1 "at_right 0" g] d10 by auto
          qed
          then have "jumpF (λt. f t/g t) (at_right 0) = - 1/2" unfolding jumpF_def by auto
          then show ?thesis using that jump_eq by auto
        qed  
        ultimately show ?thesis by fast        
      qed
      moreover have jF_finish:"jumpF_pathfinish ?g z = 
          (if c2=0  c1 0  d2 0 then 
            if c1 >0  d2 > 0 then 1/2 else -1/2
          else 
            0)"
      proof -
        define f where "f=(λt. (Im b - Im a )* t + (Im a - Im z))"
        define g where "g=(λt. (Re b - Re a )* t + (Re a - Re z))"
        have jump_eq:"jumpF_pathfinish (linepath a b) z = jumpF (λt. f t/g t) (at_left 1)"
          unfolding jumpF_pathfinish_def f_def linepath_def g_def d1_def c1_def
          by (auto simp add:algebra_simps)
        have ?thesis when "¬ (c2 =0  c1 0  d2 0)"
        proof -
          have "c1=0  c20" using ¬ (c1=0  c2=0) by auto
          moreover have "d2 =0  c20" 
          proof (rule ccontr)
            assume "¬ (d2 = 0  c2  0)"
            then have "b=z" unfolding d2_def c2_def by (simp add: complex_eqI)  
            then have "zpath_image (linepath a b)" by auto
            then show False using zclosed_segment a b by auto
          qed    
          moreover have ?thesis when "c20" 
          proof -
            have "jumpF (λt. f t/g t) (at_left 1) = 0" 
              apply (rule jumpF_not_infinity)
               apply (unfold f_def g_def)
              using that unfolding c2_def by (auto intro!: continuous_intros) 
            then show ?thesis using jump_eq using that by auto
          qed
          ultimately show ?thesis using that by blast
        qed
        moreover have ?thesis when "c2=0" "c1 0" "d2 0" "c1 >0  d2 > 0"  
        proof -
          have "(LIM x at_left 1. f x / g x :> at_top)"
          proof -
            have "(f  d2) (at_left 1)"
              unfolding f_def d2_def by (auto intro!: tendsto_eq_intros)
            moreover have "(g  0) (at_left 1)" 
              using c2=0 unfolding g_def c2_def by (auto intro!: tendsto_eq_intros)
            moreover have "(g has_sgnx sgn d2) (at_left 1)"
            proof -  
              have "(g has_sgnx - sgn (c2-c1)) (at_left 1)"
                unfolding g_def 
                apply (rule has_sgnx_derivative_at_left)
                subgoal unfolding c2_def c1_def d1_def by (auto intro!: derivative_eq_intros)
                subgoal using c2=0 unfolding c2_def by auto
                subgoal using c2=0 c10 by auto
                done    
              moreover have "- sgn (c2-c1) = sgn d2" using that by fastforce
              ultimately show ?thesis by auto
            qed
            ultimately show ?thesis   
              using filterlim_divide_at_bot_at_top_iff[of f d2 "at_left 1" g] d20 by auto
          qed
          then have "jumpF (λt. f t/g t) (at_left 1) = 1/2" unfolding jumpF_def by auto
          then show ?thesis using that jump_eq by auto
        qed
        moreover have ?thesis when "c2=0" "c1 0" "d2 0" "¬ c1 >0  d2 > 0"  
        proof -
          have "(LIM x at_left 1. f x / g x :> at_bot)"
          proof -
            have "(f  d2) (at_left 1)"
              unfolding f_def d2_def by (auto intro!: tendsto_eq_intros)
            moreover have "(g  0) (at_left 1)" 
              using c2=0 unfolding g_def c2_def by (auto intro!: tendsto_eq_intros)
            moreover have "(g has_sgnx - sgn d2) (at_left 1)"
            proof -  
              have "(g has_sgnx - sgn (c2-c1)) (at_left 1)"
                unfolding g_def 
                apply (rule has_sgnx_derivative_at_left)
                subgoal unfolding c2_def c1_def d1_def by (auto intro!: derivative_eq_intros)
                subgoal using c2=0 unfolding c2_def by auto
                subgoal using c2=0 c10 by auto
                done    
              moreover have "sgn (c2-c1) = sgn d2" using that by fastforce
              ultimately show ?thesis by auto
            qed
            ultimately show ?thesis   
              using filterlim_divide_at_bot_at_top_iff[of f d2 "at_left 1" g] d20 by auto
          qed
          then have "jumpF (λt. f t/g t) (at_left 1) = - 1/2" unfolding jumpF_def by auto
          then show ?thesis using that jump_eq by auto
        qed
        ultimately show ?thesis by fast  
      qed
      ultimately show ?thesis using ¬ ((c1>0  c2<0)  (c1<0  c2>0))
        apply (fold c1_def c2_def d1_def d2_def)
        by auto
    qed
    moreover have ?thesis when "c1=0" "c2=0"
    proof -
      have "(λt. Re (linepath a b t - z)) = (λ_. 0)"
        using that unfolding linepath_def c1_def c2_def  
        by (auto simp add:algebra_simps)
      then have "(λt. Im (linepath a b t - z) / Re (linepath a b t - z)) = (λ_. 0)"
        by (metis div_by_0)
      then have "cindex_pathE (linepath a b) z = 0" 
        unfolding cindex_pathE_def
        by (auto intro: cindexE_constI)
      thus ?thesis using ¬ ((c1>0  c2<0)  (c1<0  c2>0)) that 
        apply (fold c1_def c2_def d1_def d2_def)
        by auto
    qed    
    ultimately show ?thesis by fast
  qed
  moreover have ?thesis when c1c2_diff_sgn:"(c1>0  c2<0)  (c1<0  c2>0)"
  proof -
    define f where "f=(λt. (Im b - Im a )* t + (Im a - Im z))"
    define g where "g=(λt. (Re b - Re a )* t + (Re a - Re z))"
    define h where "h=(λt. f t/ g t)"
    define c3 where "c3=Im(a)*Re(b)+Re(z)*Im(b)+Im(z)*Re(a) -Im(z)*Re(b) - Im(b)*Re(a) - Re(z)*Im(a)"
    define u where "u = (Re z - Re a) / (Re b - Re a)"
    let ?g = "λt. linepath a b t - z"
    have "0<u" "u<1" "Re b - Re a0" using that unfolding u_def c1_def c2_def by (auto simp add:field_simps)
    have "Re(?g u) = 0" "g u=0" unfolding linepath_def u_def g_def  
      apply (auto simp add:field_simps)
      using Re b - Re a0 by (auto simp add:field_simps)
    moreover have "u1 = u2" when "Re(?g u1) = 0" "Re(?g u2) = 0" for u1 u2
    proof -
      have " (u1 - u2) * (Re b - Re a) = Re(?g u1) - Re(?g u2)" 
        unfolding linepath_def by (auto simp add:algebra_simps)
      also have "... = 0" using that by auto
      finally have "(u1 - u2) * (Re b - Re a) = 0" .
      thus ?thesis using Re b - Re a0 by auto
    qed
    ultimately have re_g_iff:"Re(?g t) = 0  t=u" for t by blast
     
    have "cindex_pathE (linepath a b) z = jumpF h (at_right u) - jumpF h (at_left u)"
    proof -
      define left where "left = {x. jumpF h (at_left x)  0  0 < x  x  1}"
      define right where "right = {x. jumpF h (at_right x)  0  0  x  x < 1}"
      have jumpF_nz:"jumpF h (at_left x) = 0" "jumpF h (at_right x) = 0"
        when "0x" "x1" "xu" for x
      proof -
        have "g x0" 
          using re_g_iff xu unfolding g_def linepath_def
          by (metis Re b - Re a  0 add_diff_cancel_left' diff_diff_eq2 diff_zero 
              nonzero_mult_div_cancel_left u_def)
        then have "isCont h x" 
          unfolding h_def f_def g_def
          by (auto intro!:continuous_intros)
        then have "continuous (at_left x) h" "continuous (at_right x) h"
          using continuous_at_split by blast+
        then show "jumpF h (at_left x) = 0" "jumpF h(at_right x) = 0"
          using jumpF_not_infinity by auto
      qed
      have "cindex_pathE (linepath a b) z = sum (λx. jumpF h (at_right x)) right 
            - sum (λx. jumpF h (at_left x)) left"
      proof -
        have "cindex_pathE (linepath a b) z = cindexE 0 1 (λt. Im (?g t) / Re (?g t))"
          unfolding cindex_pathE_def by auto
        also have "... = cindexE 0 1 h"
        proof -
          have "(λt. Im (?g t) / Re (?g t)) = h"
            unfolding h_def f_def g_def linepath_def 
            by (auto simp add:algebra_simps)
          then show ?thesis by auto
        qed
        also have "... = sum (λx. jumpF h (at_right x)) right - sum (λx. jumpF h (at_left x)) left"
          unfolding cindexE_def left_def right_def by auto
        finally show ?thesis .
      qed
      moreover have "sum (λx. jumpF h (at_right x)) right = jumpF h (at_right u)"
      proof (cases " jumpF h (at_right u) = 0")
        case True
        then have "right = {}"
          unfolding right_def using jumpF_nz by force
        then show ?thesis using True by auto 
      next
        case False
        then have "right = {u}"
          unfolding right_def using jumpF_nz 0<u u<1 by fastforce 
        then show ?thesis by auto
      qed
      moreover have "sum (λx. jumpF h (at_left x)) left = jumpF h (at_left u)"
      proof (cases " jumpF h (at_left u) = 0")
        case True
        then have "left = {}"
          unfolding left_def 
          apply safe
          apply (case_tac "x=u")
          using jumpF_nz 0<u u<1 by auto
        then show ?thesis using True by auto
      next
        case False
        then have "left = {u}"
          unfolding left_def 
          apply safe
            apply (case_tac "x=u")
          using jumpF_nz 0<u u<1 by auto
        then show ?thesis by auto
      qed
      ultimately show ?thesis by auto
    qed
    moreover have "jump h u = (if c3>0 then 1 else -1)" 
    proof -
      have "Re b-Re a0" using c1c2_diff_sgn unfolding c1_def c2_def by auto 
      have "jump (λt. Im(?g t) / Re(?g t)) u = jump h u"
        apply (rule arg_cong2[where f=jump])
        unfolding linepath_def h_def f_def g_def by (auto simp add:algebra_simps)
      moreover have "jump (λt. Im(?g t) / Re(?g t)) u 
          = (if sgn (Re b -Re a) = sgn (Im(?g u)) then 1 else - 1)" 
      proof (rule jump_divide_derivative)
        have "path ?g" using path_offset by auto
        then have "continuous_on {0..1} (λt. Im(?g t))" 
          using continuous_on_Im path_def by blast
        then show "isCont (λt. Im (?g t)) u"
          unfolding path_def
          apply (elim continuous_on_interior)
          using 0<u u<1 by auto
      next
        show "Re(?g u) = 0" "Re b - Re a  0" using Re(?g u) = 0 Re b - Re a  0
          by auto
        show "Im(?g u)  0" 
        proof (rule ccontr)
          assume "¬ Im (linepath a b u - z)  0 "
          then have "?g u = 0" using Re(?g u) = 0 
            by (simp add: complex_eq_iff)
          then have "z  closed_segment a b" using 0<u u<1
            by (auto intro:linepath_in_path)
          thus False using z  closed_segment a b by simp   
        qed
        show "((λt. Re (linepath a b t - z)) has_real_derivative Re b - Re a) (at u)"
          unfolding linepath_def by (auto intro!:derivative_eq_intros)
      qed
      moreover have "sgn (Re b - Re a) = sgn (Im(?g u))  c3 > 0"   
      proof -
        have "Im(?g u) = c3/(Re b-Re a)"
        proof -
          define ba where "ba = Re b-Re a"
          have "ba0"  using Re b - Re a  0 unfolding ba_def by auto
          then show ?thesis
            unfolding linepath_def u_def c3_def
            apply (fold ba_def)
            apply (auto simp add:field_simps)  
            by (auto simp add:algebra_simps ba_def)
        qed
        then have "sgn (Re b - Re a) = sgn (Im(?g u))  sgn (Re b - Re a) = sgn (c3/(Re b-Re a))"
          by auto
        also have "...  c3>0"
          using Re b-Re a0
          apply (cases "0::real" c3 rule:linorder_cases)
          by (auto simp add:sgn_zero_iff)
        finally show ?thesis .
      qed 
      ultimately show ?thesis by auto
    qed
    moreover have "jump h u = jumpF h (at_right u) - jumpF h (at_left u)"
    proof (rule jump_jumpF)
      have "f u0" 
      proof (rule ccontr)
        assume "¬ f u  0"
        then have "zpath_image (linepath a b)" 
          unfolding path_image_def
          apply (rule_tac rev_image_eqI[of u])
          using re_g_iff[of u,simplified] 0<u u<1 
          unfolding f_def linepath_def 
          by (auto simp add:algebra_simps complex.expand)  
        then show False using zclosed_segment a b by simp
      qed
      then show "isCont (inverse  h) u"
        unfolding h_def comp_def f_def g_def
        by (auto intro!: continuous_intros)
      define hs where "hs = sgn ((f u) / (c2 -c1))"     
      show "(h has_sgnx -hs) (at_left u)" "(h has_sgnx hs) (at_right u)"    
      proof -
        have ff:"(f has_sgnx sgn (f u)) (at_left u)" "(f has_sgnx sgn (f u)) (at_right u)" 
        proof -
          have "(f  f u) (at u)"
            unfolding f_def by (auto intro!:tendsto_intros)
          then have " (f has_sgnx sgn (f u)) (at u)"  
            using tendsto_nonzero_has_sgnx[of f, OF _ f u0] by auto
          then show "(f has_sgnx sgn (f u)) (at_left u)" "(f has_sgnx sgn (f u)) (at_right u)" 
            using has_sgnx_split by blast+
        qed
        have gg:"(g has_sgnx - sgn (c2 - c1)) (at_left u)" "(g has_sgnx sgn (c2 - c1)) (at_right u)" 
        proof -
          have "(g has_real_derivative c2 - c1) (at u)" unfolding g_def c1_def c2_def
            by (auto intro!:derivative_eq_intros)
          moreover have "c2 - c1  0" using that by auto
          ultimately show "(g has_sgnx sgn (c2 - c1)) (at_right u)" 
              "(g has_sgnx - sgn (c2 - c1)) (at_left u)"
            using has_sgnx_derivative_at_right[of g "c2-c1" u] 
                has_sgnx_derivative_at_left[of g "c2-c1" u] g u=0
            by auto
        qed
        show "(h has_sgnx - hs) (at_left u)"
          using has_sgnx_divide[OF ff(1) gg(1)] unfolding h_def hs_def 
          by auto  
        show "(h has_sgnx hs) (at_right u)"    
          using has_sgnx_divide[OF ff(2) gg(2)] unfolding h_def hs_def 
          by auto 
      qed
      show "hs0" "-hs0"
        unfolding hs_def using f u0 that by (auto simp add:sgn_if)
    qed
    ultimately show ?thesis using that 
      apply (fold c1_def c2_def c3_def)
      by auto
  qed
  ultimately show ?thesis by fast
qed
  
lemma cindex_path_linepath:
  assumes "zpath_image (linepath a b)"
  shows "cindex_path (linepath a b) z = (
    let c1=Re(a)-Re(z) ; c2=Re(b)-Re(z) ; 
        c3 = Im(a)*Re(b)+Re(z)*Im(b)+Im(z)*Re(a) -Im(z)*Re(b) - Im(b)*Re(a) - Re(z)*Im(a)
    in if (c1>0  c2<0)  (c1<0  c2>0) then (if c3>0 then 1 else -1) else 0)"  
proof -
  define c1 c2 where "c1=Re(a)-Re(z)" and "c2=Re(b)-Re(z)"
  let ?g = "linepath a b"
  have ?thesis when "¬ ((c1>0  c2<0)  (c1<0  c2>0))"   
  proof -
    have "Re a= Re z  Re b=Re z"
      when "0<t" "t<1" and asm:"(1-t)*Re a + t * Re b = Re z" for t
      unfolding c1_def c2_def using that  
    proof -
      have ?thesis when "c10" "c10"
      proof -
        have "Re a=Re z" using that unfolding c1_def by auto
        then show ?thesis using 0<t t<1 asm
          apply (cases "Re b" "Re z" rule:linorder_cases)
            apply (auto simp add:field_simps)
          done
      qed
      moreover have ?thesis when "c10" "c20"
      proof -  
        have False when "c1<0"
        proof -
          have "(1 - t) * Re a < (1 - t) * Re z"
            using t<1 c1<0 unfolding c1_def by auto
          moreover have "t * Re b  t* Re z" using t>0 c20 unfolding c2_def by auto
          ultimately have "(1 - t) * Re a + t * Re b < (1 - t) * Re z + t * Re z"
            by auto
          thus False using asm by (auto simp add:algebra_simps)
        qed
        moreover have False when "c2<0"
        proof -
          have "(1 - t) * Re a  (1 - t) * Re z"
            using t<1 c10 unfolding c1_def by auto
          moreover have "t * Re b < t* Re z" using t>0 c2<0 unfolding c2_def by auto
          ultimately have "(1 - t) * Re a + t * Re b < (1 - t) * Re z + t * Re z"
            by auto
          thus False using asm by (auto simp add:algebra_simps)
        qed
        ultimately show ?thesis using that unfolding c1_def c2_def by argo
      qed
      moreover have ?thesis when "c20" "c20"
      proof -
        have "Re b=Re z" using that unfolding c2_def by auto
        then have "(1 - t) * Re a = (1-t)*Re z" using asm by (auto simp add:field_simps)
        then have "Re a= Re z" using t<1 by auto
        then show ?thesis using Re b=Re z by auto
      qed
      moreover have ?thesis when "c10" "c20"
      proof -  
        have False when "c1>0"
        proof -
          have "(1 - t) * Re a > (1 - t) * Re z"
            using t<1 c1>0 unfolding c1_def by auto
          moreover have "t * Re b  t* Re z" using t>0 c20 unfolding c2_def by auto
          ultimately have "(1 - t) * Re a + t * Re b > (1 - t) * Re z + t * Re z"
            by auto
          thus False using asm by (auto simp add:algebra_simps)
        qed
        moreover have False when "c2>0"
        proof -
          have "(1 - t) * Re a  (1 - t) * Re z"
            using t<1 c10 unfolding c1_def by auto
          moreover have "t * Re b > t* Re z" using t>0 c2>0 unfolding c2_def by auto
          ultimately have "(1 - t) * Re a + t * Re b > (1 - t) * Re z + t * Re z"
            by auto
          thus False using asm by (auto simp add:algebra_simps)
        qed
        ultimately show ?thesis using that unfolding c1_def c2_def by argo
      qed
      moreover have "c10  c20" "c10  c20" using ¬ ((c1>0  c2<0)  (c1<0  c2>0)) by auto
      ultimately show ?thesis by fast
    qed
    then have "(t. 0<t  t<1  Re(linepath a b t - z)  0)  (Re a= Re z  Re b=Re z)" 
      using that unfolding linepath_def by auto
    moreover have ?thesis when asm:"t. 0<t  t<1  Re(linepath a b t - z)  0"
    proof -
      have "jump (λt. Im (linepath a b t - z) / Re (linepath a b t - z)) t = 0" 
        when "0<t" "t<1" for t
        apply (rule jump_Im_divide_Re_0[of "λt. linepath a b t - z", 
              OF _ asm[rule_format]])
        by (auto simp add:path_offset that)
      then have "cindex_path (linepath a b) z = 0"
        unfolding cindex_path_def cindex_def by auto
      thus ?thesis using ¬ ((c1>0  c2<0)  (c1<0  c2>0)) 
        apply (fold c1_def c2_def)
        by auto
    qed
    moreover have ?thesis when "Re a= Re z" "Re b=Re z"
    proof -
      have "(λt. Re (linepath a b t - z)) = (λ_. 0)"
        unfolding linepath_def using Re a= Re z Re b=Re z 
        by (auto simp add:algebra_simps)
      then have "(λt. Im (linepath a b t - z) / Re (linepath a b t - z)) = (λ_. 0)"
        by (metis div_by_0)
      then have "jump (λt. Im (linepath a b t - z) / Re (linepath a b t - z)) t = 0" for t
        using jump_const by auto
      then have "cindex_path (linepath a b) z = 0"
        unfolding cindex_path_def cindex_def by auto
      thus ?thesis using ¬ ((c1>0  c2<0)  (c1<0  c2>0)) 
        apply (fold c1_def c2_def)
        by auto
    qed    
    ultimately show ?thesis by auto
  qed
  moreover have ?thesis when c1c2_diff_sgn:"(c1>0  c2<0)  (c1<0  c2>0)"
  proof -
    define c3 where "c3=Im(a)*Re(b)+Re(z)*Im(b)+Im(z)*Re(a) -Im(z)*Re(b) - Im(b)*Re(a) - Re(z)*Im(a)"
    define u where "u = (Re z - Re a) / (Re b - Re a)"
    let ?g = "λt. linepath a b t - z"
    have "0<u" "u<1" "Re b - Re a0" using that unfolding u_def c1_def c2_def by (auto simp add:field_simps)
    have "Re(?g u) = 0" unfolding linepath_def u_def  
      apply (auto simp add:field_simps)
      using Re b - Re a0 by (auto simp add:field_simps)
    moreover have "u1 = u2" when "Re(?g u1) = 0" "Re(?g u2) = 0" for u1 u2
    proof -
      have " (u1 - u2) * (Re b - Re a) = Re(?g u1) - Re(?g u2)" 
        unfolding linepath_def by (auto simp add:algebra_simps)
      also have "... = 0" using that by auto
      finally have "(u1 - u2) * (Re b - Re a) = 0" .
      thus ?thesis using Re b - Re a0 by auto
    qed
    ultimately have re_g_iff:"Re(?g t) = 0  t=u" for t by blast
    have "cindex_path (linepath a b) z = jump (λt. Im (?g t)/Re(?g t)) u" 
    proof -  
      define f where "f=(λt. Im (linepath a b t - z) / Re (linepath a b t - z))"
      have "jump f t =0" when "tu" "0<t" "t<1" for t
        unfolding f_def 
        apply (rule jump_Im_divide_Re_0)
        using that re_g_iff by (auto simp add: path_offset)
      then have "{x. jump f x  0  0 < x  x < 1} = (if jump f u=0 then {} else {u})"
        using 0<u u<1 
        apply auto
        by fastforce
      then show ?thesis
        unfolding cindex_path_def cindex_def 
        apply (fold f_def)
        by auto
    qed  
    moreover have "jump (λt. Im (?g t)/Re(?g t)) u = (if c3>0 then 1 else -1)" 
    proof -
      have "Re b-Re a0" using c1c2_diff_sgn unfolding c1_def c2_def by auto  
      have "jump (λt. Im(?g t) / Re(?g t)) u 
          = (if sgn (Re b -Re a) = sgn (Im(?g u)) then 1 else - 1)" 
      proof (rule jump_divide_derivative)
        have "path ?g" using path_offset by auto
        then have "continuous_on {0..1} (λt. Im(?g t))" 
          using continuous_on_Im path_def by blast
        then show "isCont (λt. Im (?g t)) u"
          unfolding path_def
          apply (elim continuous_on_interior)
          using 0<u u<1 by auto
      next
        show "Re(?g u) = 0" "Re b - Re a  0" using Re(?g u) = 0 Re b - Re a  0
          by auto
        show "Im(?g u)  0" 
        proof (rule ccontr)
          assume "¬ Im (linepath a b u - z)  0 "
          then have "?g u = 0" using Re(?g u) = 0 
            by (simp add: complex_eq_iff)
          thus False using assms 0<u u<1 unfolding path_image_def by fastforce
        qed
        show "((λt. Re (linepath a b t - z)) has_real_derivative Re b - Re a) (at u)"
          unfolding linepath_def by (auto intro!:derivative_eq_intros)
      qed
      moreover have "sgn (Re b - Re a) = sgn (Im(?g u))  c3 > 0"   
      proof -
        have "Im(?g u) = c3/(Re b-Re a)"
        proof -
          define ba where "ba = Re b-Re a"
          have "ba0"  using Re b - Re a  0 unfolding ba_def by auto
          then show ?thesis
            unfolding linepath_def u_def c3_def
            apply (fold ba_def)
            apply (auto simp add:field_simps)  
            by (auto simp add:algebra_simps ba_def)
        qed
        then have "sgn (Re b - Re a) = sgn (Im(?g u))  sgn (Re b - Re a) = sgn (c3/(Re b-Re a))"
          by auto
        also have "...  c3>0"
          using Re b-Re a0
          apply (cases "0::real" c3 rule:linorder_cases)
          by (auto simp add:sgn_zero_iff)
        finally show ?thesis .
      qed 
      ultimately show ?thesis by auto
    qed
    ultimately show ?thesis using c1c2_diff_sgn
      apply (fold c1_def c2_def c3_def)
      by auto
  qed
  ultimately show ?thesis by blast  
qed

lemma cindex_pathE_part_circlepath:
  assumes "cmod (z-z0) r" and "r>0" "0st" "st<tt" "tt2*pi"
  shows "cindex_pathE (part_circlepath z r st tt) z0 = (
    if ¦Re z - Re z0¦ < r then 
      (let
          θ = arccos ((Re z0 - Re z)/r);
          β = 2*pi - θ
        in
          jumpF_pathstart (part_circlepath z r st tt) z0
          +
          (if st<θ  θ<tt then if r * sin θ + Im z > Im z0 then -1 else 1 else 0)
          +
          (if st<β  β < tt then if r * sin β + Im z > Im z0 then 1 else -1 else 0)
          - 
          jumpF_pathfinish (part_circlepath z r st tt) z0
      )
    else 
      if ¦Re z - Re z0¦ = r then 
        jumpF_pathstart (part_circlepath z r st tt) z0 
        - jumpF_pathfinish (part_circlepath z r st tt) z0 
      else 0
    )" 
proof -
  define f where "f=(λi. r * sin i + Im z - Im z0)"
  define g where "g=(λi. r * cos i + Re z - Re z0)"
  define h where "h=(λt. f t / g t)"
  have index_eq:"cindex_pathE (part_circlepath z r st tt) z0 = cindexE st tt h"
  proof -
    have "cindex_pathE (part_circlepath z r st tt) z0 
      = cindexE 0 1 ((λi. f i/g i) o (linepath st tt))"
      unfolding cindex_pathE_def part_circlepath_def exp_Euler f_def g_def comp_def
      by (simp add:cos_of_real sin_of_real algebra_simps)
    also have "... = cindexE st tt (λi. f i/g i)"   
      unfolding linepath_def using cindexE_linear_comp[of "tt-st" 0 1 _ st] st<tt
      by (simp add:algebra_simps)
    also have "... = cindexE st tt h" unfolding h_def by simp
    finally show ?thesis .
  qed
  have jstart_eq:"jumpF_pathstart (part_circlepath z r st tt) z0 = jumpF h (at_right st)"
  proof -
    have "jumpF_pathstart (part_circlepath z r st tt) z0 
            = jumpF ((λi. f i/g i) o (linepath st tt)) (at_right 0) "
      unfolding jumpF_pathstart_def part_circlepath_def exp_Euler f_def g_def comp_def 
      by (simp add:cos_of_real sin_of_real algebra_simps)
    also have "... = jumpF (λi. f i/g i) (at_right st)"
      unfolding linepath_def using jumpF_linear_comp(2)[of "tt-st" _ st 0] st<tt
      by (simp add:algebra_simps)
    also have "... = jumpF h (at_right st)" unfolding h_def by simp
    finally show ?thesis .
  qed
  have jfinish_eq:"jumpF_pathfinish (part_circlepath z r st tt) z0 = jumpF h (at_left tt)"
  proof -
    have "jumpF_pathfinish (part_circlepath z r st tt) z0 
            = jumpF ((λi. f i/g i) o (linepath st tt)) (at_left 1) "
      unfolding jumpF_pathfinish_def part_circlepath_def exp_Euler f_def g_def comp_def 
      by (simp add:cos_of_real sin_of_real algebra_simps)
    also have "... = jumpF (λi. f i/g i) (at_left tt)"
      unfolding linepath_def using jumpF_linear_comp(1)[of "tt-st" _ st 1] st<tt
      by (simp add:algebra_simps)
    also have "... = jumpF h (at_left tt)" unfolding h_def by simp
    finally show ?thesis .
  qed  
  have finite_jFs:"finite_jumpFs h st tt"
  proof -
    note finite_ReZ_segments_imp_jumpFs[OF finite_ReZ_segments_part_circlepath
          ,of  z r st tt z0,simplified]
    then have "finite_jumpFs ((λi. f i/g i) o (linepath st tt)) 0 1"
      unfolding h_def f_def g_def part_circlepath_def exp_Euler comp_def
      by (simp add:cos_of_real sin_of_real algebra_simps)
    then have "finite_jumpFs (λi. f i/g i) st tt"
      unfolding linepath_def using finite_jumpFs_linear_pos[of "tt-st" _ st 0 1] st<tt 
      by (simp add:algebra_simps)
    then show ?thesis unfolding h_def by auto
  qed
  have g_imp_f:"g i = 0  f i0" for i 
  proof (rule ccontr)
    assume "g i = 0" "¬ f i  0 "
    then have "r * sin i = Im (z0 - z)" "r * cos i = Re (z0 - z)" 
      unfolding f_def g_def by auto
    then have "(r * sin i) ^2 + (r * cos i)^2 = Im (z0 - z) ^ 2 +  Re (z0 - z) ^2" 
      by auto
    then have "r^2 * (sin i ^2  + cos i^2) = Im (z0 - z) ^ 2 +  Re (z0 - z) ^2" 
      by (auto simp only:algebra_simps power_mult_distrib)    
    then have "r^2 = cmod (z0-z) ^ 2"   
      unfolding cmod_def by auto
    then have "r = cmod (z0-z)"
      using r>0 power2_eq_imp_eq by fastforce
    then show False using cmod (z-z0) r using norm_minus_commute by blast
  qed  
  have ?thesis when "¦Re z - Re z0¦ > r"
  proof -      
    have "jumpF h (at_right x) = 0" "jumpF h (at_left x) = 0" for x
    proof -
      have "g x 0" 
      proof (rule ccontr)
        assume "¬ g x  0"
        then have "cos x = (Re z0 - Re z) / r" unfolding g_def using r>0  
          by (auto simp add:field_simps)
        then have "¦(Re z0 - Re z)/r¦  1"
          by (metis abs_cos_le_one)
        then have "¦Re z0 - Re z¦  r"
          using r>0 by (auto simp add:field_simps)
        then show False using that by auto
      qed    
      then have "isCont h x" 
        unfolding h_def f_def g_def by (auto intro:continuous_intros)
      then show "jumpF h (at_right x) = 0" "jumpF h (at_left x) = 0"
        using jumpF_not_infinity unfolding continuous_at_split by auto
    qed
    then have "cindexE st tt h = 0" unfolding cindexE_def by auto  
    then show ?thesis using index_eq that by auto 
  qed
  moreover have ?thesis when "¦Re z - Re z0¦ = r" 
  proof -
    define R where "R=(λS.{x. jumpF h (at_right x)  0  xS})"
    define L where "L=(λS.{x. jumpF h (at_left x)  0  xS})"
    define right where 
      "right = (λS. (xR S. jumpF h (at_right x)))"
    define left where 
      "left = (λS. (xL S. jumpF h (at_left x)))"
    have "cindex_pathE (part_circlepath z r st tt) z0 = cindexE st tt h"
      using index_eq by simp
    also have "... = right {st..<tt} - left {st<..tt}"
      unfolding cindexE_def right_def left_def R_def L_def by auto
    also have "... = jumpF h (at_right st) +  right {st<..<tt} - left {st<..<tt} - jumpF h (at_left tt)"
    proof -
      have "right {st..<tt} = jumpF h (at_right st) +  right {st<..<tt}"
      proof (cases "jumpF h (at_right st) =0")
        case True
        then have "R {st..<tt} = R {st<..<tt}"
          unfolding R_def using less_eq_real_def by auto
        then have "right {st..<tt} = right {st<..<tt}"
          unfolding right_def by auto
        then show ?thesis using True by auto
      next
        case False
        have "finite (R {st..<tt})"
          using finite_jFs unfolding R_def finite_jumpFs_def 
          by (auto elim:rev_finite_subset)
        moreover have "st  R {st..<tt}" using False st<tt unfolding R_def by auto
        moreover have "R {st..<tt} - {st} = R {st<..<tt}" unfolding R_def by auto
        ultimately show "right {st..<tt}= jumpF h (at_right st) 
            + right {st<..<tt}"
          using sum.remove[of "R {st..<tt}" st "λx. jumpF h (at_right x)"]
          unfolding right_def by simp
      qed
      moreover have "left {st<..tt} = jumpF h (at_left tt) +  left {st<..<tt}"
      proof (cases "jumpF h (at_left tt) =0")
        case True
        then have "L {st<..tt} = L {st<..<tt}"
          unfolding L_def using less_eq_real_def by auto
        then have "left {st<..tt} = left {st<..<tt}"
          unfolding left_def by auto
        then show ?thesis using True by auto
      next
        case False
        have "finite (L {st<..tt})"
          using finite_jFs unfolding L_def finite_jumpFs_def 
          by (auto elim:rev_finite_subset)
        moreover have "tt  L {st<..tt}" using False st<tt unfolding L_def by auto
        moreover have "L {st<..tt} - {tt} = L {st<..<tt}" unfolding L_def by auto
        ultimately show "left {st<..tt}= jumpF h (at_left tt) + left {st<..<tt}"
          using sum.remove[of "L {st<..tt}" tt "λx. jumpF h (at_left x)"]
          unfolding left_def by simp
      qed  
      ultimately show ?thesis by simp
    qed
    also have "... =  jumpF h (at_right st) - jumpF h (at_left tt)"  
    proof -
      define S where "S={x. (jumpF h (at_left x)  0  jumpF h (at_right x)  0)  st < x  x < tt}"
      have "right {st<..<tt} = sum (λx. jumpF h (at_right x)) S"
        unfolding right_def S_def R_def
        apply (rule sum.mono_neutral_left)
        subgoal using finite_jFs unfolding finite_jumpFs_def by (auto elim:rev_finite_subset)
        subgoal by auto
        subgoal by auto
        done
      moreover have "left {st<..<tt} = sum (λx. jumpF h (at_left x)) S"
        unfolding left_def S_def L_def
        apply (rule sum.mono_neutral_left)
        subgoal using finite_jFs unfolding finite_jumpFs_def by (auto elim:rev_finite_subset)
        subgoal by auto
        subgoal by auto
        done   
      ultimately have "right {st<..<tt} - left {st<..<tt} 
          = sum (λx. jumpF h (at_right x) - jumpF h (at_left x)) S"
        by (simp add: sum_subtractf)
      also have "... = 0"
      proof -
        have "jumpF h (at_right i) - jumpF h (at_left i) = 0" when "g i=0" for i
        proof -
          have "(LIM x at i. f x / g x :> at_bot)  (LIM x at i. f x / g x :> at_top)"
          proof -
            have *: "f i f i" "g i 0" "f i  0" 
              using g_imp_f[OF g i=0] g i=0 unfolding f_def g_def 
              by (auto intro!:tendsto_eq_intros)
            have ?thesis when "Re z > Re z0"
            proof -
              have g_alt:"g = (λt. r * cos t + r)" unfolding g_def using ¦Re z - Re z0¦ = r that by auto
              have "(g has_sgnx 1) (at i)" 
              proof -
                have "sgn (g t) = 1" when "t  i " "dist t i < pi" for t
                proof -
                  have "cos i = - 1" using g i =0 r>0 unfolding g_alt 
                    by (metis add.inverse_inverse less_numeral_extra(3) mult_cancel_left 
                        mult_minus1_right real_add_minus_iff)
                  then obtain k::int where k_def:"i = (2 * k + 1) * pi"
                    using cos_eq_minus1[of i] by auto
                  show ?thesis
                  proof (rule ccontr)
                    assume "sgn (g t)  1"
                    then have "cos t + 10" using r>0 unfolding g_alt 
                      by (metis (no_types, opaque_lifting) add_le_same_cancel1 add_minus_cancel 
                          mult_le_cancel_left1 mult_le_cancel_right1 mult_minus_right mult_zero_left 
                          sgn_pos zero_le_one)
                    then have "cos t = -1" 
                      by (metis add.commute cos_ge_minus_one le_less not_less real_add_le_0_iff)
                    then obtain k'::int where k'_def:"t = (2 * k' + 1) * pi"
                      using cos_eq_minus1[of t] by auto  
                    then have "t - i = 2 * pi*(k' - k)"
                      using k_def by (auto simp add:algebra_simps)
                    then have "2  * pi * ¦  (k' - k)¦ < pi" 
                      using dist t i < pi by (simp add:dist_norm abs_mult)
                    from divide_strict_right_mono[OF this, of "2*pi",simplified] have "¦k' - k ¦ < 1/2"
                      by auto
                    then have "k=k'" by linarith
                    then have "t=i" using k_def k'_def by auto
                    then show False using ti by auto
                  qed
                qed
                then show ?thesis unfolding has_sgnx_def eventually_at
                  apply(intro exI[where x="pi"])
                  by auto
              qed
              then show ?thesis using * filterlim_divide_at_bot_at_top_iff[of f "f i" "at i" g]
                by (simp add: sgn_if)
            qed
            moreover have ?thesis when "Re z < Re z0"
            proof -
                have g_alt:"g = (λt. r * cos t - r)" unfolding g_def using ¦Re z - Re z0¦ = r that by auto
                have "(g has_sgnx - 1) (at i)" 
                proof -
                  have "sgn (g t) = - 1" when "t  i " "dist t i < pi" for t
                  proof -
                    have "cos i = 1" using g i =0 r>0 unfolding g_alt by simp
                    then obtain k::int where k_def:"i = (2 * k  * pi)"
                      using cos_one_2pi_int[of i] by auto
                    show ?thesis
                    proof (rule ccontr)
                      assume "sgn (g t)  - 1"
                      then have "cos t - 10" using r>0 unfolding g_alt 
                        using mult_le_cancel_left1 by fastforce
                      then have "cos t = 1" 
                        by (meson cos_le_one diff_ge_0_iff_ge le_less not_less)
                      then obtain k'::int where k'_def:"t = 2 * k'* pi"
                        using cos_one_2pi_int[of t] by auto  
                      then have "t - i = 2 * pi*(k' - k)"
                        using k_def by (auto simp add:algebra_simps)
                      then have "2  * pi * ¦  (k' - k)¦ < pi" 
                        using dist t i < pi by (simp add:dist_norm abs_mult)
                      from divide_strict_right_mono[OF this, of "2*pi",simplified] have "¦k' - k ¦ < 1/2"
                        by auto
                      then have "k=k'" by linarith
                      then have "t=i" using k_def k'_def by auto
                      then show False using ti by auto
                    qed
                  qed
                  then show ?thesis unfolding has_sgnx_def eventually_at
                    apply(intro exI[where x="pi"])
                    by auto
                qed
                then show ?thesis using * filterlim_divide_at_bot_at_top_iff[of f "f i" "at i" g]
                  by (simp add: sgn_if)
            qed
            moreover have "Re z Re z0" using ¦Re z - Re z0¦ = r r>0 by fastforce 
            ultimately show ?thesis by fastforce
          qed
          moreover have ?thesis when "(LIM x at i. f x / g x :> at_bot)"
          proof -
            have "jumpF h (at_right i) = - 1/2" "jumpF h (at_left i) = -1/2"
              using that unfolding jumpF_def h_def filterlim_at_split by auto
            then show ?thesis by auto
          qed
          moreover have ?thesis when "(LIM x at i. f x / g x :> at_top)"
          proof -
            have "jumpF h (at_right i) =  1/2" "jumpF h (at_left i) = 1/2"
              using that unfolding jumpF_def h_def filterlim_at_split by auto
            then show ?thesis by auto
          qed  
          ultimately show ?thesis by auto
        qed
        moreover have "jumpF h (at_right i) - jumpF h (at_left i) = 0" when "g i0" for i 
        proof -
          have "isCont h i" using that unfolding h_def f_def g_def
            by (auto intro!:continuous_intros)
          then have "jumpF h (at_right i) = 0" "jumpF h (at_left i) = 0"  
            using jumpF_not_infinity unfolding continuous_at_split by auto
          then show ?thesis by auto
        qed
        ultimately show ?thesis by (intro sum.neutral,auto)
      qed
      finally show ?thesis by simp
    qed
    also have "... = jumpF_pathstart (part_circlepath z r st tt) z0 
        - jumpF_pathfinish (part_circlepath z r st tt) z0" 
      using jstart_eq jfinish_eq by auto
    finally have "cindex_pathE (part_circlepath z r st tt) z0 = 
        jumpF_pathstart (part_circlepath z r st tt) z0 
        - jumpF_pathfinish (part_circlepath z r st tt) z0"
      .
    then show ?thesis using that by auto
  qed
  moreover have ?thesis when "¦Re z - Re z0¦ < r"
  proof -
    define zr where "zr= (Re z0 - Re z)/r"
    define θ where "θ = arccos zr"
    define β where "β = 2*pi - θ" 
    have "0<θ" "θ<pi"
    proof -
      have "- 1 < zr" "zr < 1"  
        using that r>0 unfolding zr_def by (auto simp add:field_simps)
      from arccos_lt_bounded[OF this] show "0<θ" "θ<pi"
        unfolding θ_def by auto
    qed
    have "g θ = 0" "g β = 0" 
    proof -
      have "¦zr¦1" using that unfolding zr_def by auto
      then have "cos θ = zr" "cos β = cos θ"
        unfolding θ_def[folded zr_def] β_def by auto
      then show "g θ = 0" "g β = 0" unfolding zr_def g_def using r>0 by auto
    qed
    have g_sgnx_θ:"(g has_sgnx 1) (at_left θ)" "(g has_sgnx -1) (at_right θ)"
    proof -
      have "(g has_real_derivative - r * sin θ) (at θ)"
        unfolding g_def by (auto intro!:derivative_eq_intros)
      moreover have "- r * sin θ <0"
        using sin_gt_zero[OF 0<θ θ<pi] r>0 by auto
      ultimately show "(g has_sgnx 1) (at_left θ)" "(g has_sgnx -1) (at_right θ)"
        using has_sgnx_derivative_at_left[of g "- r * sin θ", OF _ g θ=0] 
              has_sgnx_derivative_at_right[of g "- r * sin θ", OF _ g θ=0]
        by force+
    qed
    have g_sgnx_β:"(g has_sgnx -1) (at_left β)" "(g has_sgnx 1) (at_right β)"
    proof -
      have "(g has_real_derivative - r * sin β) (at β)"
        unfolding g_def by (auto intro!:derivative_eq_intros)
      moreover have "pi<β" "β<2*pi" unfolding β_def using 0<θ θ<pi by auto
      from sin_lt_zero[OF this] r>0 have "- r * sin β >0" by (simp add: mult_pos_neg)
      ultimately show "(g has_sgnx -1) (at_left β)" "(g has_sgnx 1) (at_right β)"
        using has_sgnx_derivative_at_left[of g "- r * sin β", OF _ g β=0] 
              has_sgnx_derivative_at_right[of g "- r * sin β", OF _ g β=0]
        by force+
    qed
    have f_tendsto: "(f  f i) (at_left i)" "(f  f i) (at_right i)" 
     and g_tendsto: "(g  g i) (at_left i)" "(g  g i) (at_right i)" for i
    proof -
      have "(f  f i) (at i)"
        unfolding f_def by (auto intro!:tendsto_eq_intros)
      then show "(f  f i) (at_left i)" "(f  f i) (at_right i)"
        by (auto simp add: filterlim_at_split)
    next
      have "(g  g i) (at i)"
        unfolding g_def by (auto intro!:tendsto_eq_intros)
      then show "(g  g i) (at_left i)" "(g  g i) (at_right i)"
        by (auto simp add: filterlim_at_split)
    qed
      
    define θ_if::real where "θ_if = (if r * sin θ + Im z > Im z0 then -1 else 1)" 
    define β_if::real where "β_if = (if r * sin β + Im z > Im z0 then 1 else -1)" 
    have "jump (λi. f i/g i) θ = θ_if" 
    proof -
      have ?thesis when "r * sin θ + Im z > Im z0"
      proof -
        have "f θ > 0" using that unfolding f_def by auto
        have "(LIM x (at_left θ). f x / g x :> at_top)" 
          apply (subst filterlim_divide_at_bot_at_top_iff[of f "f θ" _ g])
          using f θ > 0 g θ =0 f_tendsto g_tendsto[of θ] g_sgnx_θ by auto
        moreover then have "¬ (LIM x (at_left θ). f x / g x :> at_bot)" by auto 
        moreover have "(LIM x (at_right θ). f x / g x :> at_bot)"    
          apply (subst filterlim_divide_at_bot_at_top_iff[of f "f θ" _ g])
          using f θ > 0 g θ =0 f_tendsto g_tendsto[of θ] g_sgnx_θ by auto
        ultimately show ?thesis using that unfolding jump_def θ_if_def by auto
      qed
      moreover have ?thesis when "r * sin θ + Im z < Im z0"
      proof -
        have "f θ < 0" using that unfolding f_def by auto
        have "(LIM x (at_left θ). f x / g x :> at_bot)" 
          apply (subst filterlim_divide_at_bot_at_top_iff[of f "f θ" _ g])
          using f θ < 0 g θ =0 f_tendsto g_tendsto[of θ] g_sgnx_θ by auto
        moreover have "(LIM x (at_right θ). f x / g x :> at_top)"    
          apply (subst filterlim_divide_at_bot_at_top_iff[of f "f θ" _ g])
          using f θ < 0 g θ =0 f_tendsto g_tendsto[of θ] g_sgnx_θ by auto
        ultimately show ?thesis using that unfolding jump_def θ_if_def by auto
      qed  
      moreover have "r * sin θ + Im z  Im z0"
        using g_imp_f[OF g θ=0] unfolding f_def by auto
      ultimately show ?thesis by fastforce
    qed
    moreover have "jump (λi. f i/g i) β = β_if" 
    proof -
      have ?thesis when "r * sin β + Im z > Im z0"
      proof -
        have "f β > 0" using that unfolding f_def by auto
        have "(LIM x (at_left β). f x / g x :> at_bot)" 
          apply (subst filterlim_divide_at_bot_at_top_iff[of f "f β" _ g])
          using f β > 0 g β =0 f_tendsto g_tendsto[of β] g_sgnx_β by auto
        moreover have "(LIM x (at_right β). f x / g x :> at_top)"    
          apply (subst filterlim_divide_at_bot_at_top_iff[of f "f β" _ g])
          using f β > 0 g β =0 f_tendsto g_tendsto[of β] g_sgnx_β by auto
        ultimately show ?thesis using that unfolding jump_def β_if_def by auto
      qed
      moreover have ?thesis when "r * sin β + Im z < Im z0"
      proof -
        have "f β < 0" using that unfolding f_def by auto
        have "(LIM x (at_left β). f x / g x :> at_top)" 
          apply (subst filterlim_divide_at_bot_at_top_iff[of f "f β" _ g])
          using f β < 0 g β =0 f_tendsto g_tendsto[of β] g_sgnx_β by auto
        moreover have "(LIM x (at_right β). f x / g x :> at_bot)"    
          apply (subst filterlim_divide_at_bot_at_top_iff[of f "f β" _ g])
          using f β < 0 g β =0 f_tendsto g_tendsto[of β] g_sgnx_β by auto
        ultimately show ?thesis using that unfolding jump_def β_if_def by auto
      qed  
      moreover have "r * sin β + Im z  Im z0"
        using g_imp_f[OF g β=0] unfolding f_def by auto
      ultimately show ?thesis by fastforce
    qed
    moreover have "jump (λi. f i / g i) x  0  x=θ  x=β" when "st<x" "x<tt" for x 
    proof 
      assume "x = θ  x = β"
      then show "jump (λi. f i / g i) x  0"
        using jump (λi. f i/g i) θ = θ_if jump (λi. f i/g i) β = β_if
        unfolding θ_if_def β_if_def 
        by (metis add.inverse_inverse add.inverse_neutral of_int_0 one_neq_zero)
    next
      assume asm:"jump (λi. f i / g i) x  0"
      let ?thesis = "x = θ  x = β"
      have "g x=0"
      proof (rule ccontr)
        assume "g x  0"
        then have "isCont (λi. f i / g i) x"  
          unfolding f_def g_def by (auto intro:continuous_intros)
        then have "jump (λi. f i / g i) x = 0" using jump_not_infinity by simp
        then show False using asm by auto
      qed
      then have "cos x = zr" unfolding g_def zr_def using r>0 by (auto simp add:field_simps)
      have ?thesis when "xpi"
      proof-
        have "x0" using st<x st0 by auto
        then have "arccos (cos x) = x" using arccos_cos[of x] that by auto
        then have "x=θ" unfolding θ_def cos x=zr by auto
        then show ?thesis by auto
      qed
      moreover have ?thesis when "¬ xpi"
      proof -
        have "x-2*pi0" "-pix-2*pi" using that x<tt tt2*pi by auto
        from arccos_cos2[OF this] have "arccos (cos (x - 2 * pi)) = 2*pi-x" by auto
        then have "arccos (cos x) = 2*pi-x" 
          by (metis arccos cos_2pi_minus cos_ge_minus_one cos_le_one)
        then have "x=β" unfolding β_def θ_def using cos x =zr by auto
        then show ?thesis by auto
      qed
      ultimately show ?thesis by auto
    qed
    then have "{x. jump (λi. f i / g i) x  0  st < x  x < tt} = {θ,β}  {st<..<tt}"
      by force
    moreover have "θβ" using β_def θ < pi by auto
    ultimately have "cindex st tt h = 
          (if st<θ  θ<tt then θ_if else 0)
          +
          (if st<β  β < tt then β_if else 0)"
      unfolding cindex_def h_def by fastforce
    moreover have "cindexE st tt h = jumpF h (at_right st) + cindex st tt h - jumpF h (at_left tt)"
    proof (rule cindex_eq_cindexE_divide[of st tt f g,folded h_def])
      show "st < tt" using st < tt .
      show "x{st..tt}. g x = 0  f x  0" using g_imp_f by auto
      show "continuous_on {st..tt} f" "continuous_on {st..tt} g"
        unfolding f_def g_def by (auto intro!:continuous_intros)
    next
      let ?S1="{t. Re (part_circlepath z r st tt t-z0) = 0  0  t  t  1}"  
      let ?S2="{t. Im (part_circlepath z r st tt t-z0) = 0  0  t  t  1}"
      define G where "G={t.  g (linepath st tt t) = 0  0  t  t  1}"
      define F where "F={t.  f (linepath st tt t) = 0  0  t  t  1}"
      define vl where "vl=(λx. (x-st)/(tt-st))"
      have "finite G" "finite F"
      proof -
        have "finite {t. Re (part_circlepath z r st tt t-z0) = 0  0  t  t  1}" 
             "finite {t. Im (part_circlepath z r st tt t-z0) = 0  0  t  t  1}"
          using part_circlepath_half_finite_inter[of st tt r "Complex 1 0" z "Re z0"]
              part_circlepath_half_finite_inter[of st tt r "Complex 0 1" z "Im z0"] st<tt r>0 
          by (auto simp add:inner_complex_def Complex_eq_0)  
        moreover have 
            "Re (part_circlepath z r st tt t-z0) = 0  g (linepath st tt t) = 0"
            "Im (part_circlepath z r st tt t-z0) = 0  f (linepath st tt t) = 0"
            for t
          unfolding cindex_pathE_def part_circlepath_def exp_Euler f_def g_def comp_def
          by (auto simp add:cos_of_real sin_of_real algebra_simps)
        ultimately show "finite G" "finite F" unfolding G_def F_def
          by auto
      qed
      then have "finite (linepath st tt ` F)" "finite (linepath st tt ` G)"
        by auto
      moreover have 
          "{x. f x = 0  st  x  x  tt}  linepath st tt ` F"
          "{x. g x = 0  st  x  x  tt}  linepath st tt ` G"
      proof -
        have *: "linepath st tt (vl t) = t" "vl t0  tst" "vl t1 ttt" for t 
          unfolding linepath_def vl_def using tt>st
            apply (auto simp add:divide_simps)  
          by (simp add:algebra_simps)   
        then show 
            "{x. f x = 0  st  x  x  tt}  linepath st tt `F"
            "{x. g x = 0  st  x  x  tt}  linepath st tt `G"
          unfolding F_def G_def 
          by (clarify|rule_tac x="vl x" in rev_image_eqI,auto)+
      qed
      ultimately have 
          "finite {x. f x = 0  st  x  x  tt}" 
          "finite {x. g x = 0  st  x  x  tt}"
        by (auto elim:rev_finite_subset)
      from finite_UnI[OF this] show "finite {x. (f x = 0  g x = 0)  st  x  x  tt}" 
        by (elim rev_finite_subset,auto)
    qed
    ultimately show ?thesis
      unfolding Let_def
      apply (fold zr_def θ_def β_def θ_if_def β_if_def)+
      using jstart_eq jfinish_eq index_eq that by auto
  qed
  ultimately show ?thesis by fastforce  
qed 

lemma jumpF_pathstart_part_circlepath: 
  assumes "st<tt" "r>0" "cmod (z-z0) r"
  shows "jumpF_pathstart (part_circlepath z r st tt) z0 = (
            if r * cos st + Re z - Re z0 = 0 then 
              (let 
                Δ = r* sin st + Im z - Im z0
              in
                if (sin st > 0  cos st=1 )  Δ < 0 
                     (sin st < 0   cos st=-1 )  Δ > 0  then 
                  1/2
                else 
                  - 1/2)
            else 0)"  
proof -
  define f where "f=(λi. r * sin i + Im z - Im z0)"
  define g where "g=(λi. r * cos i + Re z - Re z0)"
  have jumpF_eq:"jumpF_pathstart (part_circlepath z r st tt) z0 = jumpF (λi. f i/g i) (at_right st)"
  proof -
    have "jumpF_pathstart (part_circlepath z r st tt) z0 
        = jumpF ((λi. f i/g i) o linepath st tt) (at_right 0)" 
      unfolding jumpF_pathstart_def part_circlepath_def exp_Euler f_def g_def comp_def
      by (simp add:cos_of_real sin_of_real algebra_simps)
    also have "... = jumpF (λi. f i/g i) (at_right st)"
      using jumpF_linear_comp(2)[of "tt-st" "(λi. f i/g i)" st 0,symmetric] st<tt
      unfolding linepath_def by (auto simp add:algebra_simps)
    finally show ?thesis .
  qed
  have g_has_sgnx1:"(g has_sgnx 1) (at_right st)" when "g st=0" "sin st < 0  cos st=-1"  
  proof -
    have ?thesis when "sin st<0" 
    proof -
      have "(g has_sgnx sgn (- r * sin st)) (at_right st)"
        apply (rule has_sgnx_derivative_at_right[of g "- r * sin st" st])
        subgoal unfolding g_def by (auto intro!:derivative_eq_intros)
        subgoal using g st=0 .
        subgoal using r>0 sin st<0 by (simp add: mult_pos_neg)
        done
      then show ?thesis using r>0 that by (simp add: sgn_mult)
    qed
    moreover have ?thesis when "cos st = -1"
    proof -
      have "g i > 0" when "st<i" "i<st+pi" for i
      proof -
        obtain k where k_def:"st = 2 * of_int k * pi+ pi" 
          using cos st = -1 by (metis cos_eq_minus1 distrib_left mult.commute mult.right_neutral)
        have "cos (i-st) < 1" using cos_monotone_0_pi[of 0 "i-st" ] that by auto
        moreover have "cos (i-st) = - cos i" 
          apply (rule cos_eq_neg_periodic_intro[of _ _ "-k-1"])
          unfolding k_def by (auto simp add:algebra_simps)
        ultimately have "cos i>-1" by auto
        then have "cos st<cos i" using cos st=-1 by auto
        have "0 = r * cos st + Re z - Re z0"
          using g st = 0 unfolding g_def by auto
        also have "... < r * cos i + Re z - Re z0"
          using cos st < cos i r>0 by auto
        finally show ?thesis unfolding g_def by auto
      qed
      then show ?thesis
        unfolding has_sgnx_def eventually_at_right 
        apply (intro exI[where x="st+pi"])
        by auto
    qed
    ultimately show ?thesis using that(2) by auto
  qed
  have g_has_sgnx2:"(g has_sgnx -1) (at_right st)" when "g st=0" "sin st > 0  cos st=1" 
  proof -
    have ?thesis when "sin st>0"
    proof -
      have "(g has_sgnx sgn (- r * sin st)) (at_right st)"
        apply (rule has_sgnx_derivative_at_right[of _ "- r * sin st"])
        subgoal unfolding g_def by (auto intro!:derivative_eq_intros)
        subgoal using g st=0 .
        subgoal using r>0 sin st>0 by (simp add: mult_pos_neg)
        done
      then show ?thesis using r>0 that by (simp add: sgn_mult)
    qed    
    moreover have ?thesis when "cos st=1"
    proof -
      have "g i < 0" when "st<i" "i<st+pi" for i
      proof -
        obtain k where k_def:"st = 2 * of_int k * pi" 
          using cos st=1 cos_one_2pi_int by auto
        have "cos (i-st) < 1" using cos_monotone_0_pi[of 0 "i-st" ] that by auto
        moreover have "cos (i-st) = cos i" 
          apply (rule cos_eq_periodic_intro[of _ _ "-k"])
          unfolding k_def by (auto simp add:algebra_simps)
        ultimately have "cos i<1" by auto
        then have "cos st>cos i" using cos st=1 by auto
        have "0 = r * cos st + Re z - Re z0"
          using g st = 0 unfolding g_def by auto
        also have "... > r * cos i + Re z - Re z0"
          using cos st > cos i r>0 by auto
        finally show ?thesis unfolding g_def by auto
      qed
      then show ?thesis
        unfolding has_sgnx_def eventually_at_right
        apply (intro exI[where x="st+pi"])
        by auto
    qed
    ultimately show ?thesis using that(2) by auto
  qed
    
  have ?thesis when "r * cos st + Re z - Re z0  0"
  proof -
    have "g st 0" using that unfolding g_def by auto
    then have "continuous (at_right st) (λi. f i / g i)"
      unfolding f_def g_def by (auto intro!:continuous_intros)
    then have "jumpF (λi. f i/g i) (at_right st) = 0"
      using jumpF_not_infinity[of "at_right st" "(λi. f i/g i)"] by auto
    then show ?thesis using jumpF_eq that by auto
  qed
  moreover have ?thesis when "r * cos st + Re z - Re z0 = 0" 
    "(sin st > 0  (cos st=1) )  f st < 0 
                     (sin st < 0   (cos st=-1) )  f st > 0"
  proof -
    have "g st = 0" "f st0" and g_cont: "continuous (at_right st) g" and f_cont:"continuous (at_right st) f" 
      using that unfolding g_def f_def by (auto intro!:continuous_intros)
    have "(g has_sgnx sgn (f st)) (at_right st)"
      using g_has_sgnx1[OF g st=0] g_has_sgnx2[OF g st=0] that(2) by auto
    then have "LIM x at_right st. f x / g x :> at_top"
      apply (subst filterlim_divide_at_bot_at_top_iff[of f "f st" "at_right st" g])
      using f st0 g st = 0 g_cont f_cont by (auto simp add: continuous_within)
    then have "jumpF (λi. f i/g i) (at_right st) = 1/2"
      unfolding jumpF_def by auto
    then show ?thesis using jumpF_eq that unfolding f_def by auto
  qed
  moreover have ?thesis when "r * cos st + Re z - Re z0 = 0" 
    "¬ ((sin st > 0  cos st=1 )  f st < 0 
                     (sin st < 0   cos st=-1 )  f st > 0)"
  proof -
    define neq1 where "neq1 = (k::int. st  2*k*pi)"
    define neq2 where "neq2 = (k::int. st  2*k*pi+pi)"
    have "g st = 0" and g_cont: "continuous (at_right st) g" and f_cont:"continuous (at_right st) f" 
      using that unfolding g_def f_def by (auto intro!:continuous_intros)
    have "f st0"
    proof (rule ccontr)
      assume "¬ f st  0"
      then have "f st = 0" by auto
      then have "Im (z0 - z) =r * sin st " "Re (z0 - z) = r * cos st" using g st=0
        unfolding f_def g_def by (auto simp add:algebra_simps)
      then have "cmod (z0 - z) = sqrt((r * sin st)^2 + (r * cos st)^2)" 
        unfolding cmod_def by auto
      also have "... = sqrt (r^2 * ((sin st)^2 + (cos st)^2))"
        by (auto simp only:algebra_simps power_mult_distrib)
      also have "... = r"
        using r>0 by simp
      finally have "cmod (z0 - z) = r" .
      then show False using cmod (z-z0) r by (simp add: norm_minus_commute)
    qed
    have "(sin st > 0  (cos st=1) )  f st > 0  (sin st < 0   (cos st=-1) )  f st < 0"  
    proof -
      have "sin st = 0  cos st=-1  cos st=1"  
        by (metis (no_types, opaque_lifting) add.right_neutral cancel_comm_monoid_add_class.diff_cancel 
            cos_diff cos_zero mult_eq_0_iff power2_eq_1_iff power2_eq_square sin_squared_eq)
      moreover have "((sin st  0  cos st 1 )  f st > 0)  ((sin st  0   cos st-1)  f st < 0)"
        using that(2) f st0 by argo  
      ultimately show ?thesis by (meson linorder_neqE_linordered_idom not_le)   
    qed   
    then have "(g has_sgnx - sgn (f st)) (at_right st)"  
      using g_has_sgnx1[OF g st=0] g_has_sgnx2[OF g st=0] by auto
    then have "LIM x at_right st. f x / g x :> at_bot"
      apply (subst filterlim_divide_at_bot_at_top_iff[of f "f st" "at_right st" g])
      using f st0 g st = 0 g_cont f_cont by (auto simp add: continuous_within)
    then have "jumpF (λi. f i/g i) (at_right st) = -1/2"
      unfolding jumpF_def by auto
    then show ?thesis using jumpF_eq that unfolding f_def by auto
  qed    
  ultimately show ?thesis by fast
qed  
  
lemma jumpF_pathfinish_part_circlepath: 
  assumes "st<tt" "r>0" "cmod (z-z0) r"
  shows "jumpF_pathfinish (part_circlepath z r st tt) z0 = (
            if r * cos tt + Re z - Re z0 = 0 then 
              (let 
                Δ = r* sin tt + Im z - Im z0
              in
                if (sin tt > 0  cos tt=-1 )  Δ < 0 
                     (sin tt < 0   cos tt=1 )  Δ > 0  then 
                  - 1/2
                else 
                  1/2)
            else 0)"  
proof -
  define f where "f=(λi. r * sin i + Im z - Im z0)"
  define g where "g=(λi. r * cos i + Re z - Re z0)"
  have jumpF_eq:"jumpF_pathfinish (part_circlepath z r st tt) z0 = jumpF (λi. f i/g i) (at_left tt)"
  proof -
    have "jumpF_pathfinish (part_circlepath z r st tt) z0 
        = jumpF ((λi. f i/g i) o linepath st tt) (at_left 1)" 
      unfolding jumpF_pathfinish_def part_circlepath_def exp_Euler f_def g_def comp_def
      by (simp add:cos_of_real sin_of_real algebra_simps)
    also have "... = jumpF (λi. f i/g i) (at_left tt)"
      using jumpF_linear_comp(1)[of "tt-st" "(λi. f i/g i)" st 1,symmetric]  st<tt
      unfolding linepath_def by (auto simp add:algebra_simps)
    finally show ?thesis .
  qed
  have g_has_sgnx1:"(g has_sgnx -1) (at_left tt)" when "g tt=0" "sin tt < 0  cos tt=1"  
  proof -
    have ?thesis when "sin tt<0"
    proof -
      have "(g has_sgnx - sgn (- r * sin tt)) (at_left tt)"
        apply (rule has_sgnx_derivative_at_left[of _ "- r * sin tt"])
        subgoal unfolding g_def by (auto intro!:derivative_eq_intros)
        subgoal using g tt=0 .
        subgoal using r>0 sin tt<0 by (simp add: mult_pos_neg)
        done
      then show ?thesis using r>0 that by (simp add: sgn_mult)
    qed
    moreover have ?thesis when "cos tt=1"
    proof -
      have "g i < 0" when "tt-pi<i" "i<tt" for i
      proof -
        obtain k where k_def:"tt = 2 * of_int k * pi" 
          using cos tt=1 cos_one_2pi_int by auto
        have "cos (i-tt) < 1" 
          using cos_monotone_0_pi[of 0 "tt-i" ] that cos_minus[of "tt-i",simplified] by auto
        moreover have "cos (i-tt) = cos i" 
          apply (rule cos_eq_periodic_intro[of _ _ "-k"])
          unfolding k_def by (auto simp add:algebra_simps)
        ultimately have "cos i<1" by auto
        then have "cos tt>cos i" using cos tt=1 by auto
        have "0 = r * cos tt + Re z - Re z0"
          using g tt = 0 unfolding g_def by auto
        also have "... > r * cos i + Re z - Re z0"
          using cos tt > cos i r>0 by auto
        finally show ?thesis unfolding g_def by auto
      qed
      then show ?thesis
        unfolding has_sgnx_def eventually_at_left
        apply (intro exI[where x="tt-pi"])
        by auto
    qed
    ultimately show ?thesis using that(2) by auto
  qed
  have g_has_sgnx2:"(g has_sgnx 1) (at_left tt)" when "g tt=0" "sin tt > 0  cos tt=-1" 
  proof -
    have ?thesis when "sin tt>0"
    proof -
      have "(g has_sgnx - sgn (- r * sin tt)) (at_left tt)"
        apply (rule has_sgnx_derivative_at_left[of _ "- r * sin tt"])
        subgoal unfolding g_def by (auto intro!:derivative_eq_intros)
        subgoal using g tt=0 .
        subgoal using r>0 sin tt>0 by (simp add: mult_pos_neg)
        done
      then show ?thesis using r>0 that by (simp add: sgn_mult)
    qed
    moreover have ?thesis when "cos tt = -1"
    proof -
      have "g i > 0" when "tt-pi<i" "i<tt" for i
      proof -
        obtain k where k_def:"tt = 2 * of_int k * pi+ pi" 
          using cos tt = -1 by (metis cos_eq_minus1 distrib_left mult.commute mult.right_neutral)
        have "cos (i-tt) < 1" 
            using cos_monotone_0_pi[of 0 "tt-i" ] that cos_minus[of "tt-i",simplified]
            by auto
        moreover have "cos (i-tt) = - cos i" 
          apply (rule cos_eq_neg_periodic_intro[of _ _ "-k-1"])
          unfolding k_def by (auto simp add:algebra_simps)
        ultimately have "cos i>-1" by auto
        then have "cos tt<cos i" using cos tt=-1 by auto
        have "0 = r * cos tt + Re z - Re z0"
          using g tt = 0 unfolding g_def by auto
        also have "... < r * cos i + Re z - Re z0"
          using cos tt < cos i r>0 by auto
        finally show ?thesis unfolding g_def by auto
      qed
      then show ?thesis
        unfolding has_sgnx_def eventually_at_left 
        apply (intro exI[where x="tt-pi"])
        by auto
    qed
    ultimately show ?thesis using that(2) by auto
  qed
    
  have ?thesis when "r * cos tt + Re z - Re z0  0"
  proof -
    have "g tt 0" using that unfolding g_def by auto
    then have "continuous (at_left tt) (λi. f i / g i)"
      unfolding f_def g_def by (auto intro!:continuous_intros)
    then have "jumpF (λi. f i/g i) (at_left tt) = 0"
      using jumpF_not_infinity[of "at_left tt" "(λi. f i/g i)"] by auto
    then show ?thesis using jumpF_eq that by auto
  qed
  moreover have ?thesis when "r * cos tt + Re z - Re z0 = 0" 
    "(sin tt > 0  cos tt=-1 )  f tt < 0 
                     (sin tt < 0  cos tt=1 )  f tt > 0"
  proof -
    have "g tt = 0" "f tt0" and g_cont: "continuous (at_left tt) g" and f_cont:"continuous (at_left tt) f" 
      using that unfolding g_def f_def by (auto intro!:continuous_intros)
    have "(g has_sgnx - sgn (f tt)) (at_left tt)"
      using g_has_sgnx1[OF g tt=0] g_has_sgnx2[OF g tt=0] that(2) by auto
    then have "LIM x at_left tt. f x / g x :> at_bot"
      apply (subst filterlim_divide_at_bot_at_top_iff[of f "f tt" "at_left tt" g])
      using f tt0 g tt = 0 g_cont f_cont by (auto simp add: continuous_within)
    then have "jumpF (λi. f i/g i) (at_left tt) = - 1/2"
      unfolding jumpF_def by auto
    then show ?thesis using jumpF_eq that unfolding f_def by auto
  qed
  moreover have ?thesis when "r * cos tt + Re z - Re z0 = 0" 
    "¬ ((sin tt > 0  cos tt=-1 )  f tt < 0 
                     (sin tt < 0   cos tt=1 )  f tt > 0)"
  proof -
    have "g tt = 0" and g_cont: "continuous (at_left tt) g" and f_cont:"continuous (at_left tt) f" 
      using that unfolding g_def f_def by (auto intro!:continuous_intros)
    have "f tt0"
    proof (rule ccontr)
      assume "¬ f tt  0"
      then have "f tt = 0" by auto
      then have "Im (z0 - z) =r * sin tt " "Re (z0 - z) = r * cos tt" using g tt=0
        unfolding f_def g_def by (auto simp add:algebra_simps)
      then have "cmod (z0 - z) = sqrt((r * sin tt)^2 + (r * cos tt)^2)" 
        unfolding cmod_def by auto
      also have "... = sqrt (r^2 * ((sin tt)^2 + (cos tt)^2))"
        by (auto simp only:algebra_simps power_mult_distrib)
      also have "... = r"
        using r>0 by simp
      finally have "cmod (z0 - z) = r" .
      then show False using cmod (z-z0) r by (simp add: norm_minus_commute)
    qed
    have "(sin tt > 0  cos tt=-1 )  f tt > 0  (sin tt < 0   cos tt=1 )  f tt < 0"  
    proof -
      have "sin tt = 0  cos tt=-1  cos tt=1"  
        by (metis (no_types, opaque_lifting) add.right_neutral cancel_comm_monoid_add_class.diff_cancel 
            cos_diff cos_zero mult_eq_0_iff power2_eq_1_iff power2_eq_square sin_squared_eq)
      moreover have "((sin tt  0  cos tt -1 )  f tt > 0)  ((sin tt  0   cos tt1)  f tt < 0)"
        using that(2) f tt0 by argo  
      ultimately show ?thesis by (meson linorder_neqE_linordered_idom not_le)   
    qed   
    then have "(g has_sgnx sgn (f tt)) (at_left tt)"  
      using g_has_sgnx1[OF g tt=0] g_has_sgnx2[OF g tt=0] by auto
    then have "LIM x at_left tt. f x / g x :> at_top"
      apply (subst filterlim_divide_at_bot_at_top_iff[of f "f tt" "at_left tt" g])
      using f tt0 g tt = 0 g_cont f_cont by (auto simp add: continuous_within)
    then have "jumpF (λi. f i/g i) (at_left tt) = 1/2"
      unfolding jumpF_def by auto
    then show ?thesis using jumpF_eq that unfolding f_def by auto
  qed    
  ultimately show ?thesis by fast
qed

lemma 
  fixes z0 z::complex and r::real
  defines "upper  cindex_pathE (part_circlepath z r 0 pi) z0"
      and "lower  cindex_pathE (part_circlepath z r pi (2*pi)) z0"
  shows cindex_pathE_circlepath_upper:
      "cmod (z0-z) < r   upper = -1" 
      "Im (z0-z) > r; ¦Re (z0 - z)¦ < r  upper = 1"
      "Im (z0-z) < -r; ¦Re (z0 - z)¦ < r  upper = -1" 
      "¦Re (z0 - z)¦ > r; r>0  upper = 0"
  and cindex_pathE_circlepath_lower: 
      "cmod (z0-z) < r  lower = -1" 
      "Im (z0-z) > r; ¦Re (z0 - z)¦ < r  lower = -1"
      "Im (z0-z) < -r; ¦Re (z0 - z)¦ < r  lower = 1"
      "¦Re (z0 - z)¦ > r; r>0  lower = 0"
proof -
  assume assms:"cmod (z0-z) < r"
  have zz_facts:"-r<Re z - Re z0" "Re z - Re z0<r" "r>0"
    subgoal using assms complex_Re_le_cmod le_less_trans by fastforce
    subgoal by (metis assms complex_Re_le_cmod le_less_trans minus_complex.simps(1) norm_minus_commute)
    subgoal using assms le_less_trans norm_ge_zero by blast
    done
  define θ where "θ = arccos ((Re z0 - Re z) / r)"    
  have θ_bound:"0 < θ  θ < pi" 
    unfolding θ_def
    apply (rule arccos_lt_bounded)
    using zz_facts by (auto simp add:field_simps)
  have Im_sin:"abs (Im z0 - Im z) < r * sin θ"
  proof -
    define zz where "zz=z0-z"
    have "sqrt ((Re zz)2 + (Im zz)2) < r"
      using assms unfolding zz_def cmod_def .
    then have "(Re zz)2 + (Im zz)2 < r^2"
      by (metis cmod_power2 dvd_refl linorder_not_le norm_complex_def power2_le_imp_le
            real_sqrt_power zero_le_power_eq_numeral)
    then have "(Im zz)2 < r^2 - (Re zz)^2" by auto
    then have "abs (Im zz) < sqrt (r^2 - (Re zz)^2)"
      by (simp add: real_less_rsqrt)
    then show ?thesis
      unfolding θ_def zz_def
      apply (subst sin_arccos_abs)
      subgoal using zz_facts by auto
      subgoal using r>0 by (auto simp add:field_simps divide_simps real_sqrt_divide)
      done
  qed
  show "upper = - 1"
  proof -
    have "jumpF_pathstart (part_circlepath z r 0 pi) z0 = 0"
      apply (subst jumpF_pathstart_part_circlepath)
      using zz_facts assms by (auto simp add: norm_minus_commute)
    moreover have "jumpF_pathfinish (part_circlepath z r 0 pi) z0 = 0"
      apply (subst jumpF_pathfinish_part_circlepath)
      using zz_facts assms by (auto simp add: norm_minus_commute)
    ultimately show ?thesis using assms zz_facts θ_bound Im_sin unfolding upper_def
      apply (subst cindex_pathE_part_circlepath)
      by (fold θ_def,auto simp add: norm_minus_commute)
  qed
  show "lower = - 1"
  proof -    
    have "jumpF_pathstart (part_circlepath z r pi (2*pi)) z0 = 0"
      apply (subst jumpF_pathstart_part_circlepath)
      using zz_facts assms by (auto simp add: norm_minus_commute)
    moreover have "jumpF_pathfinish (part_circlepath z r pi (2*pi)) z0 = 0"
      apply (subst jumpF_pathfinish_part_circlepath)
      using zz_facts assms by (auto simp add: norm_minus_commute)
    ultimately show ?thesis using assms zz_facts θ_bound Im_sin unfolding lower_def
      apply (subst cindex_pathE_part_circlepath)
      by (fold θ_def,auto simp add: norm_minus_commute)
  qed 
next
  assume assms:"¦Re (z0 - z)¦ > r" "r>0"
  show "upper = 0" using assms unfolding upper_def 
    apply (subst cindex_pathE_part_circlepath)
    apply auto
    by (metis abs_Re_le_cmod abs_minus_commute eucl_less_le_not_le minus_complex.simps(1))
  show "lower = 0"
    using assms unfolding lower_def 
    apply (subst cindex_pathE_part_circlepath)
    apply auto
    by (metis abs_Re_le_cmod abs_minus_commute eucl_less_le_not_le minus_complex.simps(1))
next
  assume assms:"¦Re (z0 - z)¦ < r"
  then have "r>0" by auto

  define θ where "θ = arccos ((Re z0 - Re z) / r)"   
  have θ_bound:"0 < θ  θ < pi" 
    unfolding θ_def
    apply (rule arccos_lt_bounded)
    using assms by (auto simp add:field_simps)
  note norm_minus_commute[simp]
  have jumpFs:
      "jumpF_pathstart (part_circlepath z r 0 pi) z0 = 0"
      "jumpF_pathfinish (part_circlepath z r 0 pi) z0 = 0"
      "jumpF_pathstart (part_circlepath z r pi (2*pi)) z0 = 0"
      "jumpF_pathfinish (part_circlepath z r pi (2*pi)) z0 = 0"
      when "cmod (z0 - z)  r"
    subgoal by (subst jumpF_pathstart_part_circlepath,use assms that in auto)
    subgoal by (subst jumpF_pathfinish_part_circlepath,use assms that in auto)
    subgoal by (subst jumpF_pathstart_part_circlepath,use assms that in auto)
    subgoal by (subst jumpF_pathfinish_part_circlepath,use assms that in auto)
    done
  show "upper = 1" "lower = -1" when "Im (z0-z) > r"
  proof -
    have "cmod (z0 - z)  r" 
      using that assms abs_Im_le_cmod abs_le_D1 not_le by blast
    moreover have "Im z0 - Im z > r * sin θ" 
    proof -
      have "r * sin θ  r" 
        using r>0 by auto
      also have "... < Im z0 - Im z" using that by auto
      finally show ?thesis .
    qed
    ultimately show "upper = 1"  using assms jumpFs θ_bound that unfolding upper_def
      apply (subst cindex_pathE_part_circlepath)
      by (fold θ_def,auto)
    have "Im z - Im z0 < r * sin θ" 
    proof -
      have "Im z - Im z0  <0" using that r>0 by auto
      moreover have "r * sin θ>0" using r>0 θ_bound by (simp add: sin_gt_zero)
      ultimately show ?thesis by auto
    qed
    then show "lower = -1" using cmod (z0 - z)  r Im z0 - Im z > r * sin θ 
        assms jumpFs θ_bound that unfolding lower_def
      apply (subst cindex_pathE_part_circlepath)
      by (fold θ_def,auto)
  qed
  show "upper = - 1" "lower = 1" when "Im (z0-z) < -r"
  proof -
    have "cmod (z0 - z)  r" 
      using that assms 
      by (metis abs_Im_le_cmod abs_le_D1 minus_complex.simps(2) minus_diff_eq neg_less_iff_less 
          norm_minus_cancel not_le)
    moreover have "Im z - Im z0 > r * sin θ" 
    proof -
      have "r * sin θ  r" 
        using r>0 by auto
      also have "... < Im z - Im z0" using that by auto
      finally show ?thesis .
    qed
    moreover have "Im z0 - Im z < r * sin θ"
    proof -
      have "Im z0 - Im z<0" using that r>0 by auto
      moreover have "r * sin θ>0" using r>0 θ_bound by (simp add: sin_gt_zero)
      ultimately show ?thesis by auto
    qed
    ultimately show "upper = - 1" using assms jumpFs θ_bound that unfolding upper_def
      apply (subst cindex_pathE_part_circlepath)
      by (fold θ_def,auto)
    show "lower = 1"
      using Im z0 - Im z < r * sin θ Im z - Im z0 > r * sin θ cmod (z0 - z)  r
        assms jumpFs θ_bound that unfolding lower_def
      apply (subst cindex_pathE_part_circlepath)
      by (fold θ_def,auto)
  qed
qed
  
lemma jumpF_pathstart_linepath:
  "jumpF_pathstart (linepath a b) z = 
    (if Re a = Re z  Im aIm z  Re b  Re a then 
        if (Im a>Im z  Re b > Re a)  (Im a<Im z  Re b < Re a) then 1/2 else -1/2 
     else 0)"
proof -
  define f where "f=(λt. (Im b - Im a )* t + (Im a - Im z))"
  define g where "g=(λt. (Re b - Re a )* t + (Re a - Re z))"
  have jump_eq:"jumpF_pathstart (linepath a b) z = jumpF (λt. f t/g t) (at_right 0)"
    unfolding jumpF_pathstart_def f_def linepath_def g_def 
    by (auto simp add:algebra_simps)
  have ?thesis when "Re aRe z"
  proof -
    have "jumpF_pathstart (linepath a b) z = 0"
      unfolding jumpF_pathstart_def
      apply (rule jumpF_im_divide_Re_0)
         apply auto
      by (auto simp add:linepath_def that)
    then show ?thesis using that by auto
  qed
  moreover have ?thesis when "Re a=Re z" "Im a = Im z" 
  proof -
    define c where "c=(Im b - Im a) / (Re b - Re a)"
    have "jumpF (λt. f t/g t) (at_right 0) = jumpF (λ_. c) (at_right 0)"
    proof (rule jumpF_cong)
      show "F x in at_right 0. f x / g x = c"
        unfolding eventually_at_right f_def g_def c_def using that
        apply (intro exI[where x=1])
        by auto
    qed simp
    then show ?thesis using jump_eq that by auto 
  qed
  moreover have ?thesis when "Re a=Re z" "Re b = Re a" 
  proof -
    have "(λt. f t/g t) = (λ_. 0)" unfolding f_def g_def using that by auto
    then have "jumpF (λt. f t/g t) (at_right 0) = jumpF (λ_. 0) (at_right 0)" by auto
    then show ?thesis using jump_eq that by auto
  qed
  moreover have ?thesis when "Re a = Re z" "(Im a>Im z  Re b > Re a)  (Im a<Im z  Re b < Re a)"
  proof -
    have "LIM x at_right 0. f x / g x :> at_top"
      apply (subst filterlim_divide_at_bot_at_top_iff[of _ "Im a - Im z"])
      unfolding f_def g_def using that
      by (auto intro!:tendsto_eq_intros sgnx_eq_intros)  
    then have "jumpF (λt. f t/g t) (at_right 0) = 1/2"
      unfolding jumpF_def by simp
    then show ?thesis using jump_eq that by auto
  qed
  moreover have ?thesis when "Re a = Re z" "Im aIm z" "Re b  Re a" 
      "¬ ((Im a>Im z  Re b > Re a)  (Im a<Im z  Re b < Re a))"
  proof -
    have "(Im a>Im z  Re b < Re a)  (Im a<Im z  Re b > Re a)"
      using that by argo
    then have "LIM x at_right 0. f x / g x :> at_bot"
      apply (subst filterlim_divide_at_bot_at_top_iff[of _ "Im a - Im z"])
      unfolding f_def g_def using that
      by (auto intro!:tendsto_eq_intros sgnx_eq_intros) 
    moreover then have "¬ (LIM x at_right 0. f x / g x :> at_top)"
      using filterlim_at_top_at_bot by fastforce
    ultimately have "jumpF (λt. f t/g t) (at_right 0) = - 1/2"
      unfolding jumpF_def by simp
    then show ?thesis using jump_eq that by auto
  qed  
  ultimately show ?thesis by fast
qed
  
lemma jumpF_pathfinish_linepath:
  "jumpF_pathfinish (linepath a b) z = 
    (if Re b = Re z  Im b Im z  Re b  Re a then 
        if (Im b>Im z  Re a > Re b)  (Im b<Im z  Re a < Re b) then 1/2 else -1/2 
     else 0)"
proof -
  define f where "f=(λt. (Im b - Im a )* t + (Im a - Im z))"
  define g where "g=(λt. (Re b - Re a )* t + (Re a - Re z))"
  have jump_eq:"jumpF_pathfinish (linepath a b) z = jumpF (λt. f t/g t) (at_left 1)"
    unfolding jumpF_pathfinish_def f_def linepath_def g_def 
    by (auto simp add:algebra_simps)
  have ?thesis when "Re bRe z"
  proof -
    have "jumpF_pathfinish (linepath a b) z = 0"
      unfolding jumpF_pathfinish_def
      apply (rule jumpF_im_divide_Re_0)
         apply auto
      by (auto simp add:linepath_def that)
    then show ?thesis using that by auto
  qed
  moreover have ?thesis when "Re z=Re b" "Im z = Im b" 
  proof -
    define c where "c=(Im a - Im b) / (Re a - Re b)"
    have "jumpF (λt. f t/g t) (at_left 1) = jumpF (λ_. c) (at_left 1)"
    proof (rule jumpF_cong)
      have "f x / g x = c" when "x<1" for x
      proof -
        have "f x / g x = ((Im a - Im b)*(1-x))/((Re a - Re b)*(1-x))"
          unfolding f_def g_def 
          by (auto simp add:algebra_simps Re z=Re b Im z = Im b)
        also have "... = c"
          using that unfolding c_def by auto
        finally show ?thesis .
      qed
      then show "F x in at_left 1. f x / g x = c"
        unfolding eventually_at_left using that
        apply (intro exI[where x=0])
        by auto
    qed simp
    then show ?thesis using jump_eq that by auto 
  qed
  moreover have ?thesis when "Re a=Re z" "Re b = Re a" 
  proof -
    have "(λt. f t/g t) = (λ_. 0)" unfolding f_def g_def using that by auto
    then have "jumpF (λt. f t/g t) (at_left 1) = jumpF (λ_. 0) (at_left 1)" by auto
    then show ?thesis using jump_eq that by auto
  qed
  moreover have ?thesis when "Re b = Re z" "(Im b>Im z  Re a > Re b)  (Im b<Im z  Re a < Re b)"
  proof -
    have "LIM x at_left 1. f x / g x :> at_top"
    proof -
      have "(g has_real_derivative Re b - Re a) (at 1)"
        unfolding g_def by (auto intro!:derivative_eq_intros) 
      from has_sgnx_derivative_at_left[OF this] 
      have "(g has_sgnx sgn (Im b - Im z)) (at_left 1)"
        using that unfolding g_def by auto
      then show ?thesis 
        apply (subst filterlim_divide_at_bot_at_top_iff[of _ "Im b - Im z"])
        unfolding f_def g_def using that by (auto intro!:tendsto_eq_intros)
    qed
    then have "jumpF (λt. f t/g t) (at_left 1) = 1/2"
      unfolding jumpF_def by simp
    then show ?thesis using jump_eq that by auto
  qed
  moreover have ?thesis when "Re b = Re z" "Im bIm z" "Re b  Re a" 
      "¬ ((Im b>Im z  Re a > Re b)  (Im b<Im z  Re a < Re b))"
  proof -
    have "(Im b>Im z  Re a < Re b)  (Im b<Im z  Re a > Re b)"
      using that by argo
    have "LIM x at_left 1. f x / g x :> at_bot"
    proof -
      have "(g has_real_derivative Re b - Re a) (at 1)"
        unfolding g_def by (auto intro!:derivative_eq_intros) 
      from has_sgnx_derivative_at_left[OF this]
      have "(g has_sgnx - sgn (Im b - Im z)) (at_left 1)" 
        using that unfolding g_def by auto
      then show ?thesis
        apply (subst filterlim_divide_at_bot_at_top_iff[of _ "Im b - Im z"])
        unfolding f_def g_def using that by (auto intro!:tendsto_eq_intros ) 
    qed
    moreover then have "¬ (LIM x at_left 1. f x / g x :> at_top)"
      using filterlim_at_top_at_bot by fastforce
    ultimately have "jumpF (λt. f t/g t) (at_left 1) = - 1/2"
      unfolding jumpF_def by simp
    then show ?thesis using jump_eq that by auto
  qed  
  ultimately show ?thesis by argo
qed    
    
subsection ‹Setting up the method for evaluating winding numbers›  
  
lemma pathfinish_pathstart_partcirclepath_simps:
  "pathstart (part_circlepath z0 r (3*pi/2) tt) = z0 - Complex 0 r"
  "pathstart (part_circlepath z0 r (2*pi) tt) = z0 + r"
  "pathfinish (part_circlepath z0 r st (3*pi/2)) = z0 - Complex 0 r"
  "pathfinish (part_circlepath z0 r st (2*pi)) = z0 + r"
  "pathstart (part_circlepath z0 r 0 tt) = z0 + r"
  "pathstart (part_circlepath z0 r (pi/2) tt) = z0 + Complex 0 r"
  "pathstart (part_circlepath z0 r (pi) tt) = z0 - r"
  "pathfinish (part_circlepath z0 r st 0) = z0+r"
  "pathfinish (part_circlepath z0 r st (pi/2)) = z0 + Complex 0 r"
  "pathfinish (part_circlepath z0 r st (pi)) = z0 - r"
  unfolding part_circlepath_def linepath_def pathstart_def pathfinish_def exp_Euler
  subgoal 
    apply(simp, subst sin.minus_1[symmetric],subst cos.minus_1[symmetric])
    by (simp add: complex_of_real_i)
  subgoal 
    by (simp add: complex_of_real_i)
  subgoal
    apply(simp, subst sin.minus_1[symmetric],subst cos.minus_1[symmetric])
    by (simp add: complex_of_real_i)
  by (simp_all add: complex_of_real_i)
    
lemma winding_eq_intro:
  "finite_ReZ_segments g z 
  valid_path g 
  z  path_image g 
  pathfinish g = pathstart g   
  - of_real(cindex_pathE g z) =2*n 
  winding_number g z = (n::complex)"
apply (subst winding_number_cindex_pathE[of g z])
by (auto simp add:field_simps)
    
named_theorems winding_intros and winding_simps
   
lemmas [winding_intros] = 
  finite_ReZ_segments_joinpaths
  valid_path_join
  path_join_imp
  not_in_path_image_join

lemmas [winding_simps] =
  finite_ReZ_segments_linepath
  finite_ReZ_segments_part_circlepath
  jumpF_pathfinish_joinpaths
  jumpF_pathstart_joinpaths
  pathfinish_linepath
  pathstart_linepath
  pathfinish_join
  pathstart_join
  valid_path_linepath
  valid_path_part_circlepath
  path_part_circlepath
  Re_complex_of_real
  Im_complex_of_real
  of_real_linepath
  pathfinish_pathstart_partcirclepath_simps
    
method rep_subst  =
  (subst cindex_pathE_joinpaths; rep_subst)?
 
  
text ‹
The method "eval\_winding" @{term 1} will try to simplify of the form @{term "winding_number g z = n"} where 
@{term n} is an integer and @{term g} is a closed path comprised of @{term linepath}, 
@{term part_circlepath} and @{term joinpaths}.

Suppose @{term "g=l1+++l2"}, usually, the key behind the success of this framework is whether we can prove 
@{term "z  path_image l1"}, @{term "z  path_image l2"} and calculate @{term "cindex_pathE l1 z"} 
and @{term "cindex_pathE l2 z"}.
›
  
method eval_winding = 
  ((rule_tac winding_eq_intro;
    rep_subst
    )
  , auto simp only:winding_simps del:notI intro!:winding_intros
  , tactic distinct_subgoals_tac)
  
end