(* Title: Turing machine's definition and its charater

   Author: XuJian <xujian817@hotmail.com>

   Maintainer: Xujian

*)

header {* Undeciablity of the {\em Halting problem} *}

theory uncomputable

imports Main turing_basic

begin

text {*

  The {\em Copying} TM, which duplicates its input. 

*}

definition tcopy :: "tprog"

where

"tcopy \<equiv> [(W0, 0), (R, 2), (R, 3), (R, 2),

          (W1, 3), (L, 4), (L, 4), (L, 5), (R, 11), (R, 6), 

          (R, 7), (W0, 6), (R, 7), (R, 8), (W1, 9), (R, 8),

          (L, 10), (L, 9), (L, 10), (L, 5), (R, 12), (R, 12),

          (W1, 13), (L, 14), (R, 12), (R, 12), (L, 15), (W0, 14),

          (R, 0), (L, 15)]"

text {*

  @{text "wipeLastBs tp"} removes all blanks at the end of tape @{text "tp"}.

*}

fun wipeLastBs :: "block list \<Rightarrow> block list"

  where 

  "wipeLastBs bl = rev (dropWhile (\<lambda>a. a = Bk) (rev bl))"

fun isBk :: "block \<Rightarrow> bool"

  where

  "isBk b = (b = Bk)"

text {*

  The following functions are used to expression invariants of {\em Copying} TM.

*}

fun tcopy_F0 :: "nat \<Rightarrow> tape \<Rightarrow> bool"

  where

fun tcopy_F1 :: "nat \<Rightarrow> tape \<Rightarrow> bool"

  where

fun tcopy_F2 :: "nat \<Rightarrow> tape \<Rightarrow> bool"

fun tcopy_F3 :: "nat \<Rightarrow> tape \<Rightarrow> bool"

  where

fun tcopy_F4 :: "nat \<Rightarrow> tape \<Rightarrow> bool"

  where

fun tcopy_F5 :: "nat \<Rightarrow> tape \<Rightarrow> bool"

  where

fun tcopy_F6 :: "nat \<Rightarrow> tape \<Rightarrow> bool"

  where

fun tcopy_F7 :: "nat \<Rightarrow> tape \<Rightarrow> bool"

  where

fun tcopy_F8 :: "nat \<Rightarrow> tape \<Rightarrow> bool"

  where

fun tcopy_F9 :: "nat \<Rightarrow> tape \<Rightarrow> bool"

  where

fun tcopy_F10 :: "nat \<Rightarrow> tape \<Rightarrow> bool"

  where

fun tcopy_F11 :: "nat \<Rightarrow> tape \<Rightarrow> bool"

  where

fun tcopy_F12 :: "nat \<Rightarrow> tape \<Rightarrow> bool"

  where

fun tcopy_F13 :: "nat \<Rightarrow> tape \<Rightarrow> bool"

  where

fun tcopy_F14 :: "nat \<Rightarrow> tape \<Rightarrow> bool"

  where

fun tcopy_F15 :: "nat \<Rightarrow> tape \<Rightarrow> bool"

  where

text {*

  The following @{text "inv_tcopy"} is the invariant of the {\em Copying} TM.

*}

fun inv_tcopy :: "nat \<Rightarrow> t_conf \<Rightarrow> bool"

  where

  "inv_tcopy x c = (let (state, tp) = c in 

                    if state = 0 then tcopy_F0 x tp

                    else if state = 1 then tcopy_F1 x tp

                    else if state = 2 then tcopy_F2 x tp

                    else if state = 3 then tcopy_F3 x tp

                    else if state = 4 then tcopy_F4 x tp

                    else if state = 5 then tcopy_F5 x tp

                    else if state = 6 then tcopy_F6 x tp

                    else if state = 7 then tcopy_F7 x tp

                    else if state = 8 then tcopy_F8 x tp

                    else if state = 9 then tcopy_F9 x tp

                    else if state = 10 then tcopy_F10 x tp

                    else if state = 11 then tcopy_F11 x tp

                    else if state = 12 then tcopy_F12 x tp

                    else if state = 13 then tcopy_F13 x tp

                    else if state = 14 then tcopy_F14 x tp

                    else if state = 15 then tcopy_F15 x tp

                    else False)"

declare tcopy_F0.simps [simp del]

        tcopy_F1.simps [simp del]

        tcopy_F2.simps [simp del]

        tcopy_F3.simps [simp del]

        tcopy_F4.simps [simp del]

        tcopy_F5.simps [simp del]

        tcopy_F6.simps [simp del]

        tcopy_F7.simps [simp del]

        tcopy_F8.simps [simp del]

        tcopy_F9.simps [simp del]

        tcopy_F10.simps [simp del]

        tcopy_F11.simps [simp del]

        tcopy_F12.simps [simp del]

        tcopy_F13.simps [simp del]

        tcopy_F14.simps [simp del]

        tcopy_F15.simps [simp del]

done

done

