tm: comparison uncomputable.thy

equal deleted inserted replaced

-:4b35e0e0784b
+:c9b689bb4156
 text {*
 The following functions are used to expression invariants of {\em Copying} TM.
 *}
 fun tcopy_F0 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
 where
-"tcopy_F0 x tp = (let (ln, rn) = tp in
+"tcopy_F0 x (l, r) = (\<exists> i. l = Bk\<^bsup>i\<^esup> \<and> r = Oc\<^bsup>x\<^esup> @ Bk # Oc\<^bsup>x\<^esup>)"
-list_all isBk ln & rn = replicate x Oc
-@ [Bk] @ replicate x Oc)"
 fun tcopy_F1 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
 where
-"tcopy_F1 x (ln, rn) = (ln = [] & rn = replicate x Oc)"
+"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 x (l, r) = (\<exists> i j. i > 0 \<and> i + j = x \<and> l = Oc\<^bsup>i\<^esup> \<and> r = Oc\<^bsup>j\<^esup>)"
-"tcopy_F2 (Suc x) (ln, rn) = (length ln > 0 &
-ln @ rn = replicate (Suc x) Oc)"
 fun tcopy_F3 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
 where
-"tcopy_F3 0 tp = False" |
+"tcopy_F3 x (l, r) = (x > 0 \<and> l = Bk # Oc\<^bsup>x\<^esup> \<and> tl r = [])"
-"tcopy_F3 (Suc x) (ln, rn) =
-(ln = Bk # replicate (Suc x) Oc & length rn <= 1)"
 fun tcopy_F4 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
 where
-"tcopy_F4 0 tp = False" |
+"tcopy_F4 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])))"
-"tcopy_F4 (Suc x) (ln, rn) =
-((ln = replicate x Oc & rn = [Oc, Bk, Oc])
+fun tcopy_F5_loop :: "nat \<Rightarrow> tape \<Rightarrow> bool"
-| (ln = replicate (Suc x) Oc & rn = [Bk, Oc])) "
+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 x (l, r) = (tcopy_F5_loop x (l, r) \<or> tcopy_F5_exit x (l, r))"
-"tcopy_F5 (Suc x) (ln, rn) =
-(if rn = [] then False
-else if hd rn = Bk then (ln = [] &
-rn = Bk # (Oc # replicate (Suc x) Bk
-@ replicate (Suc x) Oc))
-else if hd rn = Oc then
-(\<exists>n. ln = replicate (x - n) Oc
-& rn = Oc # (Oc # replicate n Bk @ replicate n Oc)
-& n > 0 & n <= x)
-else False)"
 fun tcopy_F6 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
 where
-"tcopy_F6 0 tp = False" |
+"tcopy_F6 x (l, r) =
-"tcopy_F6 (Suc x) (ln, rn) =
+(\<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>)"
-(\<exists>n. ln = replicate (Suc x -n) Oc
-& tl rn = replicate n Bk @ replicate n Oc
-& n > 0 & n <= x)"
 fun tcopy_F7 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
 where
-"tcopy_F7 0 tp = False" |
+"tcopy_F7 x (l, r) =
-"tcopy_F7 (Suc x) (ln, rn) =
+(\<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>)"
-(let lrn = (rev ln) @ rn in
-(\<exists>n. lrn = replicate ((Suc x) - n) Oc @
-replicate (Suc n) Bk @ replicate n Oc
-& n > 0 & n <= x &
-length rn >= n & length rn <= 2 * n ))"
 fun tcopy_F8 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
 where
