Theory Example

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 
unknot›

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