Theory Link_Algebra

section‹Link\_Algebra: Defining equivalence of tangles and links›

theory Link_Algebra
imports Tangles Tangle_Algebra Tangle_Moves
begin

inductive Tangle_Equivalence :: "wall ⇒ wall  ⇒ bool"   (infixl "~" 64)
where
  refl [intro!, Pure.intro!, simp]: " a ~  a"
 |equality [Pure.intro]: "linkrel a b ⟹  a ~ b"
 |domain_compose:"(domain_wall a = 0)∧(is_tangle_diagram a) ⟹  a ~  ((basic [])∘a)"
 |codomain_compose:"(codomain_wall a = 0) ∧ (is_tangle_diagram a) ⟹ a ~ (a ∘ (basic []))"
 |compose_eq:"((B::wall) ~ D) ∧ ((A::wall) ~ C)
         ∧(is_tangle_diagram A)∧(is_tangle_diagram B)
         ∧(is_tangle_diagram C)∧(is_tangle_diagram D) 
         ∧(domain_wall B)= (codomain_wall A)
         ∧(domain_wall D)= (codomain_wall C)
                ⟹((A::wall) ∘ B) ~ (C ∘ D)"
 |trans: "A~B ⟹ B~C ⟹ A ~ C"
 |sym:"A~ B ⟹ B ~A"
 |tensor_eq: "((B::wall) ~ D) ∧ ((A::wall) ~ C) ∧(is_tangle_diagram A)∧(is_tangle_diagram B)
 ∧(is_tangle_diagram C)∧(is_tangle_diagram D) ⟹((A::wall) ⊗ B) ~ (C ⊗ D)" 


inductive Framed_Tangle_Equivalence :: "wall ⇒ wall  ⇒ bool"   (infixl "~f" 64)
where
  refl [intro!, Pure.intro!, simp]: " a ~f  a"
 |equality [Pure.intro]: "framed_linkrel a b ⟹  a ~f b"
 |domain_compose:"(domain_wall a = 0) ∧ (is_tangle_diagram a) ⟹  a ~f  ((basic [])∘a)"
 |codomain_compose:"(codomain_wall a = 0) ∧ (is_tangle_diagram a) ⟹ a ~f (a ∘ (basic []))"
 |compose_eq:"((B::wall) ~f D) ∧ ((A::wall) ~f C)
         ∧(is_tangle_diagram A)∧(is_tangle_diagram B)
         ∧(is_tangle_diagram C)∧(is_tangle_diagram D) 
         ∧(domain_wall B)= (codomain_wall A)
         ∧(domain_wall D)= (codomain_wall C)
                ⟹((A::wall) ∘ B) ~f (C ∘ D)"
 |trans: "A~fB ⟹ B~fC ⟹ A ~f C"
 |sym:"A~f B ⟹ B ~fA"
 |tensor_eq: "((B::wall) ~f D) ∧ ((A::wall) ~f C) ∧(is_tangle_diagram A)∧(is_tangle_diagram B)
 ∧(is_tangle_diagram C)∧(is_tangle_diagram D) ⟹((A::wall) ⊗ B) ~f (C ⊗ D)" 


definition Tangle_Diagram_Equivalence::"Tangle_Diagram ⇒ Tangle_Diagram ⇒ bool" 
 (infixl "~T" 64)
where
"Tangle_Diagram_Equivalence T1 T2 ≡ 
(Rep_Tangle_Diagram T1) ~ (Rep_Tangle_Diagram T2)"

definition Link_Diagram_Equivalence::"Link_Diagram ⇒ Link_Diagram ⇒ bool" 
 (infixl "~L" 64)
where
"Link_Diagram_Equivalence T1 T2 ≡ (Rep_Link_Diagram T1) ~ (Rep_Link_Diagram T2)"

