(* 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

  "tcopy_F0 x tp = (let (ln, rn) = tp in 

           list_all isBk ln & rn = replicate x Oc 

                                   @ [Bk] @ replicate x Oc)"

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

  where

   "tcopy_F1 x (ln, rn) = (ln = [] & rn = replicate x Oc)"

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

  where

  "tcopy_F2 0 tp = False" |

  "tcopy_F2 (Suc x) (ln, rn) = (length ln > 0 & 

             ln @ rn = replicate (Suc x) Oc)"

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

  where

  "tcopy_F3 0 tp = False" |

  "tcopy_F3 (Suc x) (ln, rn) = 

            (ln = Bk # replicate (Suc x) Oc & length rn <= 1)"

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

  where

  "tcopy_F4 0 tp = False" | 

  "tcopy_F4 (Suc x) (ln, rn) = 

           ((ln = replicate x Oc & rn = [Oc, Bk, Oc])

           | (ln = replicate (Suc x) Oc & rn = [Bk, Oc])) "

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

  where

  "tcopy_F5 0 tp = False" |

  "tcopy_F5 (Suc x) (ln, rn) = 

        (if rn = [] then False 

         else if hd rn = Bk then (ln = [] & 

                   rn = Bk # (Oc # replicate (Suc x) Bk

                             @ replicate (Suc x) Oc))

         else if hd rn = Oc then 

           (\<exists>n. ln = replicate (x - n) Oc 

              & rn = Oc # (Oc # replicate n Bk @ replicate n Oc)

               & n > 0 & n <= x)

          else False)"

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

  where

  "tcopy_F6 0 tp = False" |

  "tcopy_F6 (Suc x) (ln, rn) = 

            (\<exists>n. ln = replicate (Suc x -n) Oc 

                     & tl rn = replicate n Bk @ replicate n Oc

             & n > 0 & n <= x)"

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

  where

  "tcopy_F7 0 tp = False" |

  "tcopy_F7 (Suc x) (ln, rn) = 

            (let lrn = (rev ln) @ rn in 

            (\<exists>n. lrn = replicate ((Suc x) - n) Oc @

                        replicate (Suc n) Bk @ replicate n Oc

             & n > 0 & n <= x & 

               length rn >= n & length rn <= 2 * n ))"

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

  where

  "tcopy_F8 0 tp = False" |

  "tcopy_F8 (Suc x) (ln, rn) = 

            (let lrn = (rev ln) @ rn in 

            (\<exists>n. lrn = replicate ((Suc x) - n) Oc @ 

                       replicate (Suc n) Bk @ replicate n Oc

               & n > 0 & n <= x & length rn < n)) "

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

  where

  "tcopy_F9 0 tp = False" | 

  "tcopy_F9 (Suc x) (ln, rn) =  

            (let lrn = (rev ln) @ rn in 

            (\<exists>n. lrn = replicate (Suc (Suc x) - n) Oc 

                            @ replicate n Bk @ replicate n Oc

             & n > Suc 0 & n <= Suc x & length rn > 0 

                    & length rn <= Suc n))"

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

  where

  "tcopy_F10 0 tp = False" |

  "tcopy_F10 (Suc x) (ln, rn) = 

           (let lrn = (rev ln) @ rn in 

             (\<exists>n. lrn = replicate (Suc (Suc x) - n) Oc

                   @ replicate n Bk @ replicate n Oc & n > Suc 0 

                & n <= Suc x & length rn > Suc n & 

                  length rn <= 2*n + 1 ))"

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

  where

  "tcopy_F11 0 tp = False" |

  "tcopy_F11 (Suc x) (ln, rn) = 

            (ln = [Bk] & rn = Oc # replicate (Suc x) Bk 

                              @ replicate (Suc x) Oc)"

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

  where

  "tcopy_F12 0 tp = False" |

  "tcopy_F12 (Suc x) (ln, rn) =  

           (let lrn = ((rev ln) @ rn) in

           (\<exists>n. n > 0 & n <= Suc (Suc x) 

         & lrn = Bk # replicate n Oc @ replicate (Suc (Suc x) - n) Bk

                 @ replicate (Suc x) Oc 

         & length ln = Suc n))"

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

  where

  "tcopy_F13 0 tp = False" |

  "tcopy_F13 (Suc x) (ln, rn) =  

           (let lrn = ((rev ln) @ rn) in

           (\<exists>n. n > Suc 0 & n <= Suc (Suc x) 

         & lrn = Bk # replicate n Oc @ replicate (Suc (Suc x) - n) Bk

                 @ replicate (Suc x) Oc

         & length ln = n))"

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

  where

  "tcopy_F14 0 tp = False" |

  "tcopy_F14 (Suc x) (ln, rn) = 

             (ln = replicate (Suc x) Oc @ [Bk] & 

              tl rn = replicate (Suc x) Oc)"

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

  where

  "tcopy_F15 0 tp = False" |

  "tcopy_F15 (Suc x) (ln, rn) = 

            (let lrn = ((rev ln) @ rn) in

             lrn = Bk # replicate (Suc x) Oc @ [Bk] @ 

                   replicate (Suc x) Oc & length ln <= (Suc x))"

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]