-"tcopy_F8 0 tp = False" |
+"tcopy_F8 x (l, r) =
-"tcopy_F8 (Suc x) (ln, rn) =
+(\<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>)"
-(let lrn = (rev ln) @ rn in
-(\<exists>n. lrn = replicate ((Suc x) - n) Oc @
+fun tcopy_F9_loop :: "nat \<Rightarrow> tape \<Rightarrow> bool"
-replicate (Suc n) Bk @ replicate n Oc
+where
-& n > 0 & n <= x & length rn < n)) "
+"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 x (l, r) = (tcopy_F9_loop x (l, r) \<or>
-"tcopy_F9 (Suc x) (ln, rn) =
+tcopy_F9_exit x (l, r))"
-(let lrn = (rev ln) @ rn in
-(\<exists>n. lrn = replicate (Suc (Suc x) - n) Oc
+fun tcopy_F10_loop :: "nat \<Rightarrow> tape \<Rightarrow> bool"
-@ replicate n Bk @ replicate n Oc
+where
-& n > Suc 0 & n <= Suc x & length rn > 0
+"tcopy_F10_loop x (l, r) =
-& length rn <= Suc n))"
+(\<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 x (l, r) = (tcopy_F10_loop x (l, r) \<or> tcopy_F10_exit x (l, r))"
-"tcopy_F10 (Suc x) (ln, rn) =
-(let lrn = (rev ln) @ rn in
-(\<exists>n. lrn = replicate (Suc (Suc x) - n) Oc
-@ replicate n Bk @ replicate n Oc & n > Suc 0
-& n <= Suc x & length rn > Suc n &
-length rn <= 2*n + 1 ))"
 fun tcopy_F11 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
 where
-"tcopy_F11 0 tp = False" |
+"tcopy_F11 x (l, r) = (x > 0 \<and> l = [Bk] \<and> r = Oc # Bk\<^bsup>x\<^esup> @ Oc\<^bsup>x\<^esup>)"
-"tcopy_F11 (Suc x) (ln, rn) =
-(ln = [Bk] & rn = Oc # replicate (Suc x) Bk
-@ replicate (Suc x) Oc)"
 fun tcopy_F12 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
 where
-"tcopy_F12 0 tp = False" |
+"tcopy_F12 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>)"
-"tcopy_F12 (Suc x) (ln, rn) =
-(let lrn = ((rev ln) @ rn) in
-(\<exists>n. n > 0 & n <= Suc (Suc x)
-& lrn = Bk # replicate n Oc @ replicate (Suc (Suc x) - n) Bk
-@ replicate (Suc x) Oc
-& length ln = Suc n))"
 fun tcopy_F13 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
 where
-"tcopy_F13 0 tp = False" |
+"tcopy_F13 x (l, r) =
-"tcopy_F13 (Suc x) (ln, rn) =
+(\<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> )"
-(let lrn = ((rev ln) @ rn) in
-(\<exists>n. n > Suc 0 & n <= Suc (Suc x)
-& lrn = Bk # replicate n Oc @ replicate (Suc (Suc x) - n) Bk
-@ replicate (Suc x) Oc
-& length ln = n))"
 fun tcopy_F14 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
 where
-"tcopy_F14 0 tp = False" |
+"tcopy_F14 x (l, r) = (\<exists> any. x > 0 \<and> l = Oc\<^bsup>x\<^esup> @ [Bk] \<and> r = any#Oc\<^bsup>x\<^esup>)"
-"tcopy_F14 (Suc x) (ln, rn) =
-(ln = replicate (Suc x) Oc @ [Bk] &
+fun tcopy_F15_loop :: "nat \<Rightarrow> tape \<Rightarrow> bool"
-tl rn = replicate (Suc x) Oc)"
+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 x (l, r) = (tcopy_F15_loop x (l, r) \<or>  tcopy_F15_exit x (l, r))"
-"tcopy_F15 (Suc x) (ln, rn) =
-(let lrn = ((rev ln) @ rn) in
-lrn = Bk # replicate (Suc x) Oc @ [Bk] @
-replicate (Suc x) Oc & length ln <= (Suc x))"
 text {*
 The following @{text "inv_tcopy"} is the invariant of the {\em Copying} TM.
 *}
 fun inv_tcopy :: "nat \<Rightarrow> t_conf \<Rightarrow> bool"
 tcopy_F12.simps [simp del]
 tcopy_F13.simps [simp del]
 tcopy_F14.simps [simp del]
 tcopy_F15.simps [simp del]
-lemma list_replicate_Bk[dest]: "list_all isBk list \<Longrightarrow>
+lemma exp_zero_simp: "(a\<^bsup>b\<^esup> = []) = (b = 0)"
-list = replicate (length list) Bk"
+apply(auto simp: exponent_def)
-apply(induct list)
+done
-apply(simp+)
-done
+lemma exp_zero_simp2: "([] = a\<^bsup>b\<^esup> ) = (b = 0)"
+apply(auto simp: exponent_def)
-lemma [simp]: "dropWhile (\<lambda> a. a = b) (replicate x b @ ys) =
-dropWhile (\<lambda> a. a = b) ys"
-apply(induct x)
-apply(simp)
-apply(simp)
 done
 lemma [elim]: "\<lbrakk>tstep (0, a, b) tcopy = (s, l, r); s \<noteq> 0\<rbrakk> \<Longrightarrow> RR"
 apply(simp add: tstep.simps tcopy_def fetch.simps)
 done
 lemma [elim]: "\<lbrakk>tstep (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"
 lemma replicate_Cons_simp: "b # replicate n b @ xs =
 replicate n b @ b # xs"
 apply(simp)
 done
+*)
 lemma [elim]: "\<lbrakk>tstep (14, b, c) tcopy = (15, ab, ba);
 tcopy_F14 x (b, c)\<rbrakk> \<Longrightarrow> tcopy_F15 x (ab, ba)"
-apply(case_tac x)
 apply(auto simp: tstep.simps tcopy_def
 tcopy_F14.simps tcopy_F15.simps fetch.simps new_tape.simps
 split: if_splits list.splits block.splits)