quotient_type Tangle = "Tangle_Diagram"/"Tangle_Diagram_Equivalence"
morphisms Rep_Tangles Abs_Tangles
proof (rule equivpI)
 show "reflp Tangle_Diagram_Equivalence" 
         unfolding reflp_def Tangle_Diagram_Equivalence_def 
         Tangle_Equivalence.refl 
         by auto
 show "symp Tangle_Diagram_Equivalence" 
         unfolding Tangle_Diagram_Equivalence_def symp_def
         using  Tangle_Diagram_Equivalence_def Tangle_Equivalence.sym 
         by auto
 show "transp Tangle_Diagram_Equivalence"
         unfolding Tangle_Diagram_Equivalence_def transp_def
         using  Tangle_Diagram_Equivalence_def Tangle_Equivalence.trans 
         by metis
qed

quotient_type Link = "Link_Diagram"/"Link_Diagram_Equivalence"
morphisms Rep_Links Abs_Links
proof (rule equivpI)
 show "reflp Link_Diagram_Equivalence" 
         unfolding reflp_def Link_Diagram_Equivalence_def 
         Tangle_Equivalence.refl 
         by auto
 show "symp Link_Diagram_Equivalence" 
         unfolding Link_Diagram_Equivalence_def symp_def
         using  Link_Diagram_Equivalence_def  Tangle_Equivalence.sym 
         by auto
 show "transp Link_Diagram_Equivalence"
         unfolding Link_Diagram_Equivalence_def transp_def
         using  Link_Diagram_Equivalence_def Tangle_Equivalence.trans 
         by metis
qed

definition Framed_Tangle_Diagram_Equivalence::"Tangle_Diagram ⇒ Tangle_Diagram ⇒ bool" 
 (infixl "~T" 64)
where
"Framed_Tangle_Diagram_Equivalence T1 T2 
          ≡ (Rep_Tangle_Diagram T1) ~ (Rep_Tangle_Diagram T2)"


definition Framed_Link_Diagram_Equivalence::"Link_Diagram ⇒ Link_Diagram ⇒ bool" 
 (infixl "~L" 64)
where
"Framed_Link_Diagram_Equivalence T1 T2 
       ≡ (Rep_Link_Diagram T1) ~ (Rep_Link_Diagram T2)"


quotient_type Framed_Tangle = "Tangle_Diagram"
               /"Framed_Tangle_Diagram_Equivalence"
morphisms Rep_Framed_Tangles Abs_Framed_Tangles
proof (rule equivpI)
 show "reflp Framed_Tangle_Diagram_Equivalence" 
         unfolding reflp_def Framed_Tangle_Diagram_Equivalence_def 
         Framed_Tangle_Equivalence.refl 
         by auto
 show "symp Framed_Tangle_Diagram_Equivalence" 
         unfolding Framed_Tangle_Diagram_Equivalence_def symp_def
         using  Framed_Tangle_Diagram_Equivalence_def 
          Framed_Tangle_Equivalence.sym 
         by (metis Tangle_Equivalence.sym)
 show "transp Framed_Tangle_Diagram_Equivalence"
         unfolding Framed_Tangle_Diagram_Equivalence_def transp_def
         using  Framed_Tangle_Diagram_Equivalence_def Framed_Tangle_Equivalence.trans 
         by (metis Tangle_Equivalence.trans)
qed

quotient_type Framed_Link = "Link_Diagram"/"Framed_Link_Diagram_Equivalence"
morphisms Rep_Framed_Links Abs_Framed_Links
proof (rule equivpI)
 show "reflp Framed_Link_Diagram_Equivalence" 
         unfolding reflp_def Framed_Link_Diagram_Equivalence_def 
         Framed_Tangle_Equivalence.refl 
         by auto
 show "symp Framed_Link_Diagram_Equivalence" 
         unfolding Framed_Link_Diagram_Equivalence_def symp_def
         using  Framed_Link_Diagram_Equivalence_def  Framed_Tangle_Equivalence.sym 
         by (metis Tangle_Equivalence.sym)
 show "transp Framed_Link_Diagram_Equivalence"
         unfolding Framed_Link_Diagram_Equivalence_def transp_def
         using  Framed_Link_Diagram_Equivalence_def Framed_Tangle_Equivalence.trans 
         by (metis Tangle_Equivalence.trans)
 qed

end