lemma list_replicate_Bk[dest]: "list_all isBk list \<Longrightarrow> 

                            list = replicate (length list) Bk"

apply(induct list)

apply(simp+)

done

lemma [simp]: "dropWhile (\<lambda> a. a = b) (replicate x b @ ys) = 

                  dropWhile (\<lambda> a. a = b) ys"

apply(induct x)

apply(simp)

apply(simp)

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(case_tac x)

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); 

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

apply(case_tac x)

apply(auto simp: tstep.simps tcopy_F15.simps

                 tcopy_def fetch.simps new_tape.simps

            split: if_splits list.splits block.splits)

apply(case_tac b, simp+)

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(case_tac x)

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 [intro]: "list_all isBk (replicate x Bk)"

apply(induct x, simp+)

done

lemma [elim]: "list_all isBk (dropWhile (\<lambda>a. a = Oc) b) \<Longrightarrow> 

               list_all isBk (dropWhile (\<lambda>a. a = Oc) (tl b))"

apply(case_tac b, auto split: if_splits)

apply(drule list_replicate_Bk)

apply(case_tac "length list", auto)

done

lemma [elim]: "list_all (\<lambda> a. a = Oc) list \<Longrightarrow> 

               list = replicate (length list) Oc"

apply(induct list)

apply(simp+)

done

lemma append_length:  "\<lbrakk>as @ bs = cs @ ds; length bs = length ds\<rbrakk>

                    \<Longrightarrow> as = cs & bs = ds"

apply(auto)

done

lemma Suc_elim: "Suc (Suc m) - n = Suc na \<Longrightarrow> Suc m - n = na"

apply(simp)

done

lemma [elim]: "\<lbrakk>0 < n; n \<le> Suc (Suc na);

  rev b @ Oc # list = 

         Bk # replicate n Oc @ replicate (Suc (Suc na) - n) Bk @ 

         Oc # replicate na Oc;

  length b = Suc n; b \<noteq> []\<rbrakk>

       \<Longrightarrow> list_all isBk (dropWhile (\<lambda>a. a = Oc) (tl b))"

apply(case_tac "rev b", auto)

done

lemma b_cons_same: "b#bs = replicate x a @ as \<Longrightarrow> a \<noteq> b \<longrightarrow> x = 0"

apply(case_tac x, simp+)

done

lemma tcopy_tmp[elim]: 

  "\<lbrakk>0 < n; n \<le> Suc (Suc na); 

  rev b @ Oc # list = 

    Bk # replicate n Oc @ replicate (Suc (Suc na) - n) Bk 

    @ Oc # replicate na Oc; length b = Suc n; b \<noteq> []\<rbrakk>

   \<Longrightarrow> list = replicate na Oc"