lemma [elim]: "\<lbrakk>tstep (0, a, b) tcopy = (s, l, r); s \<noteq> 0\<rbrakk> \<Longrightarrow> RR"

apply(simp add: tstep.simps tcopy_def fetch.simps)

done

lemma [elim]: "\<lbrakk>tstep (Suc 0, a, b) tcopy = (s, l, r); s \<noteq> 0; s \<noteq> 2\<rbrakk>

               \<Longrightarrow> RR"

apply(simp add: tstep.simps tcopy_def fetch.simps)

apply(simp split: block.splits list.splits)

done

lemma [elim]: "\<lbrakk>tstep (2, a, b) tcopy = (s, l, r); s \<noteq> 2; s \<noteq> 3\<rbrakk>

               \<Longrightarrow> RR"

apply(simp add: tstep.simps tcopy_def fetch.simps)

apply(simp split: block.splits list.splits)

done

lemma [elim]: "\<lbrakk>tstep (3, a, b) tcopy = (s, l, r); s \<noteq> 3; s \<noteq> 4\<rbrakk> 

              \<Longrightarrow> RR"

by(simp add: tstep.simps tcopy_def fetch.simps 

        split: block.splits list.splits)

lemma [elim]: "\<lbrakk>tstep (4, a, b) tcopy = (s, l, r); s \<noteq> 4; s \<noteq> 5\<rbrakk> 

             \<Longrightarrow> RR"

by(simp add: tstep.simps tcopy_def fetch.simps 

        split: block.splits list.splits)

lemma [elim]: "\<lbrakk>tstep (5, a, b) tcopy = (s, l, r); s \<noteq> 6; s \<noteq> 11\<rbrakk> 

             \<Longrightarrow> RR"

by(simp add: tstep.simps tcopy_def fetch.simps 

        split: block.splits list.splits)

lemma [elim]: "\<lbrakk>tstep (6, a, b) tcopy = (s, l, r); s \<noteq> 6; s \<noteq> 7\<rbrakk> 

             \<Longrightarrow> RR"

by(simp add: tstep.simps tcopy_def fetch.simps 

        split: block.splits list.splits)

lemma [elim]: "\<lbrakk>tstep (7, a, b) tcopy = (s, l, r); s \<noteq> 7; s \<noteq> 8\<rbrakk> 

             \<Longrightarrow> RR"

by(simp add: tstep.simps tcopy_def fetch.simps 

        split: block.splits list.splits)

lemma [elim]: "\<lbrakk>tstep (8, a, b) tcopy = (s, l, r); s \<noteq> 8; s \<noteq> 9\<rbrakk> 

             \<Longrightarrow> RR"

by(simp add: tstep.simps tcopy_def fetch.simps 

        split: block.splits list.splits)

lemma [elim]: "\<lbrakk>tstep (9, a, b) tcopy = (s, l, r); s \<noteq> 9; s \<noteq> 10\<rbrakk> 

             \<Longrightarrow> RR"

by(simp add: tstep.simps tcopy_def fetch.simps 

        split: block.splits list.splits)

lemma [elim]: "\<lbrakk>tstep (10, a, b) tcopy = (s, l, r); s \<noteq> 10; s \<noteq> 5\<rbrakk> 

             \<Longrightarrow> RR"

by(simp add: tstep.simps tcopy_def fetch.simps 

        split: block.splits list.splits)

lemma [elim]: "\<lbrakk>tstep (11, a, b) tcopy = (s, l, r); s \<noteq> 12\<rbrakk> \<Longrightarrow> RR"

by(simp add: tstep.simps tcopy_def fetch.simps 

        split: block.splits list.splits)

lemma [elim]: "\<lbrakk>tstep (12, a, b) tcopy = (s, l, r); s \<noteq> 13; s \<noteq> 14\<rbrakk>

            \<Longrightarrow> RR"

by(simp add: tstep.simps tcopy_def fetch.simps 

        split: block.splits list.splits)

lemma [elim]: "\<lbrakk>tstep (13, a, b) tcopy = (s, l, r); s \<noteq> 12\<rbrakk> \<Longrightarrow> RR"

by(simp add: tstep.simps tcopy_def fetch.simps 

        split: block.splits list.splits)

lemma [elim]: "\<lbrakk>tstep (14, a, b) tcopy = (s, l, r); s \<noteq> 14; s \<noteq> 15\<rbrakk>  

            \<Longrightarrow> RR"

by(simp add: tstep.simps tcopy_def fetch.simps 

        split: block.splits list.splits)

lemma [elim]: "\<lbrakk>tstep (15, a, b) tcopy = (s, l, r); s \<noteq> 0; s \<noteq> 15\<rbrakk> 

            \<Longrightarrow> RR"

by(simp add: tstep.simps tcopy_def fetch.simps 

        split: block.splits list.splits)

lemma min_Suc4: "min (Suc (Suc x)) x = x"

by auto

lemma takeWhile2replicate: 

       "\<exists>n. takeWhile (\<lambda>a. a = b) list = replicate n b"

