Quelle  Example.thy

section‹Showing equivalence of links: An example›

theory Example
imports Link_Algebra 
begin

text‹We prove that a link diagram with a single crossing is equivalent to the
 ›

lemma transitive: assumes "a~b" and "b~c" shows "a~c"
    using Tangle_Equivalence.trans assms(1) assms(2) by metis

lemma prelim_cup_compress:
 " ((basic (cup#[])) ∘ (basic (vert # vert # []))) ~
      ((basic [])∘(basic (cup#[])))"  
proof-
 have "domain_wall (basic (cup # [])) = 0" 
       by auto
 moreover have "codomain_wall (basic (cup # [])) = 2" 
       by auto
 moreover 
     have "make_vert_block (nat (codomain_wall (basic (cup # []))))
                                    = (vert # vert # [])"
       unfolding make_vert_block_def 
       by auto
 moreover have "is_tangle_diagram ((basic (cup#[])) ∘ (basic (vert # vert # [])))"
      using is_tangle_diagram.simps by auto 
 ultimately 
  have "compress_bottom
          ((basic (cup#[])) ∘ (basic (vert # vert # [])))
          ((basic []) ∘(basic (cup#[])))" 
      using compress_bottom_def by (metis is_tangle_diagram.simps(1))
 then have "compress ((basic (cup#[])) ∘ (basic (vert # vert # [])))
      ((basic [])∘(basic (cup#[])))" 
      using compress_def by auto
 then have "linkrel ((basic (cup#[])) ∘ (basic (vert # vert # [])))
      ((basic [])∘(basic (cup#[])))" 
      unfolding linkrel_def by auto
 then show ?thesis 
     using Tangle_Equivalence.equality compress_bottom_def 
           Tangle_Moves.compress_bottom_def Tangle_Moves.compress_def 
           Tangle_Moves.linkrel_def 
     by auto
 qed

lemma cup_compress:
 "(basic (cup#[])) ∘ (basic (vert # vert # [])) ~ (basic (cup#[]))"
 proof-
 have " ((basic (cup#[])) ∘ (basic (vert # vert # []))) ~
      ((basic [])∘(basic (cup#[])))"  
         using prelim_cup_compress  by auto
 moreover have "((basic [])∘(basic (cup#[]))) ~ (basic (cup#[]))"
         using domain_compose refl sym Tangle_Equivalence.domain_compose 
         Tangle_Equivalence.sym domain.simps(2) domain_block.simps 
         domain_wall.simps(1) 
         is_tangle_diagram.simps(1) monoid_add_class.add.right_neutral
         by auto
 ultimately show ?thesis using trans by (metis Example.transitive)
 qed
 
abbreviation x::"wall"
where
"x ≡ (basic [cup,cup])∘(basic [vert,over,vert]) ∘ (basic [cap,cap])"

abbreviation y::"wall"
where
"y ≡ (basic [cup]) ∘ (basic [cap])"

lemma uncross_straighten_left_over:"left_over ~ straight_line"
proof-
 have "uncross right_over left_over"
        using uncross_positive_flip_def uncross_def by auto
 then have "linkrel right_over left_over"
    using linkrel_def by auto
 then have "right_over ~ left_over"
    using Tangle_Equivalence.equality by auto
 then have 1:"left_over ~ right_over"
    using Tangle_Equivalence.sym by auto
  have "uncross right_over straight_line"
        using uncross_positive_straighten_def uncross_def by auto
 then have "linkrel right_over straight_line"
    using linkrel_def by auto
 then have 2:"right_over ~ straight_line"
    using Tangle_Equivalence.equality by auto
  have "(left_over ~ straight_line) ∧ (right_over ~ straight_line)
         ==> ?thesis" 
            using transitive by auto
 then show ?thesis using 1 2 transitive  by blast
 qed



theorem Example:
  "x ~ y" 
proof-
 have 1:"left_over ~ straight_line"
    using Tangle_Equivalence.equality uncross_straighten_left_over by auto
 moreover have 2:"straight_line ~ straight_line"
   using refl by auto
 have 3:"(left_over ⊗ straight_line) ~ (straight_line ⊗ straight_line)"
 proof-
  have "is_tangle_diagram (left_over)"
    unfolding is_tangle_diagram_def by auto 
  moreover have "is_tangle_diagram (straight_line)"
    unfolding is_tangle_diagram_def by auto
  ultimately show ?thesis using 1 2 by (metis Tangle_Equivalence.tensor_eq)
 qed
 then have 4:
  "((basic (cup#[])) ∘ (left_over ⊗ straight_line))
           ~ ((basic (cup#[])) ∘ (straight_line ⊗ straight_line))"
 proof-
  have "is_tangle_diagram (left_over ⊗ straight_line)"
        by auto
  moreover have "is_tangle_diagram (straight_line ⊗ straight_line)"
        by auto
  moreover have "is_tangle_diagram (basic (cup#[]))" 
         by auto
  moreover have "domain_wall (left_over ⊗ straight_line) = (codomain_wall (basic (cup#[])))"
        unfolding domain_wall_def by auto
  moreover have "domain_wall (straight_line ⊗ straight_line) = (codomain_wall (basic (cup#[])))"
        unfolding domain_wall_def by auto
  moreover have "(basic (cup#[])) ~ (basic (cup#[]))" 
        using refl by auto
  ultimately show ?thesis 
        using compose_eq 3  by (metis Tangle_Equivalence.compose_eq)
 qed
 moreover have 5:" (basic [cup])∘ (straight_line ⊗ straight_line)
                 ~ (basic [cup])"
 proof-
  have 0:
   "(basic ([cup])) ∘ (straight_line ⊗ straight_line) = (basic [cup]) ∘(basic [vert,vert])
                                                         ∘ (basic [vert,vert])∘(basic [vert,vert])"
           by auto
  let ?x ="(basic (cup#[]))
   ∘(basic (vert#vert#[])) ∘ (basic (vert#vert#[]))
   ∘ (basic (vert#vert#[]))"
  let ?x1 = " (basic (vert#vert#[]))∘ (basic (vert#vert#[]))"
  have 1:"?x ~ ((basic (cup#[])) ∘ ?x1)"
  proof-
   have "(basic (cup#[]))∘(basic (vert # vert # [])) ~ (basic (cup#[]))"
        using cup_compress by auto
   moreover have "is_tangle_diagram (basic (cup#[]))" 
        using is_tangle_diagram_def by auto
   moreover have "is_tangle_diagram ((basic (cup#[]))∘(basic (vert # vert # [])))"
        using is_tangle_diagram_def by auto
   moreover have "is_tangle_diagram (?x1)"
        by auto
   moreover have "?x1 ~ ?x1" 
        using refl by auto       
   moreover have 
     "codomain_wall (basic (cup#[])) = domain_wall (basic (vert#vert#[]))"
        by auto
   moreover have "(basic (cup#[])) ~ (basic (cup#[]))"
         using refl by auto
   ultimately show ?thesis 
         using compose_eq codomain_wall_compose compose_leftassociativity 
               converse_composition_of_tangle_diagrams domain_wall_compose
         by (metis Tangle_Equivalence.compose_eq is_tangle_diagram.simps(1))
  qed
  have 2: " ((basic (cup#[])) ∘ ?x1) ~ (basic (cup#[]))"
  proof-
   have "
     ((basic (cup # []))∘(basic (vert # vert # [])))∘(basic (vert # vert # []))
          ~ ((basic(cup#[]))∘(basic(vert#vert#[])))"
   proof-
    have "(basic (cup#[]))∘(basic (vert # vert # [])) ~ (basic (cup#[]))"
         using cup_compress by auto
    moreover have "(basic(vert#vert#[])) ~ (basic(vert#vert#[]))" 
         using refl by auto  
    moreover have "is_tangle_diagram (basic (cup#[]))" 
         using is_tangle_diagram_def by auto
    moreover have "is_tangle_diagram ((basic (cup#[]))∘(basic (vert # vert # [])))"
         using is_tangle_diagram_def by auto
    moreover have "is_tangle_diagram ((basic(vert#vert#[])))"
         by auto     
    moreover have 
         "codomain_wall ((basic (cup#[]))∘ (basic(vert#vert#[])))
                       = domain_wall (basic(vert#vert#[])) "
         by auto
    moreover 
         have "codomain_wall (basic (cup#[])) = domain_wall (basic(vert#vert#[]))"
         by auto       
    ultimately show ?thesis 
                 using compose_eq 
                 by (metis Tangle_Equivalence.compose_eq)
   qed 
   then have "((basic (cup#[])) ∘ ?x1) ~
           ((basic(cup#[]))∘(basic(vert#vert#[])))"
         by auto
   then show ?thesis using cup_compress trans
         by (metis (full_types) Example.transitive)
  qed
  from 0 1 2 show ?thesis using trans transp_def trans compose_Nil
          by (metis (opaque_lifting, no_types) Example.transitive)
 qed
 let ?y = "((basic ([])) ∘ (basic (cup#[]))) "
 let ?temp = "(basic (vert#over#vert#[]))∘(basic (cap#vert#vert#[])) "  
 have 45:"(left_over ⊗ straight_line) =
          ((basic (cup#vert#vert#[])) ∘ ?temp)"  
          using tensor.simps by (metis compose_Nil concatenates_Cons concatenates_Nil)
 then have 55:"(basic (cup#[])) ∘ (left_over ⊗ straight_line)
             = (basic (cup#[])) ∘ (basic (cup#vert#vert#[])) ∘ ?temp"
          by auto
 then have 
  "(basic (cup#[])) ∘ (basic (cup#vert#vert#[]))
      = (basic (([]) ⊗(cup#[])))∘(basic ((cup#[])⊗(vert#vert#[])))"
          using concatenate.simps  by auto
 then have 6:
 "(basic (cup#[])) ∘ (basic (cup#vert#vert#[]))
          = ((basic ([]))∘(basic (cup#[])))
            ⊗((basic (cup#[])) ∘(basic (vert#vert#[])))"
          using tensor.simps by auto
 then have "((basic (cup#[])) ∘(basic (vert#vert#[])))
                   ~ (basic ([]))∘(basic (cup#[]))"
          using prelim_cup_compress by auto
 moreover have "((basic ([]))∘(basic (cup#[])))
                       ~ ((basic ([]))∘(basic (cup#[])))"
          using refl by auto
 moreover have "is_tangle_diagram ((basic (cup#[])) ∘(basic (vert#vert#[])))"
          by auto
 moreover have "is_tangle_diagram ((basic ([]))∘(basic (cup#[]))) "
          by auto
 ultimately have 7:"?y ⊗ ((basic (cup#[])) ∘(basic (vert#vert#[])))~ ((?y) ⊗ (?y))"
          using tensor_eq cup_compress Nil_right_tensor is_tangle_diagram.simps(1) refl
          by (metis Tangle_Equivalence.tensor_eq)
 then have " ((?y) ⊗ (?y)) = (basic (([]) ⊗ ([])))
                   ∘ ((basic (cup#[])) ⊗ (basic (cup#[])))"
          using tensor.simps(4)  by (metis compose_Nil) 
 then have " ((?y) ⊗ (?y)) = (basic ([])) ∘((basic (cup#cup#[])))"
          using tensor.simps(1) concatenate_def by auto
 then have "(?y) ⊗ ((basic (cup#[])) ∘(basic (vert#vert#[])))
             ~ (basic ([])) ∘(basic (cup#cup#[]))" 
          using 7 by auto
 moreover have "(basic ([]))∘(basic (cup#cup#[]))~(basic (cup#cup#[]))"
 proof-
  have "domain_wall (basic (cup#cup#[])) = 0"
          by auto
  then show ?thesis using domain_compose sym 
          by (metis Tangle_Equivalence.domain_compose Tangle_Equivalence.sym is_tangle_diagram.simps(1))
 qed
 ultimately have "(?y) ⊗ ((basic (cup#[])) ∘(basic (vert#vert#[])))
               ~ (basic (cup#cup#[]))"
          using trans  by (metis (full_types) Example.transitive)
 then have " (basic(cup#[]))∘(basic(cup#vert#vert#[]))~(basic(cup#cup#[]))" 
          by auto
 moreover have "?temp ~ ?temp"
          using refl by auto
 moreover  have "is_tangle_diagram ((basic(cup#[]))∘(basic(cup#vert#vert#[])))"
          by auto
 moreover have "is_tangle_diagram (basic(cup#cup#[]))"
          by auto
 moreover have "is_tangle_diagram (?temp)"
          by auto
 moreover have "codomain_wall ((basic(cup#[]))∘(basic(cup#vert#vert#[])))
                    = domain_wall ?temp"
          by auto
 moreover have "codomain_wall (basic(cup#cup#[])) = domain_wall ?temp"
          by auto
 ultimately have 8:" ((basic(cup#[]))∘(basic(cup#vert#vert#[]))) ∘(?temp)
                       ~ (basic(cup#cup#[])) ∘ (?temp)"
          using compose_eq by (metis Tangle_Equivalence.compose_eq)
 then have "((basic [cup,cup]) ∘ (?temp))
                 ~ (basic [cup] ∘ (left_over ⊗ straight_line))"
          using 55 compose_leftassociativity sym wall.simps   
          by (metis Tangle_Equivalence.sym compose_Nil)
 moreover have "(basic [cup]) ∘ (left_over ⊗ straight_line)
                    ~ (basic [cup]) ∘ (straight_line ⊗ straight_line)"
          using 4 by auto
 ultimately have "((basic [cup,cup]) ∘ (?temp))
                  ~ (basic [cup]) ∘ (straight_line ⊗ straight_line)"          
  proof-
   have "((basic [cup,cup]) ∘ (?temp))
                 ~ (basic [cup] ∘ (left_over ⊗ straight_line))"
          using 8 55 compose_leftassociativity sym wall.simps  Tangle_Equivalence.sym compose_Nil  
          by (metis)    
   moreover have "(basic [cup]) ∘ (left_over ⊗ straight_line)
                    ~ (basic [cup]) ∘ (straight_line ⊗ straight_line)"
          using 4 by auto
   moreover have "(((basic [cup,cup]) ∘ (?temp))
                 ~ (basic [cup] ∘ (left_over ⊗ straight_line)))
        ∧ ((basic [cup]) ∘ (left_over ⊗ straight_line)
                    ~ (basic [cup]) ∘ (straight_line ⊗ straight_line))
           ==> ?thesis"
          using Example.transitive by auto
   ultimately show ?thesis by auto
  qed
  then have "(basic ([cup,cup])) ∘ (?temp) ~ (basic (cup # []))"
         using trans transp_def 5 by (metis Example.transitive)
  moreover have "(basic (cap#[])) ~ (basic (cap#[]))"
         using refl by auto
  moreover have "is_tangle_diagram ((basic(cup#cup#[])) ∘ (?temp))"
         by auto
  moreover have "is_tangle_diagram (basic (cup # []))"
         by auto
  moreover have "is_tangle_diagram (basic (cap # []))"
         by auto
  moreover have "codomain_wall ((basic(cup#cup#[])) ∘ (?temp))
                   = domain_wall (basic (cap # []))"
         by auto
  moreover have "codomain_wall (basic(cup#[])) = domain_wall (basic (cap # []))"
         by auto
 ultimately have 9:"((basic(cup#cup#[])) ∘ (?temp)) ∘ (basic (cap#[]))
                     ~ (basic (cup#[])) ∘ (basic (cap#[]))"
         using Tangle_Equivalence.compose_eq by metis
  let ?z = "((basic(cup#cup#[])) ∘ (basic(vert#over#vert#[])))"
  have 10:"((basic(cup#cup#[])) ∘ (?temp)) ∘ (basic (cap#[]))
              = ?z ∘ ((basic(cap#vert#vert#[])) ∘ (basic (cap#[])))"
         by auto
  then have 11:"((basic(cap#vert#vert#[])) ∘ (basic (cap#[])))
                           = ((basic ((cap#[])⊗(vert#vert#[])))∘(basic (([]) ⊗(cap#[]))))"
          unfolding concatenate_def by auto
  then have 12:" ((basic(cap#vert#vert#[])) ∘ (basic (cap#[])))
                       = ((basic (cap#[]))∘(basic ([])))⊗((basic (vert#vert#[]))∘(basic (cap#[])))"
          using tensor.simps by auto
  let ?w = "((basic (cap#[]))∘(basic ([])))"
  have 13:"((basic (vert#vert#[]))∘(basic (cap#[]))) ~ ?w"
  proof-
   have "codomain_wall (basic (cap#[])) = 0" 
        by auto
   then have "domain_wall (basic (cap#[])) = 2" by auto
   then have "(vert#vert#[])
                          = make_vert_block (nat (domain_wall (basic (cap#[]))))"
     by (simp add: make_vert_block_def)
   then have "compress_top ((basic (vert#vert#[]))∘(basic (cap#[]))) ?w"
        using compress_top_def by auto
   then have "compress ((basic (vert#vert#[]))∘(basic (cap#[]))) ?w" 
        using compress_def by auto
   then have "linkrel ((basic (vert#vert#[]))∘(basic (cap#[]))) ?w" 
        using linkrel_def by auto
   then have " ((basic (vert#vert#[]))∘(basic (cap#[]))) ~ ?w"
        using Tangle_Equivalence.equality by auto
   then show ?thesis by simp
  qed
  moreover have "is_tangle_diagram ((basic (vert#vert#[]))∘(basic (cap#[])))"
        by auto
  moreover have "is_tangle_diagram ?w"
        by auto
  moreover have "?w ~ ?w" 
        using refl by auto
  ultimately have 14:"(?w) ⊗ ((basic (vert#vert#[]))∘(basic (cap#[]))) ~ ((?w)⊗ (?w))"
        using Tangle_Equivalence.tensor_eq by metis
  then have "((basic(cap#vert#vert#[])) ∘ (basic (cap#[]))) ~ ((?w)⊗ (?w))"
        using 13 by auto
  moreover have " ((?w)⊗ (?w)) = (basic (cap#cap#[])) ∘ (basic ([]))"
        using tensor.simps by auto
  ultimately have "((basic(cap#vert#vert#[]))∘(basic (cap#[])))~ (basic (cap#cap#[]))∘(basic ([]))"
        by auto
  moreover have "?z ~ ?z" 
        using refl by auto
  moreover have "domain_wall ((basic(cap#cap#[])) ∘ (basic ([])))
                                = codomain_wall (?z)"
        by auto
  moreover have "domain_wall (((basic(cap#vert#vert#[])) ∘ (basic (cap#[]))))
                                = codomain_wall (?z)" 
        by auto
  moreover have "is_tangle_diagram ((basic(cap#vert#vert#[])) ∘ (basic (cap#[])))"
        by auto
  moreover have "is_tangle_diagram (?z)"
        by auto
  moreover have "is_tangle_diagram ((basic(cap#cap#[])) ∘ (basic ([])))"
        by auto
  ultimately have 14:" (?z) ∘ ((basic(cap#vert#vert#[])) ∘ (basic (cap#[])))
                      ~ (?z) ∘ ((basic(cap#cap#[])) ∘ (basic ([])))" (is "?aa ~ ?bb")
        using Tangle_Equivalence.compose_eq by metis
  moreover  have 15: "((?z) ∘ ((basic(cap#cap#[]))) ∘ (basic ([])))
                ~ ((?z) ∘ (basic(cap#cap#[])))" (is "?bb ~ ?cc")
        using Tangle_Equivalence.codomain_compose  Tangle_Equivalence.sym 
               ‹is_tangle_diagram (basic [cap, cap] ∘ basic [])› codomain_wall_compose 
               compose_leftassociativity converse_composition_of_tangle_diagrams 
               domain_block.simps(1) domain_wall.simps(1)
        by (metis (opaque_lifting, mono_tags) Tangle_Equivalence.compose_eq 
                Tangle_Equivalence.refl 
                ‹codomain_wall (basic [cup, cup])
 = domain_wall (basic [vert, over, vert] ∘ basic [cap, vert, vert])›
                   ‹domain_wall (basic [cap, cap] ∘ basic [])
 = codomain_wall (basic [cup, cup] ∘ basic [vert, over, vert])›
                          comp_of_tangle_dgms domain_wall_compose is_tangle_diagram.simps(1))
  ultimately have "(?aa ~ ?bb)∧ (?bb ~ ?cc) ==>?aa ~ ?cc"
        using transitive by auto
  then have 16:"?aa ~ ?cc"
        using 14 15 by auto
  then have 17:" ((basic (cup#[]))∘(basic (cap#[])))~ ?aa"
        using 9 10 Tangle_Equivalence.trans  Tangle_Equivalence.sym 
        by (metis (opaque_lifting, no_types))
  have "(((basic (cup#[]))∘(basic (cap#[])))~ ?aa)∧(?aa ~ ?cc)
            ==> ((basic (cup#[]))∘(basic (cap#[])))~ ?cc" 
        using transitive by auto
  then have "((basic (cup#[]))∘(basic (cap#[])))~ ?cc"
            using 17 16 by auto
  then show ?thesis using Tangle_Equivalence.sym by auto
qed
    
end