-done
+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 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(case_tac x)
 apply(auto simp: tstep.simps tcopy_F15.simps
 tcopy_def fetch.simps new_tape.simps
-split: if_splits list.splits block.splits)
+split: if_splits list.splits block.splits elim: false_case1)
-apply(case_tac b, simp+)
+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 [!] j, simp_all add: exp_zero exp_ind_def)
-apply(case_tac n, simp+)
-apply(case_tac nata, simp+)
-done
-lemma replicate_app_Cons: "replicate a b @ b # replicate c b
-= replicate (Suc (a + c)) b"
-apply(simp)
-apply(simp add: replicate_app_Cons_same)
-apply(simp only: replicate_add[THEN sym])
-done
-lemma replicate_same_exE_pref: "\<exists>x. bs @ (b # cs) = replicate x y
-\<Longrightarrow> (\<exists>n. bs = replicate n y)"
-apply(induct bs)
-apply(rule_tac x = 0 in exI, simp)
-apply(drule impI)
-apply(erule impE)
-apply(erule exE, simp+)
-apply(case_tac x, auto)
-apply(case_tac x, auto)
-apply(rule_tac x = "Suc n" in exI, simp+)
-done
-lemma replicate_same_exE_inf: "\<exists>x. bs @ (b # cs) = replicate x y \<Longrightarrow> b = y"
-apply(induct bs, auto)
-apply(case_tac x, auto)
-apply(drule impI)
-apply(erule impE)
-apply(case_tac x, simp+)
-done
-lemma replicate_same_exE_suf:
-"\<exists>x. bs @ (b # cs) = replicate x y \<Longrightarrow> \<exists>n. cs = replicate n y"
-apply(induct bs, auto)
-apply(case_tac x, simp+)
-apply(drule impI, erule impE)
-apply(case_tac x, simp+)
-done
-lemma replicate_same_exE: "\<exists>x. bs @ (b # cs) = replicate x y
-\<Longrightarrow> (\<exists>n. bs = replicate n y) & (b = y) & (\<exists>m. cs = replicate m y)"
-apply(rule conjI)
-apply(drule  replicate_same_exE_pref, simp)
-apply(rule conjI)
-apply(drule replicate_same_exE_inf, simp)
-apply(drule replicate_same_exE_suf, simp)
-done
-lemma replicate_same: "bs @ (b # cs) = replicate x y
-\<Longrightarrow> (\<exists>n. bs = replicate n y) & (b = y) & (\<exists>m. cs = replicate m y)"
-apply(rule_tac replicate_same_exE)
-apply(rule_tac x = x in exI)
-apply(assumption)
-done
-lemma [elim]: "\<lbrakk> 0 < n; n \<le> Suc (Suc na);
-(rev ab @ Bk # list) = Bk # replicate n Oc
-@ replicate (Suc (Suc na) - n) Bk @ Oc # replicate na Oc; ab \<noteq> []\<rbrakk>
-\<Longrightarrow> n \<le> Suc na"
-apply(rule contrapos_pp, simp+)
-apply(case_tac "rev ab", simp+)
-apply(auto)
-apply(simp only: replicate_app_Cons)
-apply(drule replicate_same)
-apply(auto)
-done
-lemma [elim]: "\<lbrakk>0 < n; n \<le> Suc (Suc na);
-rev ab @ Bk # list = Bk # replicate n Oc @
-replicate (Suc (Suc na) - n) Bk @ Oc # replicate na Oc;
-length ab = Suc n; ab \<noteq> []\<rbrakk>
-\<Longrightarrow> rev ab @ Oc # list = Bk # Oc # replicate n Oc @
-replicate (Suc na - n) Bk @ Oc # replicate na Oc"
-apply(case_tac "rev ab", simp+)
-apply(auto)
-apply(simp only: replicate_Cons_simp)
-apply(simp)
-apply(case_tac "Suc (Suc na) - n", simp+)
 done
 lemma [elim]: "\<lbrakk>tstep (12, b, c) tcopy = (13, ab, ba);
 tcopy_F12 x (b, c)\<rbrakk> \<Longrightarrow> tcopy_F13 x (ab, ba)"
-apply(case_tac x)
+apply(auto simp:tcopy_F12.simps tcopy_F13.simps
-apply(simp_all add:tcopy_F12.simps tcopy_F13.simps
+tcopy_def tstep.simps fetch.simps new_tape.simps
-tcopy_def tstep.simps fetch.simps new_tape.simps)
+split: if_splits list.splits block.splits)
-apply(simp split: if_splits list.splits block.splits)
+apply(case_tac x, simp_all add: exp_ind_def exp_zero)
-apply(auto)
+apply(rule_tac [!] x = i in exI, simp_all)
-done
+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)
-done
+apply(rule_tac x = "Suc 0" in exI,
+rule_tac x = x in exI, simp add: exp_ind_def exp_zero)
-lemma equal_length: "a = b \<Longrightarrow> length a = length b"
+done
-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(auto simp:tcopy_F12.simps tcopy_F13.simps
-apply(simp_all add:tcopy_F12.simps tcopy_F13.simps
+tcopy_def tstep.simps fetch.simps new_tape.simps
-tcopy_def tstep.simps fetch.simps new_tape.simps)
+split: if_splits list.splits block.splits)
-apply(simp split: if_splits list.splits block.splits)
+apply(rule_tac [!] x = "Suc i" in exI, simp_all add: exp_ind_def)
-apply(auto)
-apply(drule equal_length, simp)
 done
 lemma [elim]: "\<lbrakk>tstep (5, b, c) tcopy = (11, ab, ba);
 tcopy_F5 x (b, c)\<rbrakk> \<Longrightarrow> tcopy_F11 x (ab, ba)"
