Theory Tangle_Moves

section‹Tangle\_Moves: Defining moves on tangles›

theory Tangle_Moves
imports Tangles Tangle_Algebra Tangle_Relation
begin


text‹Two Links diagrams represent the same link if and only if the diagrams can be related by a 
set of moves called the reidemeister moves. For links defined through Tangles, addition set of moves 
are needed to account for different tangle representations of the same link diagram.

We formalise these 'moves' in terms of relations. Each move is defined as a relation on diagrams. 
Two diagrams are then stated to be equivalent if the reflexive-symmetric-transitive closure of the 
disjunction of above relations holds true. A Link is defined as an element of the quotient type of
diagrams modulo equivalence relations. We formalise the definition of framed links on similar lines. 

In terms of formalising the moves, there is a trade off between choosing a small number of moves
from which all other moves can be obtained, which is conducive to probe invariance of a function 
on diagrams. However, such an approach might not be conducive to establish equivalence of two 
diagrams. We opt for the former approach of minimising the number of tangle moves. 
However, the moves that would be useful in practise are proved as theorems in
›


type_synonym relation = "wall ⇒ wall ⇒ bool" 

text‹Link uncross›

abbreviation right_over::"wall"
where
"right_over ≡   ((basic [vert,cup]) ∘ (basic [over,vert])∘(basic [vert,cap]))"


