Theory Winding_Number_Eval_Examples

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

section ‹Some examples of applying the method winding\_eval›

theory Winding_Number_Eval_Examples imports Winding_Number_Eval
begin
  
lemma example1:
  assumes "R>1"
  shows "winding_number (part_circlepath 0 R 0 pi +++ linepath (-R) R) 𝗂 = 1"
proof (eval_winding,simp_all)
  define CR where  "CR ≡part_circlepath 0 R 0 pi"
  define L where "L≡ linepath (- (complex_of_real R)) R"
  show "𝗂 ∉ path_image CR" unfolding CR_def using ‹R>1›
    by (intro not_on_circlepathI,auto)  
  show *:"𝗂 ∉ closed_segment (- (of_real R)) R" using ‹R>1› complex_eq_iff
    by (intro not_on_closed_segmentI,auto)
  from cindex_pathE_linepath[OF this] have "cindex_pathE L 𝗂 = -1"
    unfolding L_def using ‹R>1› by auto
  moreover have "cindex_pathE CR 𝗂 = -1"
    unfolding CR_def using ‹R>1› 
    apply (subst cindex_pathE_part_circlepath)
    by (simp_all add:jumpF_pathstart_part_circlepath jumpF_pathfinish_part_circlepath)
  ultimately show "- complex_of_real (cindex_pathE CR 𝗂) - cindex_pathE L 𝗂 = 2"
    unfolding L_def CR_def by auto
qed

lemma example2:
  assumes "R>1"
  shows "winding_number (part_circlepath 0 R 0 pi +++ linepath (-R) R) (-𝗂) = 0"
proof (eval_winding,simp_all)
  define CR where  "CR ≡part_circlepath 0 R 0 pi"
  define L where "L≡ linepath (- (complex_of_real R)) R"
  show "-𝗂 ∉ path_image CR" unfolding CR_def using ‹R>1›
    by (intro not_on_circlepathI,auto)  
  show *:"-𝗂 ∉ closed_segment (- (of_real R)) R" using ‹R>1› complex_eq_iff
    by (intro not_on_closed_segmentI,auto)
  from cindex_pathE_linepath[OF this] have "cindex_pathE L (-𝗂) = 1"
    unfolding L_def using ‹R>1› by auto
  moreover have "cindex_pathE CR (-𝗂) = -1"
    unfolding CR_def using ‹R>1› 
    apply (subst cindex_pathE_part_circlepath)
    by (simp_all add:jumpF_pathstart_part_circlepath jumpF_pathfinish_part_circlepath)
  ultimately show "-cindex_pathE CR (-𝗂) = cindex_pathE L (-𝗂)"
    unfolding L_def CR_def by auto    
qed
 
lemma example3:
  fixes lb ub z :: complex
  defines "rec ≡  linepath lb (Complex (Re ub) (Im lb)) +++ linepath (Complex (Re ub) (Im lb)) ub 
              +++ linepath ub (Complex (Re lb) (Im ub)) +++ linepath (Complex (Re lb) (Im ub)) lb"
  assumes order_asms:"Re lb < Re z" "Re z < Re ub" "Im lb < Im z" "Im z < Im ub"
  shows "winding_number rec z = 1"
  unfolding rec_def
proof (eval_winding)    
  let ?l1 = "linepath lb (Complex (Re ub) (Im lb))"
  and ?l2 = "linepath (Complex (Re ub) (Im lb)) ub"
  and ?l3 = "linepath ub (Complex (Re lb) (Im ub))"
  and ?l4 = "linepath (Complex (Re lb) (Im ub)) lb"
  show l1: "z ∉ path_image ?l1" 
    apply (auto intro!: not_on_closed_segmentI_complex)
    using order_asms by (simp add: algebra_simps crossproduct_eq)
  show l2:"z ∉ path_image ?l2" 
    apply (auto intro!: not_on_closed_segmentI_complex)      
    using order_asms by (simp add: algebra_simps crossproduct_eq)
  show l3:"z ∉ path_image ?l3" 
    apply (auto intro!: not_on_closed_segmentI_complex)      
    using order_asms by (simp add: algebra_simps crossproduct_eq)
  show l4:"z ∉ path_image ?l4"  
    apply (auto intro!: not_on_closed_segmentI_complex)      
    using order_asms by (simp add: algebra_simps crossproduct_eq)
  show "- complex_of_real (cindex_pathE ?l1 z + (cindex_pathE ?l2 z + (cindex_pathE ?l3 z +
          cindex_pathE ?l4 z))) = 2 * 1"  
  proof -
    have "(Im z - Im ub) * (Re ub - Re lb) < 0" 
      using mult_less_0_iff order_asms(1) order_asms(2) order_asms(4) by fastforce
    then have "cindex_pathE ?l3 z = -1"
      apply (subst cindex_pathE_linepath)
      using l3 order_asms by (auto simp add:algebra_simps)
    moreover have "(Im lb - Im z) * (Re ub - Re lb) <0" 
      using mult_less_0_iff order_asms(1) order_asms(2) order_asms(3) by fastforce
    then have "cindex_pathE ?l1 z = -1"    
      apply (subst cindex_pathE_linepath)
      using l1 order_asms by (auto simp add:algebra_simps)  
    moreover have "cindex_pathE ?l2 z = 0"    
      apply (subst cindex_pathE_linepath)
      using l2 order_asms by (auto simp add:algebra_simps)  
    moreover have "cindex_pathE ?l4 z = 0"
      apply (subst cindex_pathE_linepath)
      using l4 order_asms by (auto simp add:algebra_simps) 
    ultimately show ?thesis by auto
  qed
qed
   
end