-apply(case_tac x)
 apply(simp_all add:tcopy_F11.simps tcopy_F5.simps tcopy_def
 tstep.simps fetch.simps new_tape.simps)
 apply(simp split: if_splits list.splits block.splits)
 done
-lemma less_equal: "\<lbrakk>length xs <= b; \<not> Suc (length xs) <= b\<rbrakk> \<Longrightarrow>
+lemma F10_false: "tcopy_F10 x (b, []) = False"
-length xs = b"
+apply(auto simp: tcopy_F10.simps exp_ind_def)
-apply(simp)
+done
-done
+lemma F10_false2: "tcopy_F10 x ([], Bk # list) = False"
-lemma length_cons_same: "\<lbrakk>xs @ b # ys = as @ bs;
+apply(auto simp:tcopy_F10.simps)
-length ys = length bs\<rbrakk> \<Longrightarrow> xs @ [b] = as & ys = bs"
+apply(case_tac i, simp_all add: exp_ind_def exp_zero)
-apply(drule rev_equal)
+done
-apply(simp)
-apply(auto)
+lemma [simp]: "tcopy_F10_exit x (b, Bk # list) = False"
-apply(drule rev_equal, simp)
+apply(auto simp: tcopy_F10.simps)
 done
-lemma replicate_set_equal: "\<lbrakk> xs @ [a] = replicate n b; a \<noteq> b\<rbrakk> \<Longrightarrow> RR"
+declare tcopy_F10_loop.simps[simp del]  tcopy_F10_exit.simps[simp del]
-apply(drule rev_equal, simp)
-apply(case_tac n, simp+)
+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(simp add: tcopy_def tstep.simps fetch.simps
-apply(auto simp:tcopy_F10.simps tcopy_def tstep.simps fetch.simps
+new_tape.simps exp_ind_def exp_zero_simp exp_zero_simp2 F10_false F10_false2
-new_tape.simps
 split: if_splits list.splits block.splits)
-apply(rule_tac x = n in exI, auto)
+apply(simp add: tcopy_F10.simps del: tcopy_F10_loop.simps  tcopy_F10_exit.simps)
-apply(case_tac b, simp+)
+apply(case_tac b, simp, case_tac aa)
-apply(rule contrapos_pp, simp+)
+apply(rule_tac disjI1)
-apply(frule less_equal, simp+)
+apply(simp only: tcopy_F10_loop.simps)
-apply(drule length_cons_same, auto)
+apply(erule_tac exE)+
-apply(drule replicate_set_equal, simp+)
+apply(rule_tac x = i in exI, rule_tac x = j in exI,
-done
+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)
-lemma less_equal2: "\<not> (n::nat) \<le> m \<Longrightarrow> \<exists>x. n = x + m & x > 0"
+apply(case_tac i, simp_all add: exp_ind_def exp_zero)
-apply(rule_tac x = "n - m" in exI)
+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)
-done
+apply(simp add: exp_ind_def)
+done
-lemma replicate_tail_length[dest]:
-"\<lbrakk>rev b @ Bk # list = xs @ replicate n Bk @ replicate n Oc\<rbrakk>
+(*
-\<Longrightarrow> length list >= n"
+lemma false_case4: "\<lbrakk>i + (k + t) = Suc x;
-apply(rule contrapos_pp, simp+)
+0 < i;
-apply(drule less_equal2, auto)
+Bk # list = Oc\<^bsup>t\<^esup>;
-apply(drule rev_equal)
+\<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>));
-apply(simp add: replicate_add)
+0 < k\<rbrakk>
-apply(auto)
+\<Longrightarrow> RR"
-apply(case_tac x, simp+)
+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(case_tac x)
+apply(auto simp:tcopy_def
-apply(auto simp:tcopy_F10.simps tcopy_F9.simps tcopy_def
+tstep.simps fetch.simps new_tape.simps exp_zero_simp
-tstep.simps fetch.simps new_tape.simps
+exp_zero_simp2
 split: if_splits list.splits block.splits)
-apply(rule_tac x = n in exI, auto)
+apply(case_tac "hd b", simp add:tcopy_F9.simps tcopy_F10.simps )
-apply(case_tac b, simp+)
+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(case_tac x)
+apply(auto simp: tcopy_F9.simps tcopy_def
-apply(simp_all add: tcopy_F9.simps tcopy_def
+tstep.simps fetch.simps new_tape.simps exp_zero_simp exp_zero_simp2
-tstep.simps fetch.simps new_tape.simps
+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 [!] k, simp_all add: exp_ind_def exp_zero)
-apply(case_tac b, simp+)
+apply(erule_tac [!] x = i in allE, simp)
-apply(rule contrapos_pp, simp+)
+apply(erule_tac false_case7, simp_all)+
-apply(drule less_equal, simp+)
+apply(case_tac t, simp_all add: exp_zero exp_ind_def)
-apply(drule rev_equal, auto)
+apply(erule_tac false_case7, simp_all)+
-apply(case_tac "length list", simp+)
+apply(erule_tac false_case8, simp_all)
-done
+apply(erule_tac false_case7, simp_all)+
+apply(case_tac t, simp_all add: exp_ind_def exp_zero)
-lemma app_cons_app_simp: "xs @ a # bs @ ys = (xs @ [a]) @ bs @ ys"
+apply(erule_tac false_case7, simp_all)
-apply(simp)
+apply(erule_tac false_case8, simp_all)
-done
+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(case_tac x)
 apply(auto simp:tcopy_F8.simps tcopy_F9.simps tcopy_def
-tstep.simps fetch.simps new_tape.simps
+tstep.simps fetch.simps new_tape.simps tcopy_F9_loop.simps
+tcopy_F9_exit.simps
 split: if_splits list.splits block.splits)
-apply(rule_tac x = "Suc n" in exI, auto)
+apply(case_tac [!] t, simp_all add: exp_ind_def exp_zero)
-apply(rule_tac x = "n" in exI, auto)
+apply(rule_tac x = i in exI)
-apply(simp only: app_cons_app_simp)
+apply(rule_tac x = "Suc k" in exI, simp)
-apply(frule replicate_tail_length, 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(case_tac x)
+apply(auto simp:tcopy_F8.simps tcopy_def tstep.simps
-apply(simp_all add:tcopy_F8.simps tcopy_def tstep.simps
+fetch.simps new_tape.simps exp_zero_simp exp_zero split: if_splits list.splits
-fetch.simps new_tape.simps)
-apply(simp split: if_splits list.splits block.splits)
+block.splits)
-apply(rule_tac x = "n" in exI, auto)
+apply(rule_tac x = i in exI, rule_tac x = "k + t" in exI, simp)
-done
+apply(rule_tac x = "Suc k" in exI, simp)
+apply(rule_tac x = "t - 1" in exI, simp)
-lemma ex_less_more: "\<lbrakk>(x::nat) >= m ; x <= n\<rbrakk> \<Longrightarrow>
+apply(case_tac t, simp_all add: exp_zero exp_ind_def)
-\<exists>y. x = m + y & y <= n - m"
+done
-by(rule_tac x = "x -m" in exI, auto)
-lemma replicate_split: "x <= n \<Longrightarrow>
-(\<exists>y. replicate n b = replicate (y + x) b)"
-apply(rule_tac x = "n - x" in exI)
-apply(simp)
-done
-lemma app_app_app_app_simp: "as @ bs @ cs @ ds =
-(as @ bs) @ (cs @ ds)"
-by simp
-lemma lengthtailsame_append_elim:
-"\<lbrakk>as @ bs = cs @ ds; length bs = length ds\<rbrakk> \<Longrightarrow> bs = ds"
-apply(simp)
-done
-lemma rep_suc: "replicate (Suc n) x = replicate n x @ [x]"
-by(induct n, auto)
-lemma length_append_diff_cons:
-"\<lbrakk>b @ x # ba = xs @ replicate m y @ replicate n x; x \<noteq> y;
-Suc (length ba) \<le> m + n\<rbrakk>
-\<Longrightarrow> length ba < n"
-apply(induct n arbitrary: ba, simp)
-apply(drule_tac b = y in replicate_split,
-simp add: replicate_add, erule exE, simp del: replicate.simps)
-proof -
-fix ba ya
-assume h1:
-"b @ x # ba = xs @ y # replicate ya y @ replicate (length ba) y"
-and h2: "x \<noteq> y"
-thus "False"
-using append_eq_append_conv[of "b @ [x]"
-"xs @ y # replicate ya y" "ba" "replicate (length ba) y"]
-apply(auto)
-apply(case_tac ya, simp,
-simp add: rep_suc del: rep_suc_rev replicate.simps)
-done
-next
-fix n ba
-assume ind: "\<And>ba. \<lbrakk>b @ x # ba = xs @ replicate m y @ replicate n x;
-x \<noteq> y; Suc (length ba) \<le> m + n\<rbrakk>
-\<Longrightarrow> length ba < n"
-and h1: "b @ x # ba = xs @ replicate m y @ replicate (Suc n) x"
-and h2: "x \<noteq> y" and h3: "Suc (length ba) \<le> m + Suc n"
-show "length ba < Suc n"
-proof(cases "length ba")
-case 0 thus "?thesis" by simp
-next
-fix nat
-assume "length ba = Suc nat"
-hence "\<exists> ys a. ba = ys @ [a]"
-apply(rule_tac x = "butlast ba" in exI)
-apply(rule_tac x = "last ba" in exI)
-using append_butlast_last_id[of ba]
-apply(case_tac ba, auto)
-done
-from this obtain ys where "\<exists> a. ba = ys @ [a]" ..
-from this obtain a where "ba = ys @ [a]" ..
-thus "?thesis"
-using ind[of ys] h1 h2 h3
-apply(simp del: rep_suc_rev replicate.simps add: rep_suc)
-done
-qed
-qed
-lemma [elim]:
-"\<lbrakk>b @ Oc # ba = xs @ Bk # replicate n Bk @ replicate n Oc;
-Suc (length ba) \<le> 2 * n\<rbrakk>
-\<Longrightarrow> length ba < n"
-apply(rule_tac length_append_diff_cons[of b Oc ba xs "Suc n" Bk n])
-apply(simp, simp, simp)
-done
-lemma [elim]: "\<lbrakk>tstep (7, b, c) tcopy = (8, ab, ba);
-tcopy_F7 x (b, c)\<rbrakk> \<Longrightarrow> tcopy_F8 x (ab, ba)"
-apply(case_tac x)
-apply(simp_all add:tcopy_F8.simps tcopy_F7.simps
-tcopy_def tstep.simps fetch.simps new_tape.simps)
-apply(simp split: if_splits list.splits block.splits)
-apply(rule_tac x = "n" in exI, auto)
-done
 lemma [elim]: "\<lbrakk>tstep (7, b, c) tcopy = (7, ab, ba);
 tcopy_F7 x (b, c)\<rbrakk> \<Longrightarrow> tcopy_F7 x (ab, ba)"
-apply(case_tac x)
+apply(auto simp:tcopy_F7.simps tcopy_def tstep.simps fetch.simps
-apply(auto simp:tcopy_F7.simps tcopy_def tstep.simps
+new_tape.simps exp_ind_def exp_zero_simp
-fetch.simps new_tape.simps
+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 = "n" in exI, auto)
+apply(rule_tac x = i in exI, simp)
-apply(simp only: app_cons_app_simp)
+apply(rule_tac x =  "Suc 0" in exI, simp add: exp_ind_def exp_zero)
-apply(frule replicate_tail_length, simp)
+apply(rule_tac x = "j - 1" in exI, simp)
-done
+apply(case_tac t, simp_all add: exp_ind_def )
+apply(case_tac j, simp_all add: exp_ind_def exp_zero)
-lemma Suc_more: "n <= m \<Longrightarrow> Suc m - n = Suc (m - n)"
+done
-by simp
 lemma [elim]: "\<lbrakk>tstep (6, b, c) tcopy = (7, ab, ba);
 tcopy_F6 x (b, c)\<rbrakk> \<Longrightarrow> tcopy_F7 x (ab, ba)"
 apply(case_tac x)
 apply(auto simp:tcopy_F7.simps tcopy_F6.simps
-tcopy_def tstep.simps fetch.simps new_tape.simps
+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)
 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 = "Suc 0" in exI, simp add: exp_ind_def exp_zero)
-apply(rule_tac x = n in exI, simp)
+apply(rule_tac x = "Suc i" in exI, simp add: exp_ind_def)
-apply(drule Suc_more, simp)
-done
-lemma ex_less_more2: "\<lbrakk>(n::nat) < x ; x <= 2 * n\<rbrakk> \<Longrightarrow>
-\<exists>y. (x = n + y & y <= n)"
-apply(rule_tac x = "x - n" in exI)
-apply(auto)
-done
-lemma app_app_app_simp: "xs @ ys @ za = (xs @ ys) @ za"
-apply(simp)
-done
-lemma [elim]: "rev xs = replicate n b \<Longrightarrow> xs = replicate n b"
-using rev_replicate[of n b]
-thm rev_equal
-by(drule_tac rev_equal, simp)
-lemma app_cons_tail_same[dest]:
-"\<lbrakk>rev b @ Oc # list =
-replicate (Suc (Suc na) - n) Oc @ replicate n Bk @ replicate n Oc;
-Suc 0 < n; n \<le> Suc na; n < length list; length list \<le> 2 * n; b \<noteq> []\<rbrakk>
-\<Longrightarrow> list = replicate n Bk @ replicate n Oc
-& b = replicate (Suc na - n) Oc"
-using length_append_diff_cons[of "rev b" Oc list
-"replicate (Suc (Suc na) - n) Oc" n Bk n]
-apply(case_tac "length list = 2*n", simp)
-using append_eq_append_conv[of "rev b @ [Oc]" "replicate
-(Suc (Suc na) - n) Oc" "list" "replicate n Bk @ replicate n Oc"]
-apply(case_tac n, simp, simp add: Suc_more rep_suc
-del: rep_suc_rev replicate.simps, auto)
-done
-lemma hd_replicate_false1: "\<lbrakk>replicate x Oc \<noteq> [];
-hd (replicate x Oc) = Bk\<rbrakk> \<Longrightarrow> RR"
-apply(case_tac x, auto)
-done
-lemma hd_replicate_false2: "\<lbrakk>replicate x Oc \<noteq> [];
-hd (replicate x Oc) \<noteq> Oc\<rbrakk> \<Longrightarrow> RR"
-apply(case_tac x, auto)
-done
-lemma Suc_more_less: "\<lbrakk>n \<le> Suc m; n >= m\<rbrakk> \<Longrightarrow> n = m | n = Suc m"
-apply(auto)
-done
-lemma replicate_not_Nil: "replicate x a \<noteq> [] \<Longrightarrow> x > 0"
-apply(case_tac x, simp+)
 done
 lemma [elim]: "\<lbrakk>tstep (10, b, c) tcopy = (5, ab, ba);
 tcopy_F10 x (b, c)\<rbrakk> \<Longrightarrow> tcopy_F5 x (ab, ba)"
-apply(case_tac x)
 apply(auto simp:tcopy_F5.simps tcopy_F10.simps tcopy_def
-tstep.simps fetch.simps new_tape.simps
+tstep.simps fetch.simps new_tape.simps exp_zero_simp exp_zero_simp2
-split: if_splits list.splits block.splits)
+exp_ind_def tcopy_F10.simps tcopy_F10_loop.simps tcopy_F10_exit.simps
-apply(frule app_cons_tail_same, simp+)
+split: if_splits list.splits block.splits )
-apply(rule_tac x = n in exI, auto)
+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)
 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
+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
+exp_zero_simp exp_zero_simp2 exp_zero
 split: if_splits list.splits block.splits)
-apply(frule replicate_cons_same, auto)
+apply(rule_tac x = "Suc i" in exI, simp add: exp_ind_def exp_zero)
-apply(simp add: replicate_app_Cons_same)
+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(auto simp:tcopy_F1.simps tcopy_F2.simps
-apply(simp_all add:tcopy_F2.simps tcopy_F1.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
-apply(auto)
+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)
+tcopy_def tstep.simps fetch.simps new_tape.simps
-done
+exp_zero_simp exp_zero_simp2 exp_zero
+split: if_splits list.splits block.splits )
-lemma ex_less: "Suc x <= y \<Longrightarrow> \<exists>z. y = x + z & z > 0"
+apply(case_tac x, simp_all add: exp_ind_def exp_zero, auto)
-apply(rule_tac x = "y - x" in exI, auto)
-done
-lemma [elim]: "\<lbrakk>xs @ Bk # ba =
-Bk # Oc # replicate n Oc @ Bk # Oc # replicate n Oc;
-length xs \<le> Suc n; xs \<noteq> []\<rbrakk> \<Longrightarrow> RR"
-apply(case_tac xs, auto)
-apply(case_tac list, auto)
-apply(drule ex_less, auto)
-apply(simp add: replicate_add)
-apply(auto)
-apply(case_tac z, simp+)
 done
 lemma [elim]: "\<lbrakk>tstep (15, b, c) tcopy = (0, ab, ba);
 tcopy_F15 x (b, c)\<rbrakk> \<Longrightarrow> tcopy_F0 x (ab, ba)"
-apply(case_tac x)
 apply(auto simp: tcopy_F15.simps tcopy_F0.simps
 tcopy_def tstep.simps new_tape.simps fetch.simps
 split: if_splits list.splits block.splits)
-done
+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
 text {*
 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)
 apply(drule_tac inv_tcopy_step, simp add: tstep_red)
 done
-text {*
-The followng lemmas gives the parital correctness of Copying TM.
-*}
-theorem inv_tcopy_rs:
-"steps (Suc 0, [], replicate x Oc) tcopy stp = (0, l, r)
-\<Longrightarrow> \<exists> n. l = replicate n Bk \<and>
-r = replicate x Oc @ Bk # replicate x Oc"
-apply(insert inv_tcopy_steps[of x stp])
-apply(auto simp: inv_tcopy.simps tcopy_F0.simps isBk.simps)
-done
 (*----------halt problem of tcopy----------------------------------------*)
 apply(simp add: tstep.simps tcopy_def tcopy_LE_def lex_square_def
 lex_triple_def lex_pair_def tcopy_phase.simps tcopy_stage.simps
 tcopy_state.simps tcopy_step.simps)
 apply(simp split: if_splits list.splits block.splits taction.splits)
 apply(auto)
-apply(case_tac x, simp+)
 done
 lemma [elim]: "tcopy_F4 x (b, c) \<Longrightarrow>
 (tstep (4, b, c) tcopy, 4, b, c) \<in> tcopy_LE"
 apply(case_tac x, simp)
 apply(simp add: tcopy_F4.simps tstep.simps tcopy_def tcopy_LE_def
 lex_square_def lex_triple_def lex_pair_def tcopy_phase.simps
 tcopy_stage.simps tcopy_state.simps tcopy_step.simps)
 apply(simp split: if_splits list.splits block.splits taction.splits)
-apply(auto)
+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)
 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)
