# Theory Winding_Number_Eval_Examples

theory Winding_Number_Eval_Examples
imports Winding_Number_Eval
```(*
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)
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)
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
```