diff -r 0b302c0b449a -r 469c26d19f8e uncomputable.thy
--- a/uncomputable.thy Wed Feb 06 02:25:00 2013 +0000
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,1614 +0,0 @@
-(* 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 (l, r) = (\<exists> i. l = Bk\<^bsup>i\<^esup> \<and> r = Oc\<^bsup>x\<^esup> @ Bk # Oc\<^bsup>x\<^esup>)"
-
-fun tcopy_F1 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
- where
- "tcopy_F1 x (l, r) = (l = [] \<and> r = Oc\<^bsup>x\<^esup>)"
-
-fun tcopy_F2 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
- where
- "tcopy_F2 x (l, r) = (\<exists> i j. i > 0 \<and> i + j = x \<and> l = Oc\<^bsup>i\<^esup> \<and> r = Oc\<^bsup>j\<^esup>)"
-
-fun tcopy_F3 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
- where
- "tcopy_F3 x (l, r) = (x > 0 \<and> l = Bk # Oc\<^bsup>x\<^esup> \<and> tl r = [])"
-
-fun tcopy_F4 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
- where
- "tcopy_F4 x (l, r) = (x > 0 \<and> ((l = Oc\<^bsup>x\<^esup> \<and> r = [Bk, Oc]) \<or> (l = Oc\<^bsup>x - 1\<^esup> \<and> r = [Oc, Bk, Oc])))"
-
-fun tcopy_F5_loop :: "nat \<Rightarrow> tape \<Rightarrow> bool"
- where
- "tcopy_F5_loop x (l, r) =
- (\<exists> i j. i + j + 1 = x \<and> l = Oc\<^bsup>i\<^esup> \<and> r = Oc # Oc # Bk\<^bsup>j\<^esup> @ Oc\<^bsup>j\<^esup> \<and> j > 0)"
-
-fun tcopy_F5_exit :: "nat \<Rightarrow> tape \<Rightarrow> bool"
- where
- "tcopy_F5_exit x (l, r) =
- (l = [] \<and> r = Bk # Oc # Bk\<^bsup>x\<^esup> @ Oc\<^bsup>x\<^esup> \<and> x > 0 )"
-
-fun tcopy_F5 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
- where
- "tcopy_F5 x (l, r) = (tcopy_F5_loop x (l, r) \<or> tcopy_F5_exit x (l, r))"
-
-fun tcopy_F6 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
- where
- "tcopy_F6 x (l, r) =
- (\<exists> i j any. i + j = x \<and> x > 0 \<and> i > 0 \<and> j > 0 \<and> l = Oc\<^bsup>i\<^esup> \<and> r = any#Bk\<^bsup>j\<^esup> @ Oc\<^bsup>j\<^esup>)"
-
-fun tcopy_F7 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
- where
- "tcopy_F7 x (l, r) =
- (\<exists> i j k t. i + j = x \<and> i > 0 \<and> j > 0 \<and> k + t = Suc j \<and> l = Bk\<^bsup>k\<^esup> @ Oc\<^bsup>i\<^esup> \<and> r = Bk\<^bsup>t\<^esup> @ Oc\<^bsup>j\<^esup>)"
-
-fun tcopy_F8 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
- where
- "tcopy_F8 x (l, r) =
- (\<exists> i j k t. i + j = x \<and> i > 0 \<and> j > 0 \<and> k + t = j \<and> l = Oc\<^bsup>k\<^esup> @ Bk\<^bsup>Suc j\<^esup> @ Oc\<^bsup>i\<^esup> \<and> r = Oc\<^bsup>t\<^esup>)"
-
-fun tcopy_F9_loop :: "nat \<Rightarrow> tape \<Rightarrow> bool"
-where
- "tcopy_F9_loop x (l, r) =
- (\<exists> i j k t. i + j = Suc x \<and> i > 0 \<and> j > 0 \<and> k + t = j \<and> t > 0\<and> l = Oc\<^bsup>k\<^esup> @ Bk\<^bsup>j\<^esup> @ Oc\<^bsup>i\<^esup> \<and> r = Oc\<^bsup>t\<^esup>)"
-
-fun tcopy_F9_exit :: "nat \<Rightarrow> tape \<Rightarrow> bool"
- where
- "tcopy_F9_exit x (l, r) = (\<exists> i j. i + j = Suc x \<and> i > 0 \<and> j > 0 \<and> l = Bk\<^bsup>j - 1\<^esup> @ Oc\<^bsup>i\<^esup> \<and> r = Bk # Oc\<^bsup>j\<^esup>)"
-
-fun tcopy_F9 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
- where
- "tcopy_F9 x (l, r) = (tcopy_F9_loop x (l, r) \<or>
- tcopy_F9_exit x (l, r))"
-
-fun tcopy_F10_loop :: "nat \<Rightarrow> tape \<Rightarrow> bool"
- where
- "tcopy_F10_loop x (l, r) =
- (\<exists> i j k t. i + j = Suc x \<and> i > 0 \<and> k + t + 1 = j \<and> l = Bk\<^bsup>k\<^esup> @ Oc\<^bsup>i\<^esup> \<and> r = Bk\<^bsup>Suc t\<^esup> @ Oc\<^bsup>j\<^esup>)"
-
-fun tcopy_F10_exit :: "nat \<Rightarrow> tape \<Rightarrow> bool"
- where
- "tcopy_F10_exit x (l, r) =
- (\<exists> i j. i + j = x \<and> j > 0 \<and> l = Oc\<^bsup>i\<^esup> \<and> r = Oc # Bk\<^bsup>j\<^esup> @ Oc\<^bsup>j\<^esup>)"
-
-fun tcopy_F10 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
- where
- "tcopy_F10 x (l, r) = (tcopy_F10_loop x (l, r) \<or> tcopy_F10_exit x (l, r))"
-
-fun tcopy_F11 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
- where
- "tcopy_F11 x (l, r) = (x > 0 \<and> l = [Bk] \<and> r = Oc # Bk\<^bsup>x\<^esup> @ Oc\<^bsup>x\<^esup>)"
-
-fun tcopy_F12 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
- where
- "tcopy_F12 x (l, r) = (\<exists> i j. i + j = Suc x \<and> x > 0 \<and> l = Oc\<^bsup>i\<^esup> @ [Bk] \<and> r = Bk\<^bsup>j\<^esup> @ Oc\<^bsup>x\<^esup>)"
-
-fun tcopy_F13 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
- where
- "tcopy_F13 x (l, r) =
- (\<exists> i j. x > 0 \<and> i + j = x \<and> l = Oc\<^bsup>i\<^esup> @ [Bk] \<and> r = Oc # Bk\<^bsup>j\<^esup> @ Oc\<^bsup>x\<^esup> )"
-
-fun tcopy_F14 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
- where
- "tcopy_F14 x (l, r) = (\<exists> any. x > 0 \<and> l = Oc\<^bsup>x\<^esup> @ [Bk] \<and> r = any#Oc\<^bsup>x\<^esup>)"
-
-fun tcopy_F15_loop :: "nat \<Rightarrow> tape \<Rightarrow> bool"
- where
- "tcopy_F15_loop x (l, r) =
- (\<exists> i j. i + j = x \<and> x > 0 \<and> j > 0 \<and> l = Oc\<^bsup>i\<^esup> @ [Bk] \<and> r = Oc\<^bsup>j\<^esup> @ Bk # Oc\<^bsup>x\<^esup>)"
-
-fun tcopy_F15_exit :: "nat \<Rightarrow> tape \<Rightarrow> bool"
- where
- "tcopy_F15_exit x (l, r) = (x > 0 \<and> l = [] \<and> r = Bk # Oc\<^bsup>x\<^esup> @ Bk # Oc\<^bsup>x\<^esup>)"
-
-fun tcopy_F15 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
- where
- "tcopy_F15 x (l, r) = (tcopy_F15_loop x (l, r) \<or> tcopy_F15_exit x (l, r))"
-
-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 exp_zero_simp: "(a\<^bsup>b\<^esup> = []) = (b = 0)"
-apply(auto simp: exponent_def)
-done
-
-lemma exp_zero_simp2: "([] = a\<^bsup>b\<^esup> ) = (b = 0)"
-apply(auto simp: exponent_def)
-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)
-apply(erule_tac [!] x = "x - 1" in allE)
-apply(case_tac [!] x, simp_all add: exp_ind_def exp_zero)
-apply(erule_tac [!] x = "Suc 0" in allE, simp_all)
-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 false_case1:
- "\<lbrakk>Oc\<^bsup>j\<^esup> @ Bk # Oc\<^bsup>i + j\<^esup> = Oc # list;
- 0 < i;
- \<forall>ia. tl (Oc\<^bsup>i\<^esup> @ [Bk]) = Oc\<^bsup>ia\<^esup> @ [Bk] \<longrightarrow> (\<forall>ja. ia + ja = i + j
- \<longrightarrow> hd (Oc\<^bsup>i\<^esup> @ [Bk]) # Oc # list \<noteq> Oc\<^bsup>ja\<^esup> @ Bk # Oc\<^bsup>i + j\<^esup>)\<rbrakk>
- \<Longrightarrow> RR"
-apply(case_tac i, auto simp: exp_ind_def)
-apply(erule_tac x = nat in allE, simp add:exp_ind_def)
-apply(erule_tac x = "Suc j" in allE, simp)
-done
-
-lemma false_case3:"\<forall>ja. ja \<noteq> i \<Longrightarrow> RR"
-by auto
-
-lemma [elim]: "\<lbrakk>tstep (15, b, c) tcopy = (15, ab, ba);
- tcopy_F15 x (b, c)\<rbrakk> \<Longrightarrow> tcopy_F15 x (ab, ba)"
-apply(auto simp: tstep.simps tcopy_F15.simps
- tcopy_def fetch.simps new_tape.simps
- split: if_splits list.splits block.splits elim: false_case1)
-apply(case_tac [!] i, simp_all add: exp_zero exp_ind_def)
-apply(erule_tac [!] x = nat in allE, simp_all add: exp_ind_def)
-apply(auto elim: false_case3)
-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)
-apply(case_tac [!] j, simp_all add: exp_zero exp_ind_def)
-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(auto simp:tcopy_F12.simps tcopy_F13.simps
- tcopy_def tstep.simps fetch.simps new_tape.simps
- split: if_splits list.splits block.splits)
-apply(case_tac x, simp_all add: exp_ind_def exp_zero)
-apply(rule_tac [!] x = i in exI, simp_all)
-apply(rule_tac [!] x = "j - 1" in exI)
-apply(case_tac [!] j, simp_all add: exp_ind_def exp_zero)
-apply(case_tac x, simp_all add: exp_ind_def exp_zero)
-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)
-apply(rule_tac x = "Suc 0" in exI,
- rule_tac x = x in exI, simp add: exp_ind_def exp_zero)
-done
-
-
-lemma [elim]: "\<lbrakk>tstep (13, b, c) tcopy = (12, ab, ba);
- tcopy_F13 x (b, c)\<rbrakk> \<Longrightarrow> tcopy_F12 x (ab, ba)"
-apply(auto simp:tcopy_F12.simps tcopy_F13.simps
- tcopy_def tstep.simps fetch.simps new_tape.simps
- split: if_splits list.splits block.splits)
-apply(rule_tac [!] x = "Suc i" in exI, simp_all add: exp_ind_def)
-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(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 F10_false: "tcopy_F10 x (b, []) = False"
-apply(auto simp: tcopy_F10.simps exp_ind_def)
-done
-
-lemma F10_false2: "tcopy_F10 x ([], Bk # list) = False"
-apply(auto simp:tcopy_F10.simps)
-apply(case_tac i, simp_all add: exp_ind_def exp_zero)
-done
-
-lemma [simp]: "tcopy_F10_exit x (b, Bk # list) = False"
-apply(auto simp: tcopy_F10.simps)
-done
-
-declare tcopy_F10_loop.simps[simp del] tcopy_F10_exit.simps[simp del]
-
-lemma [simp]: "tcopy_F10_loop x (b, [Bk]) = False"
-apply(auto simp: tcopy_F10_loop.simps)
-apply(simp add: exp_ind_def)
-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(simp add: tcopy_def tstep.simps fetch.simps
- new_tape.simps exp_ind_def exp_zero_simp exp_zero_simp2 F10_false F10_false2
- split: if_splits list.splits block.splits)
-apply(simp add: tcopy_F10.simps del: tcopy_F10_loop.simps tcopy_F10_exit.simps)
-apply(case_tac b, simp, case_tac aa)
-apply(rule_tac disjI1)
-apply(simp only: tcopy_F10_loop.simps)
-apply(erule_tac exE)+
-apply(rule_tac x = i in exI, rule_tac x = j in exI,
- rule_tac x = "k - 1" in exI, rule_tac x = "Suc t" in exI, simp)
-apply(case_tac k, simp_all add: exp_ind_def exp_zero)
-apply(case_tac i, simp_all add: exp_ind_def exp_zero)
-apply(rule_tac disjI2)
-apply(simp only: tcopy_F10_loop.simps tcopy_F10_exit.simps)
-apply(erule_tac exE)+
-apply(rule_tac x = "i - 1" in exI, rule_tac x = "j" in exI)
-apply(case_tac k, simp_all add: exp_ind_def exp_zero)
-apply(case_tac i, simp_all add: exp_ind_def exp_zero)
-apply(auto)
-apply(simp add: exp_ind_def)
-done
-
-(*
-lemma false_case4: "\<lbrakk>i + (k + t) = Suc x;
- 0 < i;
- Bk # list = Oc\<^bsup>t\<^esup>;
- \<forall>ia j. ia + j = Suc x \<longrightarrow> ia = 0 \<or> (\<forall>ka. tl (Oc\<^bsup>k\<^esup>) @ Bk\<^bsup>k + t\<^esup> @ Oc\<^bsup>i\<^esup> = Bk\<^bsup>ka\<^esup> @ Oc\<^bsup>ia\<^esup> \<longrightarrow> (\<forall>ta. Suc (ka + ta) = j \<longrightarrow> Oc # Oc\<^bsup>t\<^esup> \<noteq> Bk\<^bsup>Suc ta\<^esup> @ Oc\<^bsup>j\<^esup>));
- 0 < k\<rbrakk>
- \<Longrightarrow> RR"
-apply(case_tac t, simp_all add: exp_ind_def exp_zero)
-done
-
-lemma false_case5: "
- \<lbrakk>Suc (i + nata) = x;
- 0 < i;
- \<forall>ia j. ia + j = Suc x \<longrightarrow> ia = 0 \<or> (\<forall>k. Bk\<^bsup>nata\<^esup> @ Oc\<^bsup>i\<^esup> = Bk\<^bsup>k\<^esup> @ Oc\<^bsup>ia\<^esup> \<longrightarrow> (\<forall>t. Suc (k + t) = j \<longrightarrow> Bk # Oc # Oc # Oc\<^bsup>nata\<^esup> \<noteq> Bk\<^bsup>t\<^esup> @ Oc\<^bsup>j\<^esup>))\<rbrakk>
- \<Longrightarrow> False"
-apply(erule_tac x = i in allE, simp)
-apply(erule_tac x = "Suc (Suc nata)" in allE, simp)
-apply(erule_tac x = nata in allE, simp, simp add: exp_ind_def exp_zero)
-done
-
-lemma false_case6: "\<lbrakk>0 < x; \<forall>i. tl (Oc\<^bsup>x\<^esup>) = Oc\<^bsup>i\<^esup> \<longrightarrow> (\<forall>j. i + j = x \<longrightarrow> j = 0 \<or> [Bk, Oc] \<noteq> Bk\<^bsup>j\<^esup> @ Oc\<^bsup>j\<^esup>)\<rbrakk>
- \<Longrightarrow> False"
-apply(erule_tac x = "x - 1" in allE)
-apply(case_tac x, simp_all add: exp_ind_def exp_zero)
-apply(erule_tac x = "Suc 0" in allE, simp)
-done
-*)
-
-lemma [simp]: "tcopy_F9 x ([], b) = False"
-apply(auto simp: tcopy_F9.simps)
-apply(case_tac [!] i, simp_all add: exp_ind_def exp_zero)
-done
-
-lemma [simp]: "tcopy_F9 x (b, []) = False"
-apply(auto simp: tcopy_F9.simps)
-apply(case_tac [!] t, simp_all add: exp_ind_def exp_zero)
-done
-
-declare tcopy_F9_loop.simps[simp del] tcopy_F9_exit.simps[simp del]
-lemma [simp]: "tcopy_F9_loop x (b, Bk # list) = False"
-apply(auto simp: tcopy_F9_loop.simps)
-apply(case_tac [!] t, simp_all add: exp_ind_def exp_zero)
-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(auto simp:tcopy_def
- tstep.simps fetch.simps new_tape.simps exp_zero_simp
- exp_zero_simp2
- split: if_splits list.splits block.splits)
-apply(case_tac "hd b", simp add:tcopy_F9.simps tcopy_F10.simps )
-apply(simp only: tcopy_F9_exit.simps tcopy_F10_loop.simps)
-apply(erule_tac exE)+
-apply(rule_tac x = i in exI, rule_tac x = j in exI, simp)
-apply(rule_tac x = "j - 2" in exI, simp add: exp_ind_def)
-apply(case_tac j, simp, simp)
-apply(case_tac nat, simp_all add: exp_zero exp_ind_def)
-apply(case_tac x, simp_all add: exp_ind_def exp_zero)
-apply(simp add: tcopy_F9.simps tcopy_F10.simps)
-apply(rule_tac disjI2)
-apply(simp only: tcopy_F10_exit.simps tcopy_F9_exit.simps)
-apply(erule_tac exE)+
-apply(simp)
-apply(case_tac j, simp_all, case_tac nat, simp_all add: exp_ind_def exp_zero)
-apply(case_tac x, simp_all add: exp_ind_def exp_zero)
-apply(rule_tac x = nata in exI, rule_tac x = 1 in exI, simp add: exp_ind_def exp_zero)
-done
-
-lemma false_case7:
- "\<lbrakk>i + (n + t) = x; 0 < i; 0 < t; Oc # list = Oc\<^bsup>t\<^esup>; k = Suc n;
- \<forall>j. i + j = Suc x \<longrightarrow> (\<forall>k. Oc\<^bsup>n\<^esup> @ Bk # Bk\<^bsup>n + t\<^esup> = Oc\<^bsup>k\<^esup> @ Bk\<^bsup>j\<^esup> \<longrightarrow>
- (\<forall>ta. k + ta = j \<longrightarrow> ta = 0 \<or> Oc # Oc\<^bsup>t\<^esup> \<noteq> Oc\<^bsup>ta\<^esup>))\<rbrakk>
- \<Longrightarrow> RR"
-apply(erule_tac x = "k + t" in allE, simp)
-apply(erule_tac x = n in allE, simp add: exp_ind_def)
-apply(erule_tac x = "Suc t" in allE, simp)
-done
-
-lemma false_case8:
- "\<lbrakk>i + t = Suc x;
- 0 < i;
- 0 < t;
- \<forall>ia j. tl (Bk\<^bsup>t\<^esup> @ Oc\<^bsup>i\<^esup>) = Bk\<^bsup>j - Suc 0\<^esup> @ Oc\<^bsup>ia\<^esup> \<longrightarrow>
- ia + j = Suc x \<longrightarrow> ia = 0 \<or> j = 0 \<or> Oc\<^bsup>t\<^esup> \<noteq> Oc\<^bsup>j\<^esup>\<rbrakk> \<Longrightarrow>
- RR"
-apply(erule_tac x = i in allE, simp)
-apply(erule_tac x = t in allE, simp)
-apply(case_tac t, simp_all add: exp_ind_def exp_zero)
-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(auto simp: tcopy_F9.simps tcopy_def
- tstep.simps fetch.simps new_tape.simps exp_zero_simp exp_zero_simp2
- tcopy_F9_exit.simps tcopy_F9_loop.simps
- split: if_splits list.splits block.splits)
-apply(case_tac [!] k, simp_all add: exp_ind_def exp_zero)
-apply(erule_tac [!] x = i in allE, simp)
-apply(erule_tac false_case7, simp_all)+
-apply(case_tac t, simp_all add: exp_zero exp_ind_def)
-apply(erule_tac false_case7, simp_all)+
-apply(erule_tac false_case8, simp_all)
-apply(erule_tac false_case7, simp_all)+
-apply(case_tac t, simp_all add: exp_ind_def exp_zero)
-apply(erule_tac false_case7, simp_all)
-apply(erule_tac false_case8, simp_all)
-apply(erule_tac false_case7, simp_all)
-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(auto simp:tcopy_F8.simps tcopy_F9.simps tcopy_def
- tstep.simps fetch.simps new_tape.simps tcopy_F9_loop.simps
- tcopy_F9_exit.simps
- split: if_splits list.splits block.splits)
-apply(case_tac [!] t, simp_all add: exp_ind_def exp_zero)
-apply(rule_tac x = i in exI)
-apply(rule_tac x = "Suc k" in exI, simp)
-apply(rule_tac x = "k" in exI, simp add: exp_ind_def exp_zero)
-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(auto simp:tcopy_F8.simps tcopy_def tstep.simps
- fetch.simps new_tape.simps exp_zero_simp exp_zero split: if_splits list.splits
-
- block.splits)
-apply(rule_tac x = i in exI, rule_tac x = "k + t" in exI, simp)
-apply(rule_tac x = "Suc k" in exI, simp)
-apply(rule_tac x = "t - 1" in exI, simp)
-apply(case_tac t, simp_all add: exp_zero exp_ind_def)
-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(auto simp:tcopy_F7.simps tcopy_def tstep.simps fetch.simps
- new_tape.simps exp_ind_def exp_zero_simp
- split: if_splits list.splits block.splits)
-apply(rule_tac x = i in exI)
-apply(rule_tac x = j in exI, simp)
-apply(rule_tac x = "Suc k" in exI, simp)
-apply(rule_tac x = "t - 1" in exI)
-apply(case_tac t, simp_all add: exp_zero exp_ind_def)
-apply(case_tac j, simp_all add: exp_zero exp_ind_def)
-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(auto simp:tcopy_F7.simps tcopy_def tstep.simps tcopy_F8.simps
- fetch.simps new_tape.simps exp_zero_simp
- split: if_splits list.splits block.splits)
-apply(rule_tac x = i in exI, simp)
-apply(rule_tac x = "Suc 0" in exI, simp add: exp_ind_def exp_zero)
-apply(rule_tac x = "j - 1" in exI, simp)
-apply(case_tac t, simp_all add: exp_ind_def )
-apply(case_tac j, simp_all add: exp_ind_def exp_zero)
-done
-
-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 exp_zero_simp
- split: if_splits list.splits block.splits)
-apply(case_tac i, simp_all add: exp_ind_def exp_zero)
-apply(rule_tac x = i in exI, simp)
-apply(rule_tac x = j in exI, simp)
-apply(rule_tac x = "Suc 0" in exI, simp add: exp_ind_def exp_zero)
-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(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(auto simp:tcopy_F5.simps tcopy_F6.simps tcopy_def
- tstep.simps fetch.simps new_tape.simps exp_zero_simp2
- split: if_splits list.splits block.splits)
-apply(rule_tac x = "Suc 0" in exI, simp add: exp_ind_def exp_zero)
-apply(rule_tac x = "Suc i" in exI, simp add: exp_ind_def)
-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(auto simp:tcopy_F5.simps tcopy_F10.simps tcopy_def
- tstep.simps fetch.simps new_tape.simps exp_zero_simp exp_zero_simp2
- exp_ind_def tcopy_F10.simps tcopy_F10_loop.simps tcopy_F10_exit.simps
- split: if_splits list.splits block.splits )
-apply(erule_tac [!] x = "i - 1" in allE)
-apply(erule_tac [!] x = j in allE, simp_all)
-apply(case_tac [!] i, simp_all add: exp_ind_def)
-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(auto simp:tcopy_F5.simps tcopy_F4.simps tcopy_def
- tstep.simps fetch.simps new_tape.simps exp_zero_simp exp_zero_simp2
- split: if_splits list.splits block.splits)
-apply(case_tac x, simp, simp add: exp_ind_def exp_zero)
-apply(erule_tac [!] x = "x - 2" in allE)
-apply(erule_tac [!] x = "Suc 0" in allE)
-apply(case_tac [!] x, simp_all add: exp_ind_def exp_zero)
-apply(case_tac [!] nat, simp_all add: exp_ind_def exp_zero)
-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(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 exp_zero_simp exp_zero_simp2 exp_ind_def
- 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(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 (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
- exp_zero_simp exp_zero_simp2 exp_zero
- split: if_splits list.splits block.splits)
-apply(case_tac [!] j, simp_all add: exp_zero exp_ind_def)
-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(auto simp:tcopy_F3.simps tcopy_F2.simps
- tcopy_def tstep.simps fetch.simps new_tape.simps
- exp_zero_simp exp_zero_simp2 exp_zero
- split: if_splits list.splits block.splits)
-apply(rule_tac x = "Suc i" in exI, simp add: exp_ind_def exp_zero)
-apply(rule_tac x = "j - 1" in exI, simp)
-apply(case_tac j, simp_all add: exp_ind_def exp_zero)
-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(auto simp:tcopy_F1.simps tcopy_F2.simps
- tcopy_def tstep.simps fetch.simps new_tape.simps
- exp_zero_simp exp_zero_simp2 exp_zero
- split: if_splits list.splits block.splits)
-apply(rule_tac x = "Suc 0" in exI, simp)
-apply(rule_tac x = "x - 1" in exI, simp)
-apply(case_tac x, simp_all add: exp_ind_def exp_zero)
-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(simp_all add:tcopy_F0.simps tcopy_F1.simps
- tcopy_def tstep.simps fetch.simps new_tape.simps
- exp_zero_simp exp_zero_simp2 exp_zero
- split: if_splits list.splits block.splits )
-apply(case_tac x, simp_all add: exp_ind_def exp_zero, auto)
-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(auto simp: tcopy_F15.simps tcopy_F0.simps
- tcopy_def tstep.simps new_tape.simps fetch.simps
- split: if_splits list.splits block.splits)
-apply(rule_tac x = "Suc 0" in exI, simp add: exp_ind_def exp_zero)
-apply(case_tac [!] j, simp_all add: exp_ind_def exp_zero)
-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, [], Oc\<^bsup>x\<^esup>) 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
-
-
-
-
-(*----------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)
-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 simp: exp_ind_def)
-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 exponent_def)
-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 simp: exp_zero_simp)
-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 simp: exp_zero_simp)
-apply(simp_all add: tcopy_phase.simps tcopy_stage.simps
- tcopy_state.simps tcopy_step.simps exponent_def)
-done
-
-lemma rev_equal_rev: "rev a = rev b \<Longrightarrow> a = b"
-by simp
-
-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[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_F9 x (b, c) \<Longrightarrow>
- (tstep (9, b, c) tcopy, 9, 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_F9.simps
- tcopy_F9_loop.simps tcopy_F9_exit.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_F9_loop.simps
- tcopy_state.simps tcopy_step.simps tstep.simps exp_zero_simp
- exponent_def)
-apply(case_tac [1-2] t, simp_all add: rev_tl_hd_merge)
-apply(case_tac j, simp, simp)
-apply(case_tac nat, simp_all)
-apply(case_tac nata, simp_all)
-done
-
-lemma [elim]: "tcopy_F10 x (b, c) \<Longrightarrow>
- (tstep (10, b, c) tcopy, 10, 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_F10_loop.simps
- tcopy_F10_exit.simps exp_zero_simp)
-apply(simp split: if_splits list.splits block.splits taction.splits)
-apply(auto simp: exp_zero_simp)
-apply(simp_all add: tcopy_phase.simps tcopy_stage.simps
- tcopy_state.simps tcopy_step.simps exponent_def
- rev_tl_hd_merge)
-apply(case_tac k, simp_all)
-apply(case_tac nat, simp_all)
-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)
-apply(simp_all add: exp_ind_def)
-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)
-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 exp_length: "length (a\<^bsup>b\<^esup>) = b"
-apply(induct b, simp_all add: exp_zero exp_ind_def)
-done
-
-declare tcopy_F9.simps[simp del] tcopy_F10.simps[simp del]
-
-lemma length_eq: "xs = ys \<Longrightarrow> length xs = length ys"
-by simp
-
-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
- exp_length exp_zero_simp exponent_def
- split: if_splits list.splits block.splits taction.splits)
-apply(case_tac [!] t, simp_all)
-apply(case_tac j, simp_all)
-apply(drule_tac length_eq, simp)
-done
-
-lemma tcopy_wf:
-"\<forall>n. let nc = steps (Suc 0, [], Oc\<^bsup>x\<^esup>) tcopy n in
- let Sucnc = steps (Suc 0, [], Oc\<^bsup>x\<^esup>) tcopy (Suc n) in
- \<not> isS0 nc \<longrightarrow> ((Sucnc, nc) \<in> tcopy_LE)"
-proof(rule allI, case_tac
- "steps (Suc 0, [], Oc\<^bsup>x\<^esup>) tcopy n", auto simp: tstep_red)
- fix n a b c
- assume h: "\<not> isS0 (a, b, c)"
- "steps (Suc 0, [], Oc\<^bsup>x\<^esup>) 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, [], Oc\<^bsup>x\<^esup>) tcopy n)"
-apply(insert halt_lemma
- [of tcopy_LE isS0 "steps (Suc 0, [], Oc\<^bsup>x\<^esup>) 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, [], Oc\<^bsup>x\<^esup>) tcopy stp =
- (0, Bk\<^bsup>m\<^esup>, Oc\<^bsup>x\<^esup> @ Bk # Oc\<^bsup>x\<^esup>)"
-using tcopy_halt[of x]
-proof(erule_tac exE)
- fix n
- assume h: "isS0 (steps (Suc 0, [], Oc\<^bsup>x\<^esup>) tcopy n)"
- have "inv_tcopy x (steps (Suc 0, [], Oc\<^bsup>x\<^esup>) tcopy n)"
- using inv_tcopy_steps[of x n] by simp
- thus "?thesis"
- using h
- apply(cases "(steps (Suc 0, [], Oc\<^bsup>x\<^esup>) tcopy n)",
- auto simp: isS0_def inv_tcopy.simps)
- 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, [], 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, [], 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 tinres_ex1:
- "tinres (Bk\<^bsup>nb\<^esup>) b \<Longrightarrow> \<exists>nb. b = Bk\<^bsup>nb\<^esup>"
-apply(auto simp: tinres_def)
-proof -
- fix n
- assume "Bk\<^bsup>nb\<^esup> = b @ Bk\<^bsup>n\<^esup>"
- thus "\<exists>nb. b = Bk\<^bsup>nb\<^esup>"
- proof(induct b arbitrary: nb)
- show "\<exists>nb. [] = Bk\<^bsup>nb\<^esup>"
- by(rule_tac x = 0 in exI, simp add: exp_zero)
- next
- fix a b nb
- assume ind: "\<And>nb. Bk\<^bsup>nb\<^esup> = b @ Bk\<^bsup>n\<^esup> \<Longrightarrow> \<exists>nb. b = Bk\<^bsup>nb\<^esup>"
- and h: "Bk\<^bsup>nb\<^esup> = (a # b) @ Bk\<^bsup>n\<^esup>"
- from h show "\<exists>nb. a # b = Bk\<^bsup>nb\<^esup>"
- proof(case_tac a, case_tac nb, simp_all add: exp_ind_def)
- fix nat
- assume "Bk\<^bsup>nat\<^esup> = b @ Bk\<^bsup>n\<^esup>"
- thus "\<exists>nb. Bk # b = Bk\<^bsup>nb\<^esup>"
- using ind[of nat]
- apply(auto)
- apply(rule_tac x = "Suc nb" in exI, simp add: exp_ind_def)
- done
- next
- assume "Bk\<^bsup>nb\<^esup> = Oc # b @ Bk\<^bsup>n\<^esup>"
- thus "\<exists>nb. Oc # b = Bk\<^bsup>nb\<^esup>"
- apply(case_tac nb, simp_all add: exp_ind_def)
- done
- qed
- qed
-next
- fix n
- show "\<exists>nba. Bk\<^bsup>nb\<^esup> @ Bk\<^bsup>n\<^esup> = Bk\<^bsup>nba\<^esup>"
- apply(rule_tac x = "nb + n" in exI)
- apply(simp add: exponent_def replicate_add)
- done
-qed
-
-lemma h_newcase: "\<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]))"
-proof -
- fix M n x
- assume "haltP M n"
- hence " \<exists> na nb. (steps (Suc 0, [], Oc\<^bsup>code M\<^esup> @ Bk # Oc\<^bsup>n\<^esup>) H na
- = (0, Bk\<^bsup>nb\<^esup>, [Oc]))"
- apply(erule_tac h_case)
- done
- from this obtain na nb where
- cond1:"(steps (Suc 0, [], Oc\<^bsup>code M\<^esup> @ Bk # Oc\<^bsup>n\<^esup>) H na
- = (0, Bk\<^bsup>nb\<^esup>, [Oc]))" by blast
- thus "\<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]))"
- proof(rule_tac x = na in exI, case_tac "steps (Suc 0, Bk\<^bsup>x\<^esup>, Oc\<^bsup>code M\<^esup> @ Bk # Oc\<^bsup>n\<^esup>) H na", simp)
- fix a b c
- assume cond2: "steps (Suc 0, Bk\<^bsup>x\<^esup>, Oc\<^bsup>code M\<^esup> @ Bk # Oc\<^bsup>n\<^esup>) H na = (a, b, c)"
- have "tinres (Bk\<^bsup>nb\<^esup>) b \<and> [Oc] = c \<and> 0 = a"
- proof(rule_tac tinres_steps)
- show "tinres [] (Bk\<^bsup>x\<^esup>)"
- apply(simp add: tinres_def)
- apply(auto)
- done
- next
- show "(steps (Suc 0, [], Oc\<^bsup>code M\<^esup> @ Bk # Oc\<^bsup>n\<^esup>) H na
- = (0, Bk\<^bsup>nb\<^esup>, [Oc]))"
- by(simp add: cond1)
- next
- show "steps (Suc 0, Bk\<^bsup>x\<^esup>, Oc\<^bsup>code M\<^esup> @ Bk # Oc\<^bsup>n\<^esup>) H na = (a, b, c)"
- by(simp add: cond2)
- qed
- thus "a = 0 \<and> (\<exists>nb. b = Bk\<^bsup>nb\<^esup>) \<and> c = [Oc]"
- apply(auto simp: tinres_ex1)
- done
- qed
-qed
-
-lemma nh_newcase: "\<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]))"
-proof -
- fix M n
- assume "\<not> haltP M n"
- hence "\<exists> na nb. (steps (Suc 0, [], Oc\<^bsup>code M\<^esup> @ Bk # Oc\<^bsup>n\<^esup>) H na
- = (0, Bk\<^bsup>nb\<^esup>, [Oc, Oc]))"
- apply(erule_tac nh_case)
- done
- from this obtain na nb where
- cond1: "(steps (Suc 0, [], Oc\<^bsup>code M\<^esup> @ Bk # Oc\<^bsup>n\<^esup>) H na
- = (0, Bk\<^bsup>nb\<^esup>, [Oc, Oc]))" by blast
- thus "\<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]))"
- proof(rule_tac x = na in exI, case_tac "steps (Suc 0, Bk\<^bsup>x\<^esup>, Oc\<^bsup>code M\<^esup> @ Bk # Oc\<^bsup>n\<^esup>) H na", simp)
- fix a b c
- assume cond2: "steps (Suc 0, Bk\<^bsup>x\<^esup>, Oc\<^bsup>code M\<^esup> @ Bk # Oc\<^bsup>n\<^esup>) H na = (a, b, c)"
- have "tinres (Bk\<^bsup>nb\<^esup>) b \<and> [Oc, Oc] = c \<and> 0 = a"
- proof(rule_tac tinres_steps)
- show "tinres [] (Bk\<^bsup>x\<^esup>)"
- apply(simp add: tinres_def)
- apply(auto)
- done
- next
- show "(steps (Suc 0, [], Oc\<^bsup>code M\<^esup> @ Bk # Oc\<^bsup>n\<^esup>) H na
- = (0, Bk\<^bsup>nb\<^esup>, [Oc, Oc]))"
- by(simp add: cond1)
- next
- show "steps (Suc 0, Bk\<^bsup>x\<^esup>, Oc\<^bsup>code M\<^esup> @ Bk # Oc\<^bsup>n\<^esup>) H na = (a, b, c)"
- by(simp add: cond2)
- qed
- thus "a = 0 \<and> (\<exists>nb. b = Bk\<^bsup>nb\<^esup>) \<and> c = [Oc, Oc]"
- apply(auto simp: tinres_ex1)
- done
- qed
-qed
-
-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_newcase, 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_newcase, 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
-