+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)
+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)
+apply(auto simp: exp_zero_simp)
 apply(simp_all add: tcopy_phase.simps tcopy_stage.simps
-tcopy_state.simps tcopy_step.simps)
+tcopy_state.simps tcopy_step.simps exponent_def)
-apply(simp only: app_cons_app_simp, frule replicate_tail_length, simp)
+done
-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"
 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(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
+apply(simp_all add: tcopy_phase.simps tcopy_stage.simps  tcopy_F9_loop.simps
-tcopy_state.simps tcopy_step.simps)
+tcopy_state.simps tcopy_step.simps tstep.simps exp_zero_simp
-apply(drule_tac bs = b and as = "Bk # list" in rev_tl_hd_merge)
+exponent_def)
-apply(simp)
+apply(case_tac [1-2] t, simp_all add: rev_tl_hd_merge)
-apply(drule_tac bs = b and as = "Oc # list" in rev_tl_hd_merge)
+apply(case_tac j, simp, simp)
-apply(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)
+tcopy_state.simps tcopy_step.simps exponent_def
-apply(drule_tac bs = b and as = "Bk # list" in rev_tl_hd_merge)
+rev_tl_hd_merge)
-apply(simp)
+apply(case_tac k, simp_all)
-apply(drule_tac bs = b and as = "Oc # list" in rev_tl_hd_merge)
+apply(case_tac nat, simp_all)
-apply(simp)
 done
 lemma [elim]: "tcopy_F11 x (b, c) \<Longrightarrow>
 (tstep (11, b, c) tcopy, 11, b, c) \<in> tcopy_LE"
 apply(case_tac x, simp)
 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)
 lex_triple_def lex_pair_def tcopy_phase.simps)
 apply(simp split: if_splits list.splits block.splits taction.splits)
 apply(auto)
 apply(simp_all add: tcopy_phase.simps tcopy_stage.simps
 tcopy_state.simps tcopy_step.simps)