apply(induct list)

apply(rule_tac x = 0 in exI, simp)

apply(auto)

apply(rule_tac x = "Suc n" in exI, simp)

done

lemma rev_replicate_same: "rev (replicate x b) = replicate x b"

by(simp)

lemma rev_equal: "a = b \<Longrightarrow> rev a = rev b"

by simp

lemma rev_equal_rev: "rev a = rev b \<Longrightarrow> a = b"

by simp

lemma rep_suc_rev[simp]:"replicate n b @ [b] = replicate (Suc n) b"

apply(rule rev_equal_rev)

apply(simp only: rev_append rev_replicate_same)

apply(auto)

done

lemma replicate_Cons_simp: "b # replicate n b @ xs = 

                                        replicate n b @ b # xs"

apply(simp)

done

lemma [elim]: "\<lbrakk>tstep (14, b, c) tcopy = (15, ab, ba); 

                tcopy_F14 x (b, c)\<rbrakk> \<Longrightarrow> tcopy_F15 x (ab, ba)"

apply(auto simp: tstep.simps tcopy_def 

          tcopy_F14.simps tcopy_F15.simps fetch.simps new_tape.simps 

           split: if_splits list.splits block.splits)

done

lemma dropWhile_drophd: "\<not> p a \<Longrightarrow> 

      (dropWhile p xs @ (a # as)) = (dropWhile p (xs @ [a]) @ as)"

apply(induct xs)

apply(auto)

done

lemma dropWhile_append3: "\<lbrakk>\<not> p a; 

  listall ((dropWhile p xs) @ [a]) isBk\<rbrakk> \<Longrightarrow> 

               listall (dropWhile p (xs @ [a])) isBk"

apply(drule_tac p = p and xs = xs and a = a in dropWhile_drophd, simp)

done

lemma takeWhile_append3: "\<lbrakk>\<not>p a; (takeWhile p xs) = b\<rbrakk> 

                      \<Longrightarrow> takeWhile p (xs @ (a # as)) = b"

apply(drule_tac P = p and xs = xs and x = a and l = as in 

      takeWhile_tail)

apply(simp)

done

lemma listall_append: "list_all p (xs @ ys) = 

                        (list_all p xs \<and> list_all p ys)"

apply(induct xs)

apply(simp+)

done

lemma [elim]: "\<lbrakk>tstep (15, b, c) tcopy = (15, ab, ba); 

apply(auto simp: tstep.simps tcopy_F15.simps

                 tcopy_def fetch.simps new_tape.simps

done

lemma [elim]: "\<lbrakk>tstep (14, b, c) tcopy = (14, ab, ba); 

                tcopy_F14 x (b, c)\<rbrakk> \<Longrightarrow> tcopy_F14 x (ab, ba)"

apply(auto simp: tcopy_F14.simps tcopy_def tstep.simps 

                 tcopy_F14.simps fetch.simps new_tape.simps

           split: if_splits list.splits block.splits)

done

lemma [elim]: "\<lbrakk>tstep (12, b, c) tcopy = (14, ab, ba); 

                tcopy_F12 x (b, c)\<rbrakk> \<Longrightarrow> tcopy_F14 x (ab, ba)" 

apply(auto simp:tcopy_F12.simps tcopy_F14.simps 

                tcopy_def tstep.simps fetch.simps new_tape.simps 

           split: if_splits list.splits block.splits)

done

lemma [elim]: "\<lbrakk>tstep (12, b, c) tcopy = (13, ab, ba); 

                tcopy_F12 x (b, c)\<rbrakk> \<Longrightarrow> tcopy_F13 x (ab, ba)"

done

lemma [elim]: "\<lbrakk>tstep (11, b, c) tcopy = (12, ab, ba); 

                tcopy_F11 x (b, c)\<rbrakk> \<Longrightarrow> tcopy_F12 x (ab, ba)" 

apply(simp_all add:tcopy_F12.simps tcopy_F11.simps 

                   tcopy_def tstep.simps fetch.simps new_tape.simps)

apply(auto)

done

lemma [elim]: "\<lbrakk>tstep (13, b, c) tcopy = (12, ab, ba); 

                tcopy_F13 x (b, c)\<rbrakk> \<Longrightarrow> tcopy_F12 x (ab, ba)"

done

lemma [elim]: "\<lbrakk>tstep (5, b, c) tcopy = (11, ab, ba); 

apply(simp_all add:tcopy_F11.simps tcopy_F5.simps tcopy_def 

                   tstep.simps fetch.simps new_tape.simps)

apply(simp split: if_splits list.splits block.splits)

done

done

done

done

lemma [elim]: "\<lbrakk>tstep (10, b, c) tcopy = (10, ab, ba); 

                tcopy_F10 x (b, c)\<rbrakk> \<Longrightarrow> tcopy_F10 x (ab, ba)"

           split: if_splits list.splits block.splits)

done

done

done