abbreviation left_over::"wall"
where
" left_over ≡ ((basic (cup#vert#[])) ∘ (basic (vert#over#[]))
∘ (basic (cap#vert#[])))"

abbreviation right_under::"wall"
where
"right_under ≡   ((basic (vert#cup#[])) ∘ (basic (under#vert#[]))
∘ (basic (vert#cap#[])))"


abbreviation left_under::"wall"
where
" left_under ≡ ((basic (cup#vert#[])) ∘ (basic (vert#under#[]))
∘ (basic (cap#vert#[])))"

abbreviation straight_line::"wall"
where
"straight_line ≡ (basic (vert#[])) ∘ (basic (vert#[])) ∘ (basic (vert#[]))"

definition uncross_positive_flip::relation
where
"uncross_positive_flip x y ≡ ((x = right_over)∧(y =  left_over))"

definition uncross_positive_straighten::relation
where
"uncross_positive_straighten x y ≡ ((x = right_over)∧(y = straight_line))"

definition uncross_negative_flip::relation
where
"uncross_negative_flip x y ≡ ((x = right_under)∧(y =  left_under))"


definition uncross_negative_straighten::relation
where
"uncross_negative_straighten x y ≡ ((x = left_under)∧(y = straight_line))"

(*The relation uncross*)
definition uncross
where
"uncross x y ≡ ((uncross_positive_straighten x y)∨(uncross_positive_flip x y)
                ∨(uncross_negative_straighten x y)∨ (uncross_negative_flip x y))"



text‹swing begins›

abbreviation r_over_braid::"wall"
where
"r_over_braid  ≡  ((basic ((over#vert#[]))∘(basic ((vert#over#[])))
                 ∘(basic (over# vert#[]))))"



abbreviation l_over_braid::"wall"
where
"l_over_braid  ≡   (basic (vert#over#[]))∘(basic (over#vert#[]))
                    ∘(basic (vert#over#[]))"


abbreviation r_under_braid::"wall"
where
"r_under_braid  ≡   ((basic ((under#vert#[]))∘(basic ((vert#under#[])))
                 ∘(basic (under# vert#[]))))"

abbreviation l_under_braid::"wall"
where
"l_under_braid  ≡   (basic (vert#under#[]))∘(basic (under#vert#[]))
                    ∘(basic (vert#under#[]))"

definition swing_pos::"wall ⇒ wall ⇒ bool"
where
"swing_pos x y ≡ (x = r_over_braid)∧(y = l_over_braid)"

definition swing_neg::"wall ⇒ wall ⇒ bool"
where
"swing_neg x y ≡(x = r_under_braid)∧(y=l_under_braid)"

definition swing::relation
where
"swing x y ≡ (swing_pos x y)∨(swing_neg x y)"

text‹pull begins›

definition pull_posneg::relation
where
"pull_posneg x y ≡  ((x = ((basic (over#[]))∘(basic  (under#[]))))
                            ∧(y = ((basic (vert#vert#[])))
                                   ∘(basic ((vert#vert#[])))))"


definition pull_negpos::relation
where
"pull_negpos x y ≡  ((x = ((basic (under#[]))∘(basic  (over#[]))))
                          ∧(y = ((basic (vert#vert#[])))
                                   ∘(basic ((vert#vert#[])))))"

text‹pull definition›
definition pull::relation
where
"pull x y ≡ ((pull_posneg x y) ∨ (pull_negpos x y))"                   

text‹linkrel-pull ends›    
text‹linkrel-straighten›

definition straighten_topdown::relation
where
"straighten_topdown x y ≡  ((x =((basic ((vert#cup#[])))
                                         ∘(basic ((cap#vert#[])))))
                                   ∧(y = ((basic (vert#[]))∘(basic (vert#[])))))"



definition straighten_downtop::relation
where
"straighten_downtop x y ≡  ((x =((basic ((cup# vert#[])))
                                         ∘(basic ((vert# cap#[])))))
                                   ∧(y = ((basic (vert#[]))∘(basic (vert#[])))))"




text‹definition straighten›
definition straighten::relation
where
"straighten x y ≡ ((straighten_topdown x y) ∨ (straighten_downtop x y))"



text‹straighten ends›
text‹rotate moves›

definition rotate_toppos::relation
where
"rotate_toppos x y ≡  ((x = ((basic ((vert #over#[])))
                                     ∘(basic ((cap# vert#[])))))
                             ∧ (y = ((basic ((under#vert#[]))
                                     ∘(basic ((vert#cap#[])))))))"

definition rotate_topneg::"wall ⇒ wall ⇒ bool"
where
"rotate_topneg x y ≡  ((x = ((basic ((vert #under#[])))
                                     ∘(basic ((cap# vert#[])))))
                             ∧ (y = ((basic ((over#vert#[]))
                                     ∘(basic ((vert#cap#[])))))))"


definition rotate_downpos::"wall ⇒ wall ⇒ bool"
where
"rotate_downpos x y ≡  ((x = ((basic (cup#vert#[]))
                                     ∘(basic (vert#over#[]))))
                             ∧ (y = ((basic ((vert#cup#[])))
                                    ∘(basic ((under#vert#[]))))))"



definition rotate_downneg::"wall ⇒ wall ⇒ bool"
where
"rotate_downneg x y ≡  ((x = ((basic (cup#vert#[]))
                                     ∘(basic (vert#under#[]))))
                             ∧ (y = ((basic ((vert#cup#[])))
                                    ∘(basic ((over#vert#[]))))))"


text‹rotate definition›


definition rotate::"wall ⇒ wall ⇒ bool"
where
"rotate x y ≡ ((rotate_toppos x y) ∨ (rotate_topneg x y)
∨ (rotate_downpos x y) ∨ (rotate_downneg x y))"

text‹rotate ends›


text‹Compress -  Compress has two levels of equivalences. It is a composition of Compress-null, compbelow
and compabove. compbelow and compabove are further written as disjunction of many other relations.
Compbelow refers to when the bottom row is extended or compressed. Compabove refers to when the 
row above is extended or compressed›

definition compress_top1::"wall ⇒ wall ⇒ bool"
where
"compress_top1 x y ≡  ∃B.((x = (basic (make_vert_block (nat (domain_wall B))))∘ B)
                              ∧(y = B)∧(codomain_wall B ≠ 0)
                               ∧(is_tangle_diagram B))"

definition compress_bottom1::"wall ⇒ wall ⇒ bool"
where
"compress_bottom1 x y ≡  ∃B.((x = B ∘ (basic (make_vert_block (nat (codomain_wall B)))))
                              ∧(y =  B))∧(domain_wall B ≠ 0)
                               ∧(is_tangle_diagram B)"

definition compress_bottom::"wall ⇒ wall ⇒ bool"
where
"compress_bottom x y ≡   ∃B.((x = B ∘ (basic (make_vert_block (nat (codomain_wall B)))))
                              ∧(y = ((basic ([]) ∘ B)))∧(domain_wall B = 0)
                               ∧(is_tangle_diagram B))"

definition compress_top::"wall ⇒ wall ⇒ bool"
where
"compress_top x y ≡  ∃B.((x = (basic (make_vert_block (nat (domain_wall B))))∘ B)
                              ∧(y = (B ∘ (basic ([]))))∧(codomain_wall B = 0)
                               ∧(is_tangle_diagram B))"


(*compress*)
definition compress::"wall ⇒ wall ⇒ bool"
where
"compress x y = ((compress_top x y) ∨ (compress_bottom x y))"
(*(compress_top1 x y) ∨ (compress_bottom1 x y))*)
text‹slide relation refer to the relation where a crossing is slided over a vertical strand›
definition slide::"wall ⇒ wall ⇒ bool"
where
"slide x y ≡  ∃B.((x = ((basic (make_vert_block (nat (domain_block B))))∘(basic B)))
               ∧(y = ((basic B)∘(basic (make_vert_block (nat (codomain_block B))))))
∧ ((domain_block B) ≠ 0))"
(*can integrate slide and compress using domain-codomain fundas.
ALSO check for domain and codomain in the above equations*)
text‹linkrel-definition›

definition linkrel::"wall =>wall ⇒bool"
where
"linkrel x y = ((uncross x y) ∨ (pull x y) ∨ (straighten x y) 
∨(swing x y)∨(rotate x y) ∨ (compress x y) ∨ (slide x y))"


definition framed_uncross::"wall ⇒ wall ⇒ bool"
where
"framed_uncross x y ≡ ((uncross_positive_flip x y)∨(uncross_negative_flip x y))"

definition framed_linkrel::"wall =>wall ⇒bool"
where
"framed_linkrel x y = ((framed_uncross x y) ∨ (pull x y) ∨ (straighten x y) 
∨(swing x y)∨(rotate x y) ∨ (compress x y) ∨ (slide x y))"



lemma framed_uncross_implies_uncross: "(framed_uncross x y)⟹(uncross x y)"
 by (auto simp add: framed_uncross_def uncross_def)


end