-apply(drule equal_length, simp)+
 done
 lemma [elim]: "tcopy_F14 x (b, c) \<Longrightarrow>
 (tstep (14, b, c) tcopy, 14, b, c) \<in> tcopy_LE"
 apply(case_tac x, simp)
 apply(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, [], replicate x Oc) tcopy n in
+"\<forall>n. let nc = steps (Suc 0, [], Oc\<^bsup>x\<^esup>) tcopy n in
-let Sucnc = steps (Suc 0, [], replicate x Oc) tcopy (Suc 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"
 using h
 by(rule_tac tcopy_wf_step, auto simp: isS0_def)
 text {*
 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)
 apply(simp)
 done
 text {*
 The total correntess of Copying TM:
 *}
-theorem tcopy_halt_rs: "\<exists>stp m.
+theorem tcopy_halt_rs:
-steps (Suc 0, [], replicate x Oc) tcopy stp =
+"\<exists>stp m.
-(0, replicate m Bk, replicate x Oc @ Bk # replicate x Oc)"
+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)"
+assume h: "isS0 (steps (Suc 0, [], Oc\<^bsup>x\<^esup>) tcopy n)"
-have "inv_tcopy x (steps (Suc 0, [], replicate x Oc) 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
 section {*
 The {\em Dithering} Turing Machine
 -- {*
 The following two assumptions specifies that @{text "H"} does solve the Halting problem.
 *}
 and h_case:
 "\<And> M n. \<lbrakk>(haltP M n)\<rbrakk> \<Longrightarrow>
-\<exists> na nb. (steps (Suc 0, Bk\<^bsup>x\<^esup>, Oc\<^bsup>code M\<^esup> @ Bk # Oc\<^bsup>n\<^esup>) H na = (0, Bk\<^bsup>nb\<^esup>, [Oc]))"
+\<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
 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)
 let ?Q2 = "\<lambda> (l, r). (\<exists> nd. l = Bk\<^bsup>nd \<^esup>\<and> r = [Oc])"
 let ?P3 = "\<lambda> tp. False"
 assume h: "haltP (tcontra H) (code (tcontra H))"
 hence h1: "\<And> x. \<exists> na nb. steps (Suc 0, Bk\<^bsup>x\<^esup>, Oc\<^bsup>code (tcontra H)\<^esup> @ Bk #
 Oc\<^bsup>code (tcontra H)\<^esup>) H na = (0, Bk\<^bsup>nb\<^esup>, [Oc])"
-by(drule_tac x = x in h_case, simp)
+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>)"
 proof -
 let ?cn = "code (tcontra H)"
 have h1: "\<And> x. \<exists> na nb. steps (Suc 0, Bk\<^bsup>x\<^esup>, Oc\<^bsup>?cn\<^esup> @ Bk # Oc\<^bsup>?cn\<^esup>)
 H na = (0, Bk\<^bsup>nb\<^esup>, [Oc, Oc])"
 using uh
-by(drule_tac x = x in nh_case, simp)
+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

changeset 37	c9b689bb4156
parent 0	aa8656a8dbef