diff -r cbb4ac6c8081 -r 1ce04eb1c8ad utm/uncomputable.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/utm/uncomputable.thy	Sat Sep 29 12:38:12 2012 +0000
@@ -0,0 +1,1693 @@
+(* 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)
+apply(auto)
+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(case_tac x)
+apply(simp_all add:tcopy_F12.simps tcopy_F11.simps 
+                   tcopy_def tstep.simps fetch.simps new_tape.simps)
+apply(auto)
+done
+
+lemma equal_length: "a = b \<Longrightarrow> length a = length b"
+by(simp)
+
+lemma [elim]: "\<lbrakk>tstep (13, b, c) tcopy = (12, ab, ba); 
+                tcopy_F13 x (b, c)\<rbrakk> \<Longrightarrow> tcopy_F12 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)
+apply(auto)
+apply(drule equal_length, simp)
+done
+
+lemma [elim]: "\<lbrakk>tstep (5, b, c) tcopy = (11, ab, ba); 
+                tcopy_F5 x (b, c)\<rbrakk> \<Longrightarrow> tcopy_F11 x (ab, ba)" 
+apply(case_tac x)
+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
+
+lemma less_equal: "\<lbrakk>length xs <= b; \<not> Suc (length xs) <= b\<rbrakk> \<Longrightarrow> 
+                   length xs = b"
+apply(simp)
+done
+
+lemma length_cons_same: "\<lbrakk>xs @ b # ys = as @ bs; 
+                 length ys = length bs\<rbrakk> \<Longrightarrow> xs @ [b] = as & ys = bs"
+apply(drule rev_equal)
+apply(simp)
+apply(auto)
+apply(drule rev_equal, simp)
+done
+
+lemma replicate_set_equal: "\<lbrakk> xs @ [a] = replicate n b; a \<noteq> b\<rbrakk> \<Longrightarrow> RR"
+apply(drule rev_equal, simp)
+apply(case_tac n, simp+)
+done
+
+lemma [elim]: "\<lbrakk>tstep (10, b, c) tcopy = (10, ab, ba); 
+                tcopy_F10 x (b, c)\<rbrakk> \<Longrightarrow> tcopy_F10 x (ab, ba)"
+apply(case_tac x)
+apply(auto simp:tcopy_F10.simps tcopy_def tstep.simps fetch.simps 
+                new_tape.simps
+           split: if_splits list.splits block.splits)
+apply(rule_tac x = n in exI, auto)
+apply(case_tac b, simp+)
+apply(rule contrapos_pp, simp+)
+apply(frule less_equal, simp+)
+apply(drule length_cons_same, auto)
+apply(drule replicate_set_equal, simp+)
+done
+
+lemma less_equal2: "\<not> (n::nat) \<le> m \<Longrightarrow> \<exists>x. n = x + m & x > 0"
+apply(rule_tac x = "n - m" in exI)
+apply(auto)
+done
+
+lemma replicate_tail_length[dest]:
+    "\<lbrakk>rev b @ Bk # list = xs @ replicate n Bk @ replicate n Oc\<rbrakk> 
+ \<Longrightarrow> length list >= n"
+apply(rule contrapos_pp, simp+)
+apply(drule less_equal2, auto)
+apply(drule rev_equal)
+apply(simp add: replicate_add)
+apply(auto)
+apply(case_tac x, simp+)
+done
+
+
+lemma [elim]: "\<lbrakk>tstep (9, b, c) tcopy = (10, ab, ba); 
+                tcopy_F9 x (b, c)\<rbrakk> \<Longrightarrow> tcopy_F10 x (ab, ba)" 
+apply(case_tac x)
+apply(auto simp:tcopy_F10.simps tcopy_F9.simps tcopy_def
+                tstep.simps fetch.simps new_tape.simps 
+           split: if_splits list.splits block.splits)
+apply(rule_tac x = n in exI, auto)
+apply(case_tac b, simp+)
+done
+
+lemma [elim]: "\<lbrakk>tstep (9, b, c) tcopy = (9, ab, ba); 
+                tcopy_F9 x (b, c)\<rbrakk> \<Longrightarrow> tcopy_F9 x (ab, ba)"
+apply(case_tac x)
+apply(simp_all add: tcopy_F9.simps tcopy_def 
+                    tstep.simps fetch.simps new_tape.simps 
+  split: if_splits list.splits block.splits)
+apply(rule_tac x = n in exI, auto)
+apply(case_tac b, simp+)
+apply(rule contrapos_pp, simp+)
+apply(drule less_equal, simp+)
+apply(drule rev_equal, auto)
+apply(case_tac "length list", simp+)
+done
+
+lemma app_cons_app_simp: "xs @ a # bs @ ys = (xs @ [a]) @ bs @ ys"
+apply(simp)
+done
+
+lemma [elim]: "\<lbrakk>tstep (8, b, c) tcopy = (9, ab, ba); 
+                tcopy_F8 x (b, c)\<rbrakk> \<Longrightarrow> tcopy_F9 x (ab, ba)" 
+apply(case_tac x)
+apply(auto simp:tcopy_F8.simps tcopy_F9.simps tcopy_def 
+                tstep.simps fetch.simps new_tape.simps
+  split: if_splits list.splits block.splits)
+apply(rule_tac x = "Suc n" in exI, auto)
+apply(rule_tac x = "n" in exI, auto)
+apply(simp only: app_cons_app_simp)
+apply(frule replicate_tail_length, simp)
+done
+
+lemma [elim]: "\<lbrakk>tstep (8, b, c) tcopy = (8, ab, ba); 
+                tcopy_F8 x (b, c)\<rbrakk> \<Longrightarrow> tcopy_F8 x (ab, ba)"
+apply(case_tac x)
+apply(simp_all add:tcopy_F8.simps tcopy_def tstep.simps 
+                   fetch.simps new_tape.simps)
+apply(simp split: if_splits list.splits block.splits)
+apply(rule_tac x = "n" in exI, auto)
+done
+
+lemma ex_less_more: "\<lbrakk>(x::nat) >= m ; x <= n\<rbrakk> \<Longrightarrow> 
+                        \<exists>y. x = m + y & y <= n - m"
+by(rule_tac x = "x -m" in exI, auto)
+
+lemma replicate_split: "x <= n \<Longrightarrow> 
+                      (\<exists>y. replicate n b = replicate (y + x) b)"
+apply(rule_tac x = "n - x" in exI)
+apply(simp)
+done
+
+lemma app_app_app_app_simp: "as @ bs @ cs @ ds = 
+                             (as @ bs) @ (cs @ ds)"
+by simp
+
+lemma lengthtailsame_append_elim: 
+     "\<lbrakk>as @ bs = cs @ ds; length bs = length ds\<rbrakk> \<Longrightarrow> bs = ds"
+apply(simp)
+done
+
+lemma rep_suc: "replicate (Suc n) x = replicate n x @ [x]" 
+by(induct n, auto)
+
+lemma length_append_diff_cons: 
+ "\<lbrakk>b @ x # ba = xs @ replicate m y @ replicate n x; x \<noteq> y; 
+   Suc (length ba) \<le> m + n\<rbrakk>
+  \<Longrightarrow> length ba < n"
+apply(induct n arbitrary: ba, simp)
+apply(drule_tac b = y in replicate_split,
+      simp add: replicate_add, erule exE, simp del: replicate.simps)
+proof -
+  fix ba ya
+  assume h1: 
+     "b @ x # ba = xs @ y # replicate ya y @ replicate (length ba) y" 
+    and h2: "x \<noteq> y"
+  thus "False"  
+    using append_eq_append_conv[of "b @ [x]" 
+            "xs @ y # replicate ya y" "ba" "replicate (length ba) y"]
+    apply(auto)
+    apply(case_tac ya, simp, 
+           simp add: rep_suc del: rep_suc_rev replicate.simps)
+    done
+next
+  fix n ba
+  assume ind: "\<And>ba. \<lbrakk>b @ x # ba = xs @ replicate m y @ replicate n x;
+                      x \<noteq> y; Suc (length ba) \<le> m + n\<rbrakk> 
+                 \<Longrightarrow> length ba < n"
+    and h1: "b @ x # ba = xs @ replicate m y @ replicate (Suc n) x" 
+    and h2: "x \<noteq> y" and h3: "Suc (length ba) \<le> m + Suc n"
+  show "length ba < Suc n"
+  proof(cases "length ba")
+    case 0 thus "?thesis" by simp
+  next
+    fix nat
+    assume "length ba = Suc nat"
+    hence "\<exists> ys a. ba = ys @ [a]"
+      apply(rule_tac x = "butlast ba" in exI)
+      apply(rule_tac x = "last ba" in exI)
+      using append_butlast_last_id[of ba]
+      apply(case_tac ba, auto)
+      done
+    from this obtain ys where "\<exists> a. ba = ys @ [a]" ..
+    from this obtain a where "ba = ys @ [a]" ..
+    thus "?thesis"
+      using ind[of ys] h1 h2 h3
+      apply(simp del: rep_suc_rev replicate.simps add: rep_suc)
+      done
+  qed
+qed
+      
+lemma [elim]: 
+  "\<lbrakk>b @ Oc # ba = xs @ Bk # replicate n Bk @ replicate n Oc;  
+   Suc (length ba) \<le> 2 * n\<rbrakk>
+  \<Longrightarrow> length ba < n"
+  apply(rule_tac length_append_diff_cons[of b Oc ba xs "Suc n" Bk n])
+  apply(simp, simp, simp)
+  done
+
+lemma [elim]: "\<lbrakk>tstep (7, b, c) tcopy = (8, ab, ba); 
+                tcopy_F7 x (b, c)\<rbrakk> \<Longrightarrow> tcopy_F8 x (ab, ba)" 
+apply(case_tac x)
+apply(simp_all add:tcopy_F8.simps tcopy_F7.simps 
+                   tcopy_def tstep.simps fetch.simps new_tape.simps)
+apply(simp split: if_splits list.splits block.splits)
+apply(rule_tac x = "n" in exI, auto)
+done
+
+lemma [elim]: "\<lbrakk>tstep (7, b, c) tcopy = (7, ab, ba); 
+                tcopy_F7 x (b, c)\<rbrakk> \<Longrightarrow> tcopy_F7 x (ab, ba)"
+apply(case_tac x)
+apply(auto simp:tcopy_F7.simps tcopy_def tstep.simps 
+                fetch.simps new_tape.simps
+  split: if_splits list.splits block.splits)
+apply(rule_tac x = "n" in exI, auto)
+apply(simp only: app_cons_app_simp)
+apply(frule replicate_tail_length, simp)
+done
+
+lemma Suc_more: "n <= m \<Longrightarrow> Suc m - n = Suc (m - n)"
+by simp
+
+lemma [elim]: "\<lbrakk>tstep (6, b, c) tcopy = (7, ab, ba); 
+                tcopy_F6 x (b, c)\<rbrakk> \<Longrightarrow> tcopy_F7 x (ab, ba)" 
+apply(case_tac x)
+apply(auto simp:tcopy_F7.simps tcopy_F6.simps 
+                tcopy_def tstep.simps fetch.simps new_tape.simps
+  split: if_splits list.splits block.splits)
+done
+
+lemma [elim]: "\<lbrakk>tstep (6, b, c) tcopy = (6, ab, ba); 
+                tcopy_F6 x (b, c)\<rbrakk> \<Longrightarrow> tcopy_F6 x (ab, ba)"
+apply(case_tac x)
+apply(auto simp:tcopy_F6.simps tcopy_def tstep.simps 
+                new_tape.simps fetch.simps
+  split: if_splits list.splits block.splits)
+done
+
+lemma [elim]: "\<lbrakk>tstep (5, b, c) tcopy = (6, ab, ba); 
+                tcopy_F5 x (b, c)\<rbrakk> \<Longrightarrow> tcopy_F6 x (ab, ba)" 
+apply(case_tac x)
+apply(auto simp:tcopy_F5.simps tcopy_F6.simps tcopy_def 
+                tstep.simps fetch.simps new_tape.simps 
+  split: if_splits list.splits block.splits)
+apply(rule_tac x = n in exI, simp)
+apply(rule_tac x = n in exI, simp)
+apply(drule Suc_more, simp)
+done
+
+lemma ex_less_more2: "\<lbrakk>(n::nat) < x ; x <= 2 * n\<rbrakk> \<Longrightarrow> 
+                               \<exists>y. (x = n + y & y <= n)"
+apply(rule_tac x = "x - n" in exI)
+apply(auto)
+done
+
+lemma app_app_app_simp: "xs @ ys @ za = (xs @ ys) @ za"
+apply(simp)
+done
+
+lemma [elim]: "rev xs = replicate n b \<Longrightarrow> xs = replicate n b"
+using rev_replicate[of n b]
+thm rev_equal
+by(drule_tac rev_equal, simp)
+
+lemma app_cons_tail_same[dest]: 
+  "\<lbrakk>rev b @ Oc # list = 
+    replicate (Suc (Suc na) - n) Oc @ replicate n Bk @ replicate n Oc;
+  Suc 0 < n; n \<le> Suc na; n < length list; length list \<le> 2 * n; b \<noteq> []\<rbrakk>
+  \<Longrightarrow> list = replicate n Bk @ replicate n Oc 
+           & b = replicate (Suc na - n) Oc"
+using length_append_diff_cons[of "rev b" Oc list 
+                "replicate (Suc (Suc na) - n) Oc" n Bk n]
+apply(case_tac "length list = 2*n", simp)
+using append_eq_append_conv[of "rev b @ [Oc]" "replicate 
+      (Suc (Suc na) - n) Oc" "list" "replicate n Bk @ replicate n Oc"]
+apply(case_tac n, simp, simp add: Suc_more rep_suc 
+                             del: rep_suc_rev replicate.simps, auto)
+done
+
+lemma hd_replicate_false1: "\<lbrakk>replicate x Oc \<noteq> [];
+                             hd (replicate x Oc) = Bk\<rbrakk> \<Longrightarrow> RR"
+apply(case_tac x, auto)
+done
+
+lemma hd_replicate_false2: "\<lbrakk>replicate x Oc \<noteq> [];
+                            hd (replicate x Oc) \<noteq> Oc\<rbrakk> \<Longrightarrow> RR"
+apply(case_tac x, auto)
+done
+
+lemma Suc_more_less: "\<lbrakk>n \<le> Suc m; n >= m\<rbrakk> \<Longrightarrow> n = m | n = Suc m"
+apply(auto)
+done
+
+lemma replicate_not_Nil: "replicate x a \<noteq> [] \<Longrightarrow> x > 0"
+apply(case_tac x, simp+)
+done
+
+lemma [elim]: "\<lbrakk>tstep (10, b, c) tcopy = (5, ab, ba); 
+                tcopy_F10 x (b, c)\<rbrakk> \<Longrightarrow> tcopy_F5 x (ab, ba)"
+apply(case_tac x)
+apply(auto simp:tcopy_F5.simps tcopy_F10.simps tcopy_def 
+                tstep.simps fetch.simps new_tape.simps
+           split: if_splits list.splits block.splits)
+apply(frule app_cons_tail_same, simp+)
+apply(rule_tac x = n in exI, auto)
+done
+
+lemma [elim]: "\<lbrakk>tstep (4, b, c) tcopy = (5, ab, ba); 
+                tcopy_F4 x (b, c)\<rbrakk> \<Longrightarrow> tcopy_F5 x (ab, ba)" 
+apply(case_tac x)
+apply(auto simp:tcopy_F5.simps tcopy_F4.simps tcopy_def 
+                tstep.simps fetch.simps new_tape.simps
+           split: if_splits list.splits block.splits)
+done
+
+lemma [elim]: "\<lbrakk>tstep (3, b, c) tcopy = (4, ab, ba); 
+                tcopy_F3 x (b, c)\<rbrakk> \<Longrightarrow> tcopy_F4 x (ab, ba)"
+apply(case_tac x)
+apply(auto simp:tcopy_F3.simps tcopy_F4.simps 
+                tcopy_def tstep.simps fetch.simps new_tape.simps
+           split: if_splits list.splits block.splits)
+done
+
+lemma [elim]: "\<lbrakk>tstep (4, b, c) tcopy = (4, ab, ba);
+                tcopy_F4 x (b, c)\<rbrakk> \<Longrightarrow> tcopy_F4 x (ab, ba)" 
+apply(case_tac x)
+apply(auto simp:tcopy_F3.simps tcopy_F4.simps 
+                tcopy_def tstep.simps fetch.simps new_tape.simps
+  split: if_splits list.splits block.splits)
+done
+
+lemma [elim]: "\<lbrakk>tstep (3, b, c) tcopy = (3, ab, ba); 
+                tcopy_F3 x (b, c)\<rbrakk> \<Longrightarrow> tcopy_F3 x (ab, ba)"
+apply(case_tac x)
+apply(auto simp:tcopy_F3.simps tcopy_F4.simps 
+                tcopy_def tstep.simps fetch.simps new_tape.simps 
+  split: if_splits list.splits block.splits)
+done
+
+lemma replicate_cons_back: "y # replicate x y = replicate (Suc x) y"
+apply(simp)
+done
+
+lemma replicate_cons_same: "bs @ (b # cs) = y # replicate x y \<Longrightarrow> 
+        (\<exists>n. bs = replicate n y) & (b = y) & (\<exists>m. cs = replicate m y)"
+apply(simp only: replicate_cons_back)
+apply(drule_tac replicate_same)
+apply(simp)
+done
+
+lemma [elim]: "\<lbrakk>tstep (2, b, c) tcopy = (3, ab, ba); 
+                tcopy_F2 x (b, c)\<rbrakk> \<Longrightarrow> tcopy_F3 x (ab, ba)" 
+apply(case_tac x)
+apply(auto simp:tcopy_F3.simps tcopy_F2.simps 
+                tcopy_def tstep.simps fetch.simps new_tape.simps
+  split: if_splits list.splits block.splits)
+apply(drule replicate_cons_same, auto)+
+done
+
+lemma [elim]: "\<lbrakk>tstep (2, b, c) tcopy = (2, ab, ba); 
+                tcopy_F2 x (b, c)\<rbrakk> \<Longrightarrow> tcopy_F2 x (ab, ba)"
+apply(case_tac x)
+apply(auto simp:tcopy_F3.simps tcopy_F2.simps 
+                tcopy_def tstep.simps fetch.simps new_tape.simps
+  split: if_splits list.splits block.splits)
+apply(frule replicate_cons_same, auto)
+apply(simp add: replicate_app_Cons_same)
+done
+
+lemma [elim]: "\<lbrakk>tstep (Suc 0, b, c) tcopy = (2, ab, ba); 
+                tcopy_F1 x (b, c)\<rbrakk> \<Longrightarrow> tcopy_F2 x (ab, ba)" 
+apply(case_tac x)
+apply(simp_all add:tcopy_F2.simps tcopy_F1.simps 
+                   tcopy_def tstep.simps fetch.simps new_tape.simps)
+apply(auto)
+done
+
+lemma [elim]: "\<lbrakk>tstep (Suc 0, b, c) tcopy = (0, ab, ba); 
+                tcopy_F1 x (b, c)\<rbrakk> \<Longrightarrow> tcopy_F0 x (ab, ba)"
+apply(case_tac x)
+apply(simp_all add:tcopy_F0.simps tcopy_F1.simps 
+                   tcopy_def tstep.simps fetch.simps new_tape.simps)
+done
+
+lemma ex_less: "Suc x <= y \<Longrightarrow> \<exists>z. y = x + z & z > 0"
+apply(rule_tac x = "y - x" in exI, auto)
+done
+
+lemma [elim]: "\<lbrakk>xs @ Bk # ba = 
+  Bk # Oc # replicate n Oc @ Bk # Oc # replicate n Oc; 
+  length xs \<le> Suc n; xs \<noteq> []\<rbrakk> \<Longrightarrow> RR"
+apply(case_tac xs, auto)
+apply(case_tac list, auto)
+apply(drule ex_less, auto)
+apply(simp add: replicate_add)
+apply(auto)
+apply(case_tac z, simp+)
+done
+
+lemma [elim]: "\<lbrakk>tstep (15, b, c) tcopy = (0, ab, ba); 
+                tcopy_F15 x (b, c)\<rbrakk> \<Longrightarrow> tcopy_F0 x (ab, ba)"
+apply(case_tac x)
+apply(auto simp: tcopy_F15.simps tcopy_F0.simps 
+                 tcopy_def tstep.simps new_tape.simps fetch.simps
+           split: if_splits list.splits block.splits)
+done
+
+lemma [elim]: "\<lbrakk>tstep (0, b, c) tcopy = (0, ab, ba); 
+                tcopy_F0 x (b, c)\<rbrakk> \<Longrightarrow> tcopy_F0 x (ab, ba)" 
+apply(case_tac x)
+apply(simp_all add: tcopy_F0.simps tcopy_def 
+                    tstep.simps new_tape.simps fetch.simps)
+done
+
+declare tstep.simps[simp del]
+
+text {*
+  Finally establishes the invariant of Copying TM, which is used to dervie 
+  the parital correctness of Copying TM.
+*}
+lemma inv_tcopy_step:"inv_tcopy x c \<Longrightarrow> inv_tcopy x (tstep c tcopy)"
+apply(induct c)
+apply(auto split: if_splits block.splits list.splits taction.splits)
+apply(auto simp: tstep.simps tcopy_def fetch.simps new_tape.simps 
+  split: if_splits list.splits block.splits taction.splits)
+done
+
+declare inv_tcopy.simps[simp del]
+
+text {*
+  Invariant under mult-step execution.
+  *}
+lemma inv_tcopy_steps: 
+  "inv_tcopy x (steps (Suc 0, [], replicate x Oc) tcopy stp) "
+apply(induct stp)
+apply(simp add: tstep.simps tcopy_def steps.simps 
+                tcopy_F1.simps inv_tcopy.simps)
+apply(drule_tac inv_tcopy_step, simp add: tstep_red)
+done
+  
+
+text {*
+  The followng lemmas gives the parital correctness of Copying TM.
+*}
+theorem inv_tcopy_rs: 
+  "steps (Suc 0, [], replicate x Oc) tcopy stp = (0, l, r)
+  \<Longrightarrow> \<exists> n. l = replicate n Bk \<and> 
+           r = replicate x Oc @ Bk # replicate x Oc"
+apply(insert inv_tcopy_steps[of x stp])
+apply(auto simp: inv_tcopy.simps tcopy_F0.simps isBk.simps)
+done
+
+
+
+
+(*----------halt problem of tcopy----------------------------------------*)
+
+section {*
+  The following definitions are used to construct the measure function used to show
+  the termnation of Copying TM.
+*}
+
+definition lex_pair :: "((nat \<times> nat) \<times> nat \<times> nat) set"
+  where
+  "lex_pair \<equiv> less_than <*lex*> less_than"
+
+definition lex_triple :: 
+ "((nat \<times> (nat \<times> nat)) \<times> (nat \<times> (nat \<times> nat))) set"
+  where
+"lex_triple \<equiv> less_than <*lex*> lex_pair"
+
+definition lex_square :: 
+  "((nat \<times> nat \<times> nat \<times> nat) \<times> (nat \<times> nat \<times> nat \<times> nat)) set"
+  where
+"lex_square \<equiv> less_than <*lex*> lex_triple"
+
+lemma wf_lex_triple: "wf lex_triple"
+  by (auto intro:wf_lex_prod simp:lex_triple_def lex_pair_def)
+
+lemma wf_lex_square: "wf lex_square"
+  by (auto intro:wf_lex_prod 
+           simp:lex_triple_def lex_square_def lex_pair_def)
+
+text {*
+  A measurement functions used to show the termination of copying machine:
+*}
+fun tcopy_phase :: "t_conf \<Rightarrow> nat"
+  where
+  "tcopy_phase c = (let (state, tp) = c in
+                    if state > 0 & state <= 4 then 5
+                    else if state >=5 & state <= 10 then 4
+                    else if state = 11 then 3
+                    else if state = 12 | state = 13 then 2
+                    else if state = 14 | state = 15 then 1
+                    else 0)" 
+
+fun tcopy_phase4_stage :: "tape \<Rightarrow> nat"
+  where
+  "tcopy_phase4_stage (ln, rn) = 
+                   (let lrn = (rev ln) @ rn 
+                    in length (takeWhile (\<lambda>a. a = Oc) lrn))"
+
+fun tcopy_stage :: "t_conf \<Rightarrow> nat"
+  where
+  "tcopy_stage c = (let (state, ln, rn) = c in 
+                    if tcopy_phase c = 5 then 0
+                    else if tcopy_phase c = 4 then 
+                               tcopy_phase4_stage (ln, rn)
+                    else if tcopy_phase c = 3 then 0
+                    else if tcopy_phase c = 2 then length rn
+                    else if tcopy_phase c = 1 then 0
+                    else 0)"
+
+fun tcopy_phase4_state :: "t_conf \<Rightarrow> nat"
+  where
+  "tcopy_phase4_state c = (let (state, ln, rn) = c in
+                           if state = 6 & hd rn = Oc then 0
+                           else if state = 5 then 1
+                           else 12 - state)"
+
+fun tcopy_state :: "t_conf \<Rightarrow> nat"
+  where
+  "tcopy_state c = (let (state, ln, rn) = c in
+                    if tcopy_phase c = 5 then 4 - state
+                    else if tcopy_phase c = 4 then 
+                         tcopy_phase4_state c
+                    else if tcopy_phase c = 3 then 0
+                    else if tcopy_phase c = 2 then 13 - state
+                    else if tcopy_phase c = 1 then 15 - state
+                    else 0)"
+
+fun tcopy_step2 :: "t_conf \<Rightarrow> nat"
+  where
+  "tcopy_step2 (s, l, r) = length r"
+
+fun tcopy_step3 :: "t_conf \<Rightarrow> nat"
+  where
+  "tcopy_step3 (s, l, r) = (if r = [] | r = [Bk] then Suc 0 else 0)"
+
+fun tcopy_step4 :: "t_conf \<Rightarrow> nat"
+  where
+  "tcopy_step4 (s, l, r) = length l"
+
+fun tcopy_step7 :: "t_conf \<Rightarrow> nat"
+  where
+  "tcopy_step7 (s, l, r) = length r"
+
+fun tcopy_step8 :: "t_conf \<Rightarrow> nat"
+  where
+  "tcopy_step8 (s, l, r) = length r"
+
+fun tcopy_step9 :: "t_conf \<Rightarrow> nat"
+  where
+  "tcopy_step9 (s, l, r) = length l"
+
+fun tcopy_step10 :: "t_conf \<Rightarrow> nat"
+  where
+  "tcopy_step10 (s, l, r) = length l"
+
+fun tcopy_step14 :: "t_conf \<Rightarrow> nat"
+  where
+  "tcopy_step14 (s, l, r) = (case hd r of 
+                            Oc \<Rightarrow> 1 |
+                            Bk    \<Rightarrow> 0)"
+
+fun tcopy_step15 :: "t_conf \<Rightarrow> nat"
+  where
+  "tcopy_step15 (s, l, r) = length l"
+
+fun tcopy_step :: "t_conf \<Rightarrow> nat"
+  where
+  "tcopy_step c = (let (state, ln, rn) = c in
+             if state = 0 | state = 1 | state = 11 | 
+                state = 5 | state = 6 | state = 12 | state = 13 then 0
+                   else if state = 2 then tcopy_step2 c
+                   else if state = 3 then tcopy_step3 c
+                   else if state = 4 then tcopy_step4 c
+                   else if state = 7 then tcopy_step7 c
+                   else if state = 8 then tcopy_step8 c
+                   else if state = 9 then tcopy_step9 c
+                   else if state = 10 then tcopy_step10 c
+                   else if state = 14 then tcopy_step14 c
+                   else if state = 15 then tcopy_step15 c
+                   else 0)"
+
+text {*
+  The measure function used to show the termination of Copying TM.
+*}
+fun tcopy_measure :: "t_conf \<Rightarrow> (nat * nat * nat * nat)"
+  where
+  "tcopy_measure c = 
+   (tcopy_phase c, tcopy_stage c, tcopy_state c, tcopy_step c)"
+
+definition tcopy_LE :: "((nat \<times> block list \<times> block list) \<times> 
+                        (nat \<times> block list \<times> block list)) set"
+  where
+   "tcopy_LE \<equiv> (inv_image lex_square tcopy_measure)"
+
+lemma wf_tcopy_le: "wf tcopy_LE"
+by(auto intro:wf_inv_image wf_lex_square simp:tcopy_LE_def)
+
+
+declare steps.simps[simp del] 
+
+declare tcopy_phase.simps[simp del] tcopy_stage.simps[simp del] 
+        tcopy_state.simps[simp del] tcopy_step.simps[simp del] 
+        inv_tcopy.simps[simp del]
+declare tcopy_F0.simps [simp]
+        tcopy_F1.simps [simp]
+        tcopy_F2.simps [simp]
+        tcopy_F3.simps [simp]
+        tcopy_F4.simps [simp]
+        tcopy_F5.simps [simp]
+        tcopy_F6.simps [simp]
+        tcopy_F7.simps [simp]
+        tcopy_F8.simps [simp]
+        tcopy_F9.simps [simp]
+        tcopy_F10.simps [simp]
+        tcopy_F11.simps [simp]
+        tcopy_F12.simps [simp]
+        tcopy_F13.simps [simp]
+        tcopy_F14.simps [simp]
+        tcopy_F15.simps [simp]
+        fetch.simps[simp]
+        new_tape.simps[simp]
+lemma [elim]: "tcopy_F1 x (b, c) \<Longrightarrow> 
+              (tstep (Suc 0, b, c) tcopy, Suc 0, b, c) \<in> tcopy_LE"
+apply(simp add: tcopy_F1.simps tstep.simps tcopy_def tcopy_LE_def 
+  lex_square_def lex_triple_def lex_pair_def tcopy_phase.simps 
+  tcopy_stage.simps tcopy_state.simps tcopy_step.simps)
+apply(simp split: if_splits list.splits block.splits taction.splits)
+done
+
+lemma [elim]: "tcopy_F2 x (b, c) \<Longrightarrow> 
+              (tstep (2, b, c) tcopy, 2, b, c) \<in> tcopy_LE"
+apply(simp add:tstep.simps tcopy_def tcopy_LE_def lex_square_def 
+  lex_triple_def lex_pair_def tcopy_phase.simps tcopy_stage.simps 
+  tcopy_state.simps tcopy_step.simps)
+apply(simp split: if_splits list.splits block.splits taction.splits)
+done
+
+lemma [elim]: "tcopy_F3 x (b, c) \<Longrightarrow> 
+             (tstep (3, b, c) tcopy, 3, b, c) \<in> tcopy_LE"
+apply(simp add: tstep.simps tcopy_def tcopy_LE_def lex_square_def 
+ lex_triple_def lex_pair_def tcopy_phase.simps tcopy_stage.simps 
+ tcopy_state.simps tcopy_step.simps)
+apply(simp split: if_splits list.splits block.splits taction.splits)
+apply(auto)
+apply(case_tac x, simp+)
+done
+
+lemma [elim]: "tcopy_F4 x (b, c) \<Longrightarrow> 
+            (tstep (4, b, c) tcopy, 4, b, c) \<in> tcopy_LE"
+apply(case_tac x, simp)
+apply(simp add: tcopy_F4.simps tstep.simps tcopy_def tcopy_LE_def 
+ lex_square_def lex_triple_def lex_pair_def tcopy_phase.simps 
+ tcopy_stage.simps tcopy_state.simps tcopy_step.simps)
+apply(simp split: if_splits list.splits block.splits taction.splits)
+apply(auto)
+done
+
+lemma[simp]: "takeWhile (\<lambda>a. a = b) (replicate x b @ ys) = 
+             replicate x b @ (takeWhile (\<lambda>a. a = b) ys)"
+apply(induct x)
+apply(simp+)
+done
+
+lemma [elim]: "tcopy_F5 x (b, c) \<Longrightarrow> 
+              (tstep (5, b, c) tcopy, 5, b, c) \<in> tcopy_LE"
+apply(case_tac x, simp)
+apply(simp add: tstep.simps tcopy_def tcopy_LE_def 
+        lex_square_def lex_triple_def lex_pair_def tcopy_phase.simps)
+apply(simp split: if_splits list.splits block.splits taction.splits)
+apply(auto)
+apply(simp_all add: tcopy_phase.simps 
+                    tcopy_stage.simps tcopy_state.simps)
+done
+
+lemma [elim]: "\<lbrakk>replicate n x = []; n > 0\<rbrakk> \<Longrightarrow> RR"
+apply(case_tac n, simp+)
+done
+
+lemma [elim]: "tcopy_F6 x (b, c) \<Longrightarrow> 
+              (tstep (6, b, c) tcopy, 6, b, c) \<in> tcopy_LE"
+apply(case_tac x, simp)
+apply(simp add: tstep.simps tcopy_def tcopy_LE_def 
+                lex_square_def lex_triple_def lex_pair_def 
+                tcopy_phase.simps)
+apply(simp split: if_splits list.splits block.splits taction.splits)
+apply(auto)
+apply(simp_all add: tcopy_phase.simps tcopy_stage.simps 
+                    tcopy_state.simps tcopy_step.simps)
+done
+
+lemma [elim]: "tcopy_F7 x (b, c) \<Longrightarrow> 
+             (tstep (7, b, c) tcopy, 7, b, c) \<in> tcopy_LE"
+apply(case_tac x, simp)
+apply(simp add: tstep.simps tcopy_def tcopy_LE_def lex_square_def 
+                lex_triple_def lex_pair_def tcopy_phase.simps)
+apply(simp split: if_splits list.splits block.splits taction.splits)
+apply(auto)
+apply(simp_all add: tcopy_phase.simps tcopy_stage.simps 
+                    tcopy_state.simps tcopy_step.simps)
+done
+
+lemma [elim]: "tcopy_F8 x (b, c) \<Longrightarrow> 
+              (tstep (8, b, c) tcopy, 8, b, c) \<in> tcopy_LE"
+apply(case_tac x, simp)
+apply(simp add: tstep.simps tcopy_def tcopy_LE_def lex_square_def 
+                lex_triple_def lex_pair_def tcopy_phase.simps)
+apply(simp split: if_splits list.splits block.splits taction.splits)
+apply(auto)
+apply(simp_all add: tcopy_phase.simps tcopy_stage.simps 
+                    tcopy_state.simps tcopy_step.simps)
+apply(simp only: app_cons_app_simp, frule replicate_tail_length, simp)
+done
+
+lemma app_app_app_equal: "xs @ ys @ zs = (xs @ ys) @ zs"
+by simp
+
+lemma append_cons_assoc: "as @ b # bs = (as @ [b]) @ bs"
+apply(rule rev_equal_rev)
+apply(simp)
+done
+
+lemma rev_tl_hd_merge: "bs \<noteq> [] \<Longrightarrow> 
+                        rev (tl bs) @ hd bs # as = rev bs @ as"
+apply(rule rev_equal_rev)
+apply(simp)
+done
+
+lemma [elim]: "tcopy_F9 x (b, c) \<Longrightarrow> 
+                      (tstep (9, b, c) tcopy, 9, b, c) \<in> tcopy_LE"
+apply(case_tac x, simp)
+apply(simp add: tstep.simps tcopy_def tcopy_LE_def lex_square_def 
+                lex_triple_def lex_pair_def tcopy_phase.simps)
+apply(simp split: if_splits list.splits block.splits taction.splits)
+apply(auto)
+apply(simp_all add: tcopy_phase.simps tcopy_stage.simps 
+                    tcopy_state.simps tcopy_step.simps)
+apply(drule_tac bs = b and as = "Bk # list" in rev_tl_hd_merge)
+apply(simp)
+apply(drule_tac bs = b and as = "Oc # list" in rev_tl_hd_merge)
+apply(simp)
+done
+
+lemma [elim]: "tcopy_F10 x (b, c) \<Longrightarrow> 
+              (tstep (10, b, c) tcopy, 10, b, c) \<in> tcopy_LE"
+apply(case_tac x, simp)
+apply(simp add: tstep.simps tcopy_def tcopy_LE_def lex_square_def 
+                lex_triple_def lex_pair_def tcopy_phase.simps)
+apply(simp split: if_splits list.splits block.splits taction.splits)
+apply(auto)
+apply(simp_all add: tcopy_phase.simps tcopy_stage.simps 
+                    tcopy_state.simps tcopy_step.simps)
+apply(drule_tac bs = b and as = "Bk # list" in rev_tl_hd_merge)
+apply(simp)
+apply(drule_tac bs = b and as = "Oc # list" in rev_tl_hd_merge)
+apply(simp)
+done
+
+lemma [elim]: "tcopy_F11 x (b, c) \<Longrightarrow> 
+              (tstep (11, b, c) tcopy, 11, b, c) \<in> tcopy_LE"
+apply(case_tac x, simp)
+apply(simp add: tstep.simps tcopy_def tcopy_LE_def 
+                lex_square_def lex_triple_def lex_pair_def 
+                tcopy_phase.simps)
+done
+
+lemma [elim]: "tcopy_F12 x (b, c) \<Longrightarrow> 
+              (tstep (12, b, c) tcopy, 12, b, c) \<in> tcopy_LE"
+apply(case_tac x, simp)
+apply(simp add: tstep.simps tcopy_def tcopy_LE_def lex_square_def 
+                lex_triple_def lex_pair_def tcopy_phase.simps)
+apply(simp split: if_splits list.splits block.splits taction.splits)
+apply(auto)
+apply(simp_all add: tcopy_phase.simps tcopy_stage.simps 
+                    tcopy_state.simps tcopy_step.simps)
+done
+
+lemma [elim]: "tcopy_F13 x (b, c) \<Longrightarrow> 
+              (tstep (13, b, c) tcopy, 13, b, c) \<in> tcopy_LE"
+apply(case_tac x, simp)
+apply(simp add: tstep.simps tcopy_def tcopy_LE_def lex_square_def 
+                lex_triple_def lex_pair_def tcopy_phase.simps)
+apply(simp split: if_splits list.splits block.splits taction.splits)
+apply(auto)
+apply(simp_all add: tcopy_phase.simps tcopy_stage.simps 
+                    tcopy_state.simps tcopy_step.simps)
+apply(drule equal_length, simp)+
+done
+
+lemma [elim]: "tcopy_F14 x (b, c) \<Longrightarrow> 
+             (tstep (14, b, c) tcopy, 14, b, c) \<in> tcopy_LE"
+apply(case_tac x, simp)
+apply(simp add: tstep.simps tcopy_def tcopy_LE_def lex_square_def 
+                lex_triple_def lex_pair_def tcopy_phase.simps)
+apply(simp split: if_splits list.splits block.splits taction.splits)
+apply(auto)
+apply(simp_all add: tcopy_phase.simps tcopy_stage.simps 
+                    tcopy_state.simps tcopy_step.simps)
+done
+
+lemma [elim]: "tcopy_F15 x (b, c) \<Longrightarrow> 
+          (tstep (15, b, c) tcopy, 15, b, c) \<in> tcopy_LE"
+apply(case_tac x, simp)
+apply(simp add: tstep.simps tcopy_def tcopy_LE_def lex_square_def 
+                lex_triple_def lex_pair_def tcopy_phase.simps )
+apply(simp split: if_splits list.splits block.splits taction.splits)
+apply(auto)
+apply(simp_all add: tcopy_phase.simps tcopy_stage.simps 
+                    tcopy_state.simps tcopy_step.simps)
+done
+
+lemma tcopy_wf_step:"\<lbrakk>a > 0; inv_tcopy x (a, b, c)\<rbrakk> \<Longrightarrow> 
+                     (tstep (a, b, c) tcopy, (a, b, c)) \<in> tcopy_LE"
+apply(simp add:inv_tcopy.simps split: if_splits, auto)
+apply(auto simp: tstep.simps tcopy_def  tcopy_LE_def lex_square_def 
+                 lex_triple_def lex_pair_def tcopy_phase.simps 
+                 tcopy_stage.simps tcopy_state.simps tcopy_step.simps
+           split: if_splits list.splits block.splits taction.splits)
+done
+
+lemma tcopy_wf: 
+"\<forall>n. let nc = steps (Suc 0, [], replicate x Oc) tcopy n in 
+      let Sucnc = steps (Suc 0, [], replicate x Oc) tcopy (Suc n) in
+  \<not> isS0 nc \<longrightarrow> ((Sucnc, nc) \<in> tcopy_LE)"
+proof(rule allI, case_tac 
+   "steps (Suc 0, [], replicate x Oc) tcopy n", auto simp: tstep_red)
+  fix n a b c
+  assume h: "\<not> isS0 (a, b, c)" 
+       "steps (Suc 0, [], replicate x Oc) tcopy n = (a, b, c)"
+  hence  "inv_tcopy x (a, b, c)"
+    using inv_tcopy_steps[of x n] by(simp)
+  thus "(tstep (a, b, c) tcopy, a, b, c) \<in> tcopy_LE"
+    using h
+    by(rule_tac tcopy_wf_step, auto simp: isS0_def)
+qed
+
+text {*
+  The termination of Copying TM:
+*}
+lemma tcopy_halt: 
+  "\<exists>n. isS0 (steps (Suc 0, [], replicate x Oc) tcopy n)"
+apply(insert halt_lemma 
+        [of tcopy_LE isS0 "steps (Suc 0, [], replicate x Oc) tcopy"])
+apply(insert tcopy_wf [of x])
+apply(simp only: Let_def)
+apply(insert wf_tcopy_le)
+apply(simp)
+done
+
+text {*
+  The total correntess of Copying TM:
+*}
+theorem tcopy_halt_rs: "\<exists>stp m. 
+  steps (Suc 0, [], replicate x Oc) tcopy stp = 
+       (0, replicate m Bk, replicate x Oc @ Bk # replicate x Oc)"
+using tcopy_halt[of x]
+proof(erule_tac exE)
+  fix n
+  assume h: "isS0 (steps (Suc 0, [], replicate x Oc) tcopy n)"
+  have "inv_tcopy x (steps (Suc 0, [], replicate x Oc) tcopy n)"
+    using inv_tcopy_steps[of x n] by simp
+  thus "?thesis"
+    using h
+    apply(cases "(steps (Suc 0, [], replicate x Oc) tcopy n)", 
+          auto simp: isS0_def inv_tcopy.simps)
+    apply(rule_tac x = n in exI, auto)
+    done
+qed
+
+section {*
+  The {\em Dithering} Turing Machine 
+*}
+
+text {*
+  The {\em Dithering} TM, when the input is @{text "1"}, it will loop forever, otherwise, it will
+  terminate.
+*}
+definition dither :: "tprog"
+  where
+  "dither \<equiv> [(W0, 1), (R, 2), (L, 1), (L, 0)] "
+
+lemma dither_halt_rs: 
+  "\<exists> stp. steps (Suc 0, Bk\<^bsup>m\<^esup>, [Oc, Oc]) dither stp = 
+                                 (0, Bk\<^bsup>m\<^esup>, [Oc, Oc])"
+apply(rule_tac x = "Suc (Suc (Suc 0))" in exI)
+apply(simp add: dither_def steps.simps 
+                tstep.simps fetch.simps new_tape.simps)
+done
+
+lemma dither_unhalt_state: 
+  "(steps (Suc 0, Bk\<^bsup>m\<^esup>, [Oc]) dither stp = 
+   (Suc 0, Bk\<^bsup>m\<^esup>, [Oc])) \<or> 
+   (steps (Suc 0, Bk\<^bsup>m\<^esup>, [Oc]) dither stp = (2, Oc # Bk\<^bsup>m\<^esup>, []))"
+  apply(induct stp, simp add: steps.simps)
+  apply(simp add: tstep_red, auto)
+  apply(auto simp: tstep.simps fetch.simps dither_def new_tape.simps)
+  done
+
+lemma dither_unhalt_rs: 
+  "\<not> (\<exists> stp. isS0 (steps (Suc 0, Bk\<^bsup>m\<^esup>, [Oc]) dither stp))"
+proof(auto)
+  fix stp
+  assume h1: "isS0 (steps (Suc 0, Bk\<^bsup>m\<^esup>, [Oc]) dither stp)"
+  have "\<not> isS0 ((steps (Suc 0, Bk\<^bsup>m\<^esup>, [Oc]) dither stp))"
+    using dither_unhalt_state[of m stp]
+      by(auto simp: isS0_def)
+  from h1 and this show False by (auto)
+qed
+
+section {*
+  The final diagnal arguments to show the undecidability of Halting problem.
+*}
+
+text {*
+  @{text "haltP tp x"} means TM @{text "tp"} terminates on input @{text "x"}
+  and the final configuration is standard.
+*}
+definition haltP :: "tprog \<Rightarrow> nat \<Rightarrow> bool"
+  where
+  "haltP t x = (\<exists>n a b c. steps (Suc 0, [], Oc\<^bsup>x\<^esup>) t n = (0, Bk\<^bsup>a\<^esup>, Oc\<^bsup>b\<^esup> @ Bk\<^bsup>c\<^esup>))"
+
+lemma [simp]: "length (A |+| B) = length A + length B"
+by(auto simp: t_add.simps tshift.simps)
+
+lemma [intro]: "\<lbrakk>iseven (x::nat); iseven y\<rbrakk> \<Longrightarrow> iseven (x + y)"
+apply(auto simp: iseven_def)
+apply(rule_tac x = "x + xa" in exI, simp)
+done
+
+lemma t_correct_add[intro]: 
+      "\<lbrakk>t_correct A; t_correct B\<rbrakk> \<Longrightarrow> t_correct (A |+| B)"
+apply(auto simp: t_correct.simps tshift.simps t_add.simps 
+  change_termi_state.simps list_all_iff)
+apply(erule_tac x = "(a, b)" in ballE, auto)
+apply(case_tac "ba = 0", auto)
+done
+
+lemma [intro]: "t_correct tcopy"
+apply(simp add: t_correct.simps tcopy_def iseven_def)
+apply(rule_tac x = 15 in exI, simp)
+done
+
+lemma [intro]: "t_correct dither"
+apply(simp add: t_correct.simps dither_def iseven_def)
+apply(rule_tac x = 2 in exI, simp)
+done
+
+text {*
+  The following locale specifies that TM @{text "H"} can be used to solve 
+  the {\em Halting Problem} and @{text "False"} is going to be derived 
+  under this locale. Therefore, the undecidability of {\em Halting Problem}
+  is established. 
+*}
+locale uncomputable = 
+  -- {* The coding function of TM, interestingly, the detailed definition of this 
+  funciton @{text "code"} does not affect the final result. *}
+  fixes code :: "tprog \<Rightarrow> nat" 
+  -- {* 
+  The TM @{text "H"} is the one which is assummed being able to solve the Halting problem.
+  *}
+  and H :: "tprog"
+  assumes h_wf[intro]: "t_correct H"
+  -- {*
+  The following two assumptions specifies that @{text "H"} does solve the Halting problem.
+  *}
+  and h_case: 
+  "\<And> M n. \<lbrakk>(haltP M n)\<rbrakk> \<Longrightarrow> 
+             \<exists> na nb. (steps (Suc 0, Bk\<^bsup>x\<^esup>, Oc\<^bsup>code M\<^esup> @ Bk # Oc\<^bsup>n\<^esup>) H na = (0, Bk\<^bsup>nb\<^esup>, [Oc]))"
+  and nh_case: 
+  "\<And> M n. \<lbrakk>(\<not> haltP M n)\<rbrakk> \<Longrightarrow>
+             \<exists> na nb. (steps (Suc 0, Bk\<^bsup>x\<^esup>, Oc\<^bsup>code M\<^esup> @ Bk # Oc\<^bsup>n\<^esup>) H na = (0, Bk\<^bsup>nb\<^esup>, [Oc, Oc]))"
+begin
+
+term t_correct
+declare haltP_def[simp del]
+definition tcontra :: "tprog \<Rightarrow> tprog"
+  where
+  "tcontra h \<equiv> ((tcopy |+| h) |+| dither)"
+
+lemma [simp]: "a\<^bsup>0\<^esup> = []"
+  by(simp add: exponent_def)
+lemma haltP_weaking: 
+  "haltP (tcontra H) (code (tcontra H)) \<Longrightarrow> 
+    \<exists>stp. isS0 (steps (Suc 0, [], Oc\<^bsup>code (tcontra H)\<^esup>) 
+          ((tcopy |+| H) |+| dither) stp)"
+  apply(simp add: haltP_def, auto)
+  apply(rule_tac x = n in exI, simp add: isS0_def tcontra_def)
+  done
+
+lemma h_uh: "haltP (tcontra H) (code (tcontra H))
+       \<Longrightarrow> \<not> haltP (tcontra H) (code (tcontra H))"
+proof -
+  let ?cn = "code (tcontra H)"
+  let ?P1 = "\<lambda> tp. let (l, r) = tp in (l = [] \<and> 
+    (r::block list) = Oc\<^bsup>(?cn)\<^esup>)"
+  let ?Q1 = "\<lambda> (l, r).(\<exists> nb. l = Bk\<^bsup>nb\<^esup> \<and> 
+    r = Oc\<^bsup>(?cn)\<^esup> @ Bk # Oc\<^bsup>(?cn)\<^esup>)"
+  let ?P2 = ?Q1
+  let ?Q2 = "\<lambda> (l, r). (\<exists> nd. l = Bk\<^bsup>nd \<^esup>\<and> r = [Oc])"
+  let ?P3 = "\<lambda> tp. False"
+  assume h: "haltP (tcontra H) (code (tcontra H))"
+  hence h1: "\<And> x. \<exists> na nb. steps (Suc 0, Bk\<^bsup>x\<^esup>, Oc\<^bsup>code (tcontra H)\<^esup> @ Bk # 
+                       Oc\<^bsup>code (tcontra H)\<^esup>) H na = (0, Bk\<^bsup>nb\<^esup>, [Oc])"
+    by(drule_tac x = x in h_case, simp)
+  have "?P1 \<turnstile>-> \<lambda> tp. (\<exists> stp tp'. steps (Suc 0, tp) (tcopy |+| H) stp = (0, tp') \<and> ?Q2 tp')"
+  proof(rule_tac turing_merge.t_merge_halt[of tcopy H "?P1" "?P2" "?P3" 
+         "?P3" "?Q1" "?Q2"], auto simp: turing_merge_def)
+    show "\<exists>stp. case steps (Suc 0, [], Oc\<^bsup>?cn\<^esup>) tcopy stp of (s, tp') \<Rightarrow> 
+                   s = 0 \<and> (case tp' of (l, r) \<Rightarrow> (\<exists>nb. l = Bk\<^bsup>nb\<^esup>) \<and> r = Oc\<^bsup>?cn\<^esup> @ Bk # Oc\<^bsup>?cn\<^esup>)"
+      using tcopy_halt_rs[of "?cn"]
+      apply(auto)
+      apply(rule_tac x = stp in exI, auto simp: exponent_def)
+      done
+  next
+    fix nb
+    show "\<exists>stp. case steps (Suc 0, Bk\<^bsup>nb\<^esup>, Oc\<^bsup>code (tcontra H)\<^esup> @ Bk # Oc\<^bsup>code (tcontra H)\<^esup>) H stp of 
+                     (s, tp') \<Rightarrow> s = 0 \<and> (case tp' of (l, r) \<Rightarrow> (\<exists>nd. l = Bk\<^bsup>nd\<^esup>) \<and> r = [Oc])"
+      using h1[of nb]
+      apply(auto)
+      apply(rule_tac x = na in exI, auto)
+      done
+  next
+    show "\<lambda>(l, r). ((\<exists>nb. l = Bk\<^bsup>nb\<^esup>) \<and> r = Oc\<^bsup>code (tcontra H)\<^esup> @ Bk # Oc\<^bsup>code (tcontra H)\<^esup>) \<turnstile>->
+           \<lambda>(l, r). ((\<exists>nb. l = Bk\<^bsup>nb\<^esup>) \<and> r = Oc\<^bsup>code (tcontra H)\<^esup> @ Bk # Oc\<^bsup>code (tcontra H)\<^esup>)"
+      apply(simp add: t_imply_def)
+      done
+  qed
+  hence "\<exists>stp tp'. steps (Suc 0, [], Oc\<^bsup>?cn\<^esup>) (tcopy |+| H) stp = (0, tp') \<and> 
+                         (case tp' of (l, r) \<Rightarrow> \<exists>nd. l = Bk\<^bsup>nd\<^esup> \<and> r = [Oc])"
+    apply(simp add: t_imply_def)
+    done
+  hence "?P1 \<turnstile>-> \<lambda> tp. \<not> (\<exists> stp. isS0 (steps (Suc 0, tp) ((tcopy |+| H) |+| dither) stp))"
+  proof(rule_tac turing_merge.t_merge_uhalt[of "tcopy |+| H" dither "?P1" "?P3" "?P3" 
+         "?Q2" "?Q2" "?Q2"], simp add: turing_merge_def, auto)
+    fix stp nd
+    assume "steps (Suc 0, [], Oc\<^bsup>code (tcontra H)\<^esup>) (tcopy |+| H) stp = (0, Bk\<^bsup>nd\<^esup>, [Oc])"
+    thus "\<exists>stp. case steps (Suc 0, [], Oc\<^bsup>code (tcontra H)\<^esup>) (tcopy |+| H) stp of (s, tp') 
+              \<Rightarrow> s = 0 \<and> (case tp' of (l, r) \<Rightarrow> (\<exists>nd. l = Bk\<^bsup>nd\<^esup>) \<and> r = [Oc])"
+      apply(rule_tac x = stp in exI, auto)
+      done
+  next
+    fix stp nd  nda stpa
+    assume "isS0 (steps (Suc 0, Bk\<^bsup>nda\<^esup>, [Oc]) dither stpa)"
+    thus "False"
+      using dither_unhalt_rs[of nda]
+      apply auto
+      done
+  next
+    fix stp nd
+    show "\<lambda>(l, r). ((\<exists>nd. l = Bk\<^bsup>nd\<^esup>) \<and> r = [Oc]) \<turnstile>-> 
+               \<lambda>(l, r). ((\<exists>nd. l = Bk\<^bsup>nd\<^esup>) \<and> r = [Oc])"
+      by (simp add: t_imply_def)
+  qed
+  thus "\<not> haltP (tcontra H) (code (tcontra H))"
+    apply(simp add: t_imply_def haltP_def tcontra_def, auto)
+    apply(erule_tac x = n in allE, simp add: isS0_def)
+    done
+qed
+
+lemma uh_h: 
+  assumes uh: "\<not> haltP (tcontra H) (code (tcontra H))"
+  shows "haltP (tcontra H) (code (tcontra H))"
+proof -
+  let ?cn = "code (tcontra H)"
+  have h1: "\<And> x. \<exists> na nb. steps (Suc 0, Bk\<^bsup>x\<^esup>, Oc\<^bsup>?cn\<^esup> @ Bk # Oc\<^bsup>?cn\<^esup>)
+                             H na = (0, Bk\<^bsup>nb\<^esup>, [Oc, Oc])"
+    using uh
+    by(drule_tac x = x in nh_case, simp)
+  let ?P1 = "\<lambda> tp. let (l, r) = tp in (l = [] \<and> 
+                        (r::block list) = Oc\<^bsup>(?cn)\<^esup>)"
+  let ?Q1 = "\<lambda> (l, r).(\<exists> na. l = Bk\<^bsup>na\<^esup> \<and> r = [Oc, Oc])"
+  let ?P2 = ?Q1
+  let ?Q2 = ?Q1
+  let ?P3 = "\<lambda> tp. False"
+  have "?P1 \<turnstile>-> \<lambda> tp. (\<exists> stp tp'. steps (Suc 0, tp) ((tcopy |+| H ) |+| dither) 
+                    stp = (0, tp') \<and> ?Q2 tp')"
+  proof(rule_tac turing_merge.t_merge_halt[of "tcopy |+| H" dither ?P1 ?P2 ?P3 ?P3     
+                                                ?Q1 ?Q2], auto simp: turing_merge_def)
+    show "\<exists>stp. case steps (Suc 0, [], Oc\<^bsup>code (tcontra H)\<^esup>) (tcopy |+| H) stp of (s, tp') \<Rightarrow>  
+
+                        s = 0 \<and> (case tp' of (l, r) \<Rightarrow> (\<exists>na. l = Bk\<^bsup>na\<^esup>) \<and> r = [Oc, Oc])"
+    proof -
+      let ?Q1 = "\<lambda> (l, r).(\<exists> nb. l = Bk\<^bsup>nb\<^esup> \<and>  r = Oc\<^bsup>(?cn)\<^esup> @ Bk # Oc\<^bsup>(?cn)\<^esup>)"
+      let ?P2 = "?Q1"
+      let ?Q2 = "\<lambda> (l, r).(\<exists> na. l = Bk\<^bsup>na\<^esup> \<and> r = [Oc, Oc])"
+      have "?P1 \<turnstile>-> \<lambda> tp. (\<exists> stp tp'. steps (Suc 0, tp) (tcopy |+| H ) 
+                    stp = (0, tp') \<and> ?Q2 tp')"
+      proof(rule_tac turing_merge.t_merge_halt[of tcopy H ?P1 ?P2 ?P3 ?P3 
+                                   ?Q1 ?Q2], auto simp: turing_merge_def)
+        show "\<exists>stp. case steps (Suc 0, [], Oc\<^bsup>code (tcontra H)\<^esup>) tcopy stp of (s, tp') \<Rightarrow> s = 0
+     \<and> (case tp' of (l, r) \<Rightarrow> (\<exists>nb. l = Bk\<^bsup>nb\<^esup>) \<and> r = Oc\<^bsup>code (tcontra H)\<^esup> @ Bk # Oc\<^bsup>code (tcontra H)\<^esup>)"
+          using tcopy_halt_rs[of "?cn"]
+          apply(auto)
+          apply(rule_tac x = stp in exI, simp add: exponent_def)
+          done
+      next
+        fix nb
+        show "\<exists>stp. case steps (Suc 0, Bk\<^bsup>nb\<^esup>, Oc\<^bsup>code (tcontra H)\<^esup> @ Bk # Oc\<^bsup>code (tcontra H)\<^esup>) H stp of
+                (s, tp') \<Rightarrow> s = 0 \<and> (case tp' of (l, r) \<Rightarrow> (\<exists>na. l = Bk\<^bsup>na\<^esup>) \<and> r = [Oc, Oc])"
+          using h1[of nb]
+          apply(auto)
+          apply(rule_tac x = na in exI, auto)
+          done
+      next
+        show "\<lambda>(l, r). ((\<exists>nb. l = Bk\<^bsup>nb\<^esup>) \<and> r = Oc\<^bsup>code (tcontra H)\<^esup> @ Bk # Oc\<^bsup>code (tcontra H)\<^esup>) \<turnstile>->
+                  \<lambda>(l, r). ((\<exists>nb. l = Bk\<^bsup>nb\<^esup>) \<and> r = Oc\<^bsup>code (tcontra H)\<^esup> @ Bk # Oc\<^bsup>code (tcontra H)\<^esup>)"
+          by(simp add: t_imply_def)
+      qed
+      hence "(\<exists> stp tp'. steps (Suc 0, [], Oc\<^bsup>?cn\<^esup>) (tcopy |+| H ) stp = (0, tp') \<and> ?Q2 tp')"
+        apply(simp add: t_imply_def)
+        done
+      thus "?thesis"
+        apply(auto)
+        apply(rule_tac x = stp in exI, auto)
+        done
+    qed
+  next
+    fix na
+    show "\<exists>stp. case steps (Suc 0, Bk\<^bsup>na\<^esup>, [Oc, Oc]) dither stp of (s, tp')
+              \<Rightarrow> s = 0 \<and> (case tp' of (l, r) \<Rightarrow> (\<exists>na. l = Bk\<^bsup>na\<^esup>) \<and> r = [Oc, Oc])"
+      using dither_halt_rs[of na]
+      apply(auto)
+      apply(rule_tac x = stp in exI, auto)
+      done
+  next
+    show "\<lambda>(l, r). ((\<exists>na. l = Bk\<^bsup>na\<^esup>) \<and> r = [Oc, Oc]) \<turnstile>->
+                           (\<lambda>(l, r). (\<exists>na. l = Bk\<^bsup>na\<^esup>) \<and> r = [Oc, Oc])"
+      by (simp add: t_imply_def)
+  qed
+  hence "\<exists> stp tp'. steps (Suc 0, [], Oc\<^bsup>?cn\<^esup>) ((tcopy |+| H ) |+| dither) 
+                    stp = (0, tp') \<and> ?Q2 tp'"
+    apply(simp add: t_imply_def)
+    done
+  thus "haltP (tcontra H) (code (tcontra H))"
+    apply(auto simp: haltP_def tcontra_def)
+    apply(rule_tac x = stp in exI,
+         rule_tac x = na in exI,
+         rule_tac x = "Suc (Suc 0)" in exI,
+         rule_tac x = "0" in exI, simp add: exp_ind_def)
+    done
+qed
+   
+text {*
+  @{text "False"} is finally derived.
+*}
+
+lemma "False"
+using uh_h h_uh
+by auto
+end
+
+end
+