--- a/utm/uncomputable.thy Wed Dec 12 11:45:04 2012 +0000
+++ b/utm/uncomputable.thy Fri Mar 01 17:13:32 2013 +0000
@@ -37,136 +37,110 @@
*}
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)"
+ "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 (ln, rn) = (ln = [] & rn = replicate x Oc)"
+ "tcopy_F1 x (l, r) = (l = [] \<and> r = Oc\<^bsup>x\<^esup>)"
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)"
+ 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 0 tp = False" |
- "tcopy_F3 (Suc x) (ln, rn) =
- (ln = Bk # replicate (Suc x) Oc & length rn <= 1)"
+ "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 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])) "
+ "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 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)"
-
+ "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 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)"
-
+ "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 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 ))"
-
+ "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 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)) "
+ "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 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))"
+ "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 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 ))"
+ "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 0 tp = False" |
- "tcopy_F11 (Suc x) (ln, rn) =
- (ln = [Bk] & rn = Oc # replicate (Suc x) Bk
- @ replicate (Suc x) Oc)"
+ "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 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))"
+ "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 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))"
-
+ "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 0 tp = False" |
- "tcopy_F14 (Suc x) (ln, rn) =
- (ln = replicate (Suc x) Oc @ [Bk] &
- tl rn = replicate (Suc x) Oc)"
+ "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 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))"
+ "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.
@@ -208,17 +182,12 @@
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+)
+lemma exp_zero_simp: "(a\<^bsup>b\<^esup> = []) = (b = 0)"
+apply(auto simp: exponent_def)
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)
+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"
@@ -300,6 +269,7 @@
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
@@ -330,22 +300,26 @@
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)
+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"
@@ -364,495 +338,341 @@
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(case_tac x)
+ 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)
-apply(case_tac b, simp+)
+ 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(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+)
+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(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(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(case_tac x)
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 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)
+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(case_tac x)
+ 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 less_equal: "\<lbrakk>length xs <= b; \<not> Suc (length xs) <= b\<rbrakk> \<Longrightarrow>
- length xs = b"
-apply(simp)
+lemma F10_false: "tcopy_F10 x (b, []) = False"
+apply(auto simp: tcopy_F10.simps exp_ind_def)
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)
+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
-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+)
+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(case_tac x)
-apply(auto simp:tcopy_F10.simps tcopy_def tstep.simps fetch.simps
- new_tape.simps
+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(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+)
+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 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)
+(*
+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 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+)
+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 [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+)
+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(case_tac x)
-apply(simp_all add: tcopy_F9.simps tcopy_def
- tstep.simps fetch.simps new_tape.simps
+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(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+)
+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 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)
+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 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)
+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 Suc_more: "n <= m \<Longrightarrow> Suc m - n = Suc (m - n)"
-by simp
+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
+ 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(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)
+ 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
+ tstep.simps fetch.simps new_tape.simps exp_zero_simp2
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+)
+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(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)
+ 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(case_tac x)
apply(auto simp:tcopy_F5.simps tcopy_F4.simps tcopy_def
- tstep.simps fetch.simps new_tape.simps
+ 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(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)
@@ -862,86 +682,68 @@
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
+ 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(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
+ exp_zero_simp exp_zero_simp2 exp_zero
split: if_splits list.splits block.splits)
-apply(drule replicate_cons_same, auto)+
+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(case_tac x)
apply(auto simp:tcopy_F3.simps tcopy_F2.simps
- tcopy_def tstep.simps fetch.simps new_tape.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(frule replicate_cons_same, auto)
-apply(simp add: replicate_app_Cons_same)
+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(case_tac x)
-apply(simp_all add:tcopy_F2.simps tcopy_F1.simps
- tcopy_def tstep.simps fetch.simps new_tape.simps)
-apply(auto)
+ 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(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+)
+ 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(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)
+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)
@@ -968,7 +770,7 @@
Invariant under mult-step execution.
*}
lemma inv_tcopy_steps:
- "inv_tcopy x (steps (Suc 0, [], replicate x Oc) tcopy stp) "
+ "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)
@@ -976,18 +778,6 @@
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----------------------------------------*)
@@ -1183,7 +973,6 @@
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>
@@ -1193,7 +982,7 @@
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(auto simp: exp_ind_def)
done
lemma[simp]: "takeWhile (\<lambda>a. a = b) (replicate x b @ ys) =
@@ -1226,7 +1015,7 @@
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)
+ tcopy_state.simps tcopy_step.simps exponent_def)
done
lemma [elim]: "tcopy_F7 x (b, c) \<Longrightarrow>
@@ -1235,7 +1024,7 @@
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(auto simp: exp_zero_simp)
apply(simp_all add: tcopy_phase.simps tcopy_stage.simps
tcopy_state.simps tcopy_step.simps)
done
@@ -1246,12 +1035,14 @@
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(auto simp: exp_zero_simp)
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)
+ 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
@@ -1266,34 +1057,40 @@
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(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)
+ 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_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)
+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(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)
+ 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)
+apply(auto simp: exp_zero_simp)
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)
+ 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>
@@ -1313,6 +1110,7 @@
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>
@@ -1324,7 +1122,6 @@
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>
@@ -1349,24 +1146,37 @@
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, [], replicate x Oc) tcopy n in
- let Sucnc = steps (Suc 0, [], replicate x Oc) tcopy (Suc n) in
+"\<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, [], replicate x Oc) tcopy n", auto simp: tstep_red)
+ "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, [], replicate x Oc) tcopy n = (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"
@@ -1378,9 +1188,9 @@
The termination of Copying TM:
*}
lemma tcopy_halt:
- "\<exists>n. isS0 (steps (Suc 0, [], replicate x Oc) tcopy n)"
+ "\<exists>n. isS0 (steps (Suc 0, [], Oc\<^bsup>x\<^esup>) tcopy n)"
apply(insert halt_lemma
- [of tcopy_LE isS0 "steps (Suc 0, [], replicate x Oc) tcopy"])
+ [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)
@@ -1390,20 +1200,20 @@
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)"
+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, [], replicate x Oc) tcopy n)"
- have "inv_tcopy x (steps (Suc 0, [], replicate x Oc) tcopy 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, [], replicate x Oc) tcopy n)",
+ apply(cases "(steps (Suc 0, [], Oc\<^bsup>x\<^esup>) tcopy n)",
auto simp: isS0_def inv_tcopy.simps)
- apply(rule_tac x = n in exI, auto)
done
qed
@@ -1505,10 +1315,10 @@
*}
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]))"
+ \<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, Bk\<^bsup>x\<^esup>, Oc\<^bsup>code M\<^esup> @ Bk # Oc\<^bsup>n\<^esup>) H na = (0, Bk\<^bsup>nb\<^esup>, [Oc, Oc]))"
+ \<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
@@ -1519,6 +1329,117 @@
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>)
@@ -1541,7 +1462,7 @@
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)
+ 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)
@@ -1605,7 +1526,7 @@
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)
+ 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])"