apply(case_tac "rev b", simp+)

apply(auto)

apply(frule b_cons_same, auto)

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(case_tac x)

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)

apply(frule tcopy_tmp, simp+)

apply(case_tac n, simp+)

apply(case_tac nata, simp+)

done

lemma replicate_app_Cons: "replicate a b @ b # replicate c b 

                        = replicate (Suc (a + c)) b"

apply(simp)

apply(simp add: replicate_app_Cons_same)

apply(simp only: replicate_add[THEN sym])

done

lemma replicate_same_exE_pref: "\<exists>x. bs @ (b # cs) = replicate x y

                            \<Longrightarrow> (\<exists>n. bs = replicate n y)"

apply(induct bs)

apply(rule_tac x = 0 in exI, simp)

apply(drule impI)

apply(erule impE)

apply(erule exE, simp+)

apply(case_tac x, auto)

apply(case_tac x, auto)

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

done

lemma replicate_same_exE_inf: "\<exists>x. bs @ (b # cs) = replicate x y \<Longrightarrow> b = y"

apply(induct bs, auto)

apply(case_tac x, auto)

apply(drule impI)

apply(erule impE)

apply(case_tac x, simp+)

done

lemma replicate_same_exE_suf: 

     "\<exists>x. bs @ (b # cs) = replicate x y \<Longrightarrow> \<exists>n. cs = replicate n y"

apply(induct bs, auto)

apply(case_tac x, simp+)

apply(drule impI, erule impE)

apply(case_tac x, simp+)

done

lemma replicate_same_exE: "\<exists>x. bs @ (b # cs) = replicate x y 

    \<Longrightarrow> (\<exists>n. bs = replicate n y) & (b = y) & (\<exists>m. cs = replicate m y)"

apply(rule conjI)

apply(drule  replicate_same_exE_pref, simp)

apply(rule conjI)

apply(drule replicate_same_exE_inf, simp)

apply(drule replicate_same_exE_suf, simp)

done

lemma replicate_same: "bs @ (b # cs) = replicate x y

    \<Longrightarrow> (\<exists>n. bs = replicate n y) & (b = y) & (\<exists>m. cs = replicate m y)"

apply(rule_tac replicate_same_exE)

apply(rule_tac x = x in exI)

apply(assumption)

done

lemma [elim]: "\<lbrakk> 0 < n; n \<le> Suc (Suc na);

    (rev ab @ Bk # list) = Bk # replicate n Oc 

   @ replicate (Suc (Suc na) - n) Bk @ Oc # replicate na Oc; ab \<noteq> []\<rbrakk>

    \<Longrightarrow> n \<le> Suc na"

apply(rule contrapos_pp, simp+)

apply(case_tac "rev ab", simp+)

apply(auto)

apply(simp only: replicate_app_Cons)

apply(drule replicate_same)

apply(auto)

done

lemma [elim]: "\<lbrakk>0 < n; n \<le> Suc (Suc na); 

   rev ab @ Bk # list = Bk # replicate n Oc @ 

    replicate (Suc (Suc na) - n) Bk @ Oc # replicate na Oc; 

   length ab = Suc n; ab \<noteq> []\<rbrakk>

    \<Longrightarrow> rev ab @ Oc # list = Bk # Oc # replicate n Oc @ 

               replicate (Suc na - n) Bk @ Oc # replicate na Oc"

apply(case_tac "rev ab", simp+)

apply(auto)

apply(simp only: replicate_Cons_simp)

apply(simp)

apply(case_tac "Suc (Suc na) - n", simp+)

done

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

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

apply(case_tac x)

apply(simp_all add:tcopy_F12.simps tcopy_F13.simps 

                   tcopy_def tstep.simps fetch.simps new_tape.simps)

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