(* Title: Turing machines Author: Xu Jian <xujian817@hotmail.com> Maintainer: Xu Jian*)theory turing_basicimports Mainbeginsection {* Basic definitions of Turing machine *}datatype action = W0 | W1 | L | R | Nopdatatype cell = Bk | Octype_synonym tape = "cell list \<times> cell list"type_synonym state = nattype_synonym instr = "action \<times> state"type_synonym tprog = "instr list \<times> nat"type_synonym tprog0 = "instr list"type_synonym config = "state \<times> tape"fun nth_of where "nth_of xs i = (if i \<ge> length xs then None else Some (xs ! i))"lemma nth_of_map [simp]: shows "nth_of (map f p) n = (case (nth_of p n) of None \<Rightarrow> None | Some x \<Rightarrow> Some (f x))"apply(induct p arbitrary: n)apply(auto)apply(case_tac n)apply(auto)donefun fetch :: "instr list \<Rightarrow> state \<Rightarrow> cell \<Rightarrow> instr"where "fetch p 0 b = (Nop, 0)"| "fetch p (Suc s) Bk = (case nth_of p (2 * s) of Some i \<Rightarrow> i | None \<Rightarrow> (Nop, 0))"|"fetch p (Suc s) Oc = (case nth_of p ((2 * s) + 1) of Some i \<Rightarrow> i | None \<Rightarrow> (Nop, 0))"lemma fetch_Nil [simp]: shows "fetch [] s b = (Nop, 0)"apply(case_tac s)apply(auto)apply(case_tac b)apply(auto)donefun update :: "action \<Rightarrow> tape \<Rightarrow> tape"where "update W0 (l, r) = (l, Bk # (tl r))" | "update W1 (l, r) = (l, Oc # (tl r))"| "update L (l, r) = (if l = [] then ([], Bk # r) else (tl l, (hd l) # r))" | "update R (l, r) = (if r = [] then (Bk # l, []) else ((hd r) # l, tl r))" | "update Nop (l, r) = (l, r)"abbreviation "read r == if (r = []) then Bk else hd r"fun step :: "config \<Rightarrow> tprog \<Rightarrow> config" where "step (s, l, r) (p, off) = (let (a, s') = fetch p (s - off) (read r) in (s', update a (l, r)))"fun steps :: "config \<Rightarrow> tprog \<Rightarrow> nat \<Rightarrow> config" where "steps c p 0 = c" | "steps c p (Suc n) = steps (step c p) p n"abbreviation "step0 c p \<equiv> step c (p, 0)"abbreviation "steps0 c p n \<equiv> steps c (p, 0) n"lemma step_red [simp]: shows "steps c p (Suc n) = step (steps c p n) p"by (induct n arbitrary: c) (auto)lemma steps_add [simp]: shows "steps c p (m + n) = steps (steps c p m) p n"by (induct m arbitrary: c) (auto)lemma step_0 [simp]: shows "step (0, (l, r)) p = (0, (l, r))"by (case_tac p, simp)lemma steps_0 [simp]: shows "steps (0, (l, r)) p n = (0, (l, r))"by (induct n) (simp_all)fun is_final :: "config \<Rightarrow> bool"where "is_final (s, l, r) = (s = 0)"lemma is_final_eq: shows "is_final (s, tp) = (s = 0)"by (case_tac tp) (auto)lemma is_final_steps: assumes "is_final (s, l, r)" shows "is_final (steps (s, l, r) (p, off) n)"using assms by (induct n) (auto)(* if the machine is in the halting state, there must have been a state just before the halting state *)lemma before_final: assumes "steps0 (1, tp) A n = (0, tp')" shows "\<exists> n'. \<not> is_final (steps0 (1, tp) A n') \<and> steps0 (1, tp) A (Suc n') = (0, tp')"using assmsproof(induct n arbitrary: tp') case (0 tp') have asm: "steps0 (1, tp) A 0 = (0, tp')" by fact then show "\<exists>n'. \<not> is_final (steps0 (1, tp) A n') \<and> steps0 (1, tp) A (Suc n') = (0, tp')" by simpnext case (Suc n tp') have ih: "\<And>tp'. steps0 (1, tp) A n = (0, tp') \<Longrightarrow> \<exists>n'. \<not> is_final (steps0 (1, tp) A n') \<and> steps0 (1, tp) A (Suc n') = (0, tp')" by fact have asm: "steps0 (1, tp) A (Suc n) = (0, tp')" by fact obtain s l r where cases: "steps0 (1, tp) A n = (s, l, r)" by (auto intro: is_final.cases) then show "\<exists>n'. \<not> is_final (steps0 (1, tp) A n') \<and> steps0 (1, tp) A (Suc n') = (0, tp')" proof (cases "s = 0") case True (* in halting state *) then have "steps0 (1, tp) A n = (0, tp')" using asm cases by (simp del: steps.simps) then show ?thesis using ih by simp next case False (* not in halting state *) then have "\<not> is_final (steps0 (1, tp) A n) \<and> steps0 (1, tp) A (Suc n) = (0, tp')" using asm cases by simp then show ?thesis by auto qedqed(* well-formedness of Turing machine programs *)fun tm_wf :: "tprog \<Rightarrow> bool"where "tm_wf (p, off) = (length p \<ge> 2 \<and> length p mod 2 = 0 \<and> (\<forall>(a, s) \<in> set p. s \<le> length p div 2 + off \<and> s \<ge> off))"lemma halt_lemma: "\<lbrakk>wf LE; \<forall>n. (\<not> P (f n) \<longrightarrow> (f (Suc n), (f n)) \<in> LE)\<rbrakk> \<Longrightarrow> \<exists>n. P (f n)"by (metis wf_iff_no_infinite_down_chain)abbreviation exponent :: "'a \<Rightarrow> nat \<Rightarrow> 'a list" ("_ \<up> _" [100, 99] 100) where "x \<up> n == replicate n x"consts tape_of :: "'a \<Rightarrow> cell list" ("<_>" 100)fun tape_of_nat_list :: "nat list \<Rightarrow> cell list" where "tape_of_nat_list [] = []" | "tape_of_nat_list [n] = Oc\<up>(Suc n)" | "tape_of_nat_list (n#ns) = Oc\<up>(Suc n) @ Bk # (tape_of_nat_list ns)"defs (overloaded) tape_of_nl_abv: "<am> \<equiv> tape_of_nat_list am" tape_of_nat_abv : "<(n::nat)> \<equiv> Oc\<up>(Suc n)"definition tinres :: "cell list \<Rightarrow> cell list \<Rightarrow> bool" where "tinres xs ys = (\<exists>n. xs = ys @ Bk \<up> n \<or> ys = xs @ Bk \<up> n)"fun shift :: "instr list \<Rightarrow> nat \<Rightarrow> instr list"where "shift p n = (map (\<lambda> (a, s). (a, (if s = 0 then 0 else s + n))) p)"fun adjust :: "instr list \<Rightarrow> instr list"where "adjust p = map (\<lambda> (a, s). (a, if s = 0 then (Suc (length p div 2)) else s)) p"lemma length_shift [simp]: shows "length (shift p n) = length p"by simplemma length_adjust [simp]: shows "length (adjust p) = length p"by (induct p) (auto)(* composition of two Turing machines *)fun tm_comp :: "instr list \<Rightarrow> instr list \<Rightarrow> instr list" ("_ |+| _" [0, 0] 100)where "tm_comp p1 p2 = ((adjust p1) @ (shift p2 (length p1 div 2)))"lemma tm_comp_length: shows "length (A |+| B) = length A + length B"by autolemma tm_comp_pre_eq_step: assumes unfinal: "\<not> is_final (step0 c A)" shows "step0 c (A |+| B) = step0 c A"proof - obtain s l r where eq: "c = (s, l, r)" by (metis is_final.cases) have "\<not> is_final (step0 (s, l, r) A)" using unfinal eq by simp then have "case (fetch A s (read r)) of (a, s) \<Rightarrow> s \<noteq> 0" by (auto simp add: is_final_eq) then have "fetch (A |+| B) s (read r) = fetch A s (read r)" apply(case_tac [!] "read r") apply(case_tac [!] s) apply(auto simp: tm_comp_length nth_append) done then show "step0 c (A |+| B) = step0 c A" by (simp add: eq) qedlemma tm_comp_pre_eq: assumes "\<not> is_final (steps0 (1, tp) A n)" shows "steps0 (1, tp) (A |+| B) n = steps0 (1, tp) A n"using assmsproof(induct n) case 0 then show "steps0 (1, tp) (A |+| B) 0 = steps0 (1, tp) A 0" by autonext case (Suc n) have ih: "\<not> is_final (steps0 (1, tp) A n) \<Longrightarrow> steps0 (1, tp) (A |+| B) n = steps0 (1, tp) A n" by fact have fin: "\<not> is_final (steps0 (1, tp) A (Suc n))" by fact then have fin1: "\<not> is_final (step0 (steps0 (1, tp) A n) A)" by (auto simp only: step_red) then have fin2: "\<not> is_final (steps0 (1, tp) A n)" by (metis is_final_eq step_0 surj_pair) have "steps0 (1, tp) (A |+| B) (Suc n) = step0 (steps0 (1, tp) (A |+| B) n) (A |+| B)" by (simp only: step_red) also have "... = step0 (steps0 (1, tp) A n) (A |+| B)" by (simp only: ih[OF fin2]) also have "... = step0 (steps0 (1, tp) A n) A" by (simp only: tm_comp_pre_eq_step[OF fin1]) finally show "steps0 (1, tp) (A |+| B) (Suc n) = steps0 (1, tp) A (Suc n)" by (simp only: step_red)qeddeclare steps.simps[simp del]declare tm_comp.simps [simp del] adjust.simps[simp del] shift.simps[simp del]declare tm_wf.simps[simp del] step.simps[simp del]lemma tmcomp_fetch_in_first2: assumes "fetch A a x = (ac, 0)" "tm_wf (A, 0)" "a \<le> length A div 2" "a > 0" shows "fetch (A |+| B) a x = (ac, Suc (length A div 2))"using assmsapply(case_tac a, case_tac [!] x, auto simp: tm_comp_length tm_comp.simps length_adjust nth_append)apply(simp_all add: adjust.simps)donelemma tmcomp_exec_after_first: "\<lbrakk>0 < a; step (a, b, c) (A, 0) = (0, tp'); tm_wf (A, 0); a \<le> length A div 2\<rbrakk> \<Longrightarrow> step (a, b, c) (A |+| B, 0) = (Suc (length A div 2), tp')"apply(simp add: step.simps, auto)apply(case_tac "fetch A a Bk", simp add: tmcomp_fetch_in_first2)apply(case_tac "fetch A a (hd c)", simp add: tmcomp_fetch_in_first2)donelemma step_nothalt_pre: "\<lbrakk>step (aa, ba, ca) (A, 0) = (a, b, c); 0 < a\<rbrakk> \<Longrightarrow> 0 < aa"apply(case_tac "aa = 0", simp add: step_0, simp)donelemma nth_in_set: "\<lbrakk> A ! i = x; i < length A\<rbrakk> \<Longrightarrow> x \<in> set A"by autolemma step_nothalt: "\<lbrakk>step (aa, ba, ca) (A, 0) = (a, b, c); 0 < a; tm_wf (A, 0)\<rbrakk> \<Longrightarrow> a \<le> length A div 2"apply(simp add: step.simps)apply(case_tac aa, case_tac [!] aa, auto split: if_splits simp: tm_wf.simps)apply(case_tac "A ! (2 * nat)", simp)apply(erule_tac x = "(aa, a)" in ballE, simp_all add: nth_in_set)apply(case_tac "hd ca", auto split: if_splits simp: tm_wf.simps)apply(case_tac "A ! (2 * nat)", simp)apply(erule_tac x = "(aa, a)" in ballE, simp_all add: nth_in_set)apply(case_tac "A ! (Suc (2 * nat))")apply(erule_tac x = "(aa,bb)" in ballE, simp_all add: nth_in_set)donelemma steps_in_range: " \<lbrakk>0 < a; steps (Suc 0, tp) (A, 0) stp = (a, b, c); tm_wf (A, 0)\<rbrakk> \<Longrightarrow> a \<le> length A div 2"proof(induct stp arbitrary: a b c) fix a b c assume h: "0 < a" "steps (Suc 0, tp) (A, 0) 0 = (a, b, c)" "tm_wf (A, 0)" thus "a \<le> length A div 2" apply(simp add: steps.simps tm_wf.simps, auto) donenext fix stp a b c assume ind: "\<And>a b c. \<lbrakk>0 < a; steps (Suc 0, tp) (A, 0) stp = (a, b, c); tm_wf (A, 0)\<rbrakk> \<Longrightarrow> a \<le> length A div 2" and h: "0 < a" "steps (Suc 0, tp) (A, 0) (Suc stp) = (a, b, c)" "tm_wf (A, 0)" from h show "a \<le> length A div 2" proof(simp add: step_red, case_tac "(steps (Suc 0, tp) (A, 0) stp)", simp) fix aa ba ca assume g: "step (aa, ba, ca) (A, 0) = (a, b, c)" "steps (Suc 0, tp) (A, 0) stp = (aa, ba, ca)" hence "aa \<le> length A div 2" apply(rule_tac ind, auto simp: h step_nothalt_pre) done thus "?thesis" using g h apply(rule_tac step_nothalt, auto) done qedqedlemma t_merge_pre_halt_same: assumes a_ht: "steps (1, tp) (A, 0) n = (0, tp')" and a_wf: "tm_wf (A, 0)" obtains n' where "steps (1, tp) (A |+| B, 0) n' = (Suc (length A div 2), tp')"proof - assume a: "\<And>n. steps (1, tp) (A |+| B, 0) n = (Suc (length A div 2), tp') \<Longrightarrow> thesis" obtain stp' where "\<not> is_final (steps (1, tp) (A, 0) stp')" and "steps (1, tp) (A, 0) (Suc stp') = (0, tp')" using a_ht before_final by blast then have "steps (1, tp) (A |+| B, 0) (Suc stp') = (Suc (length A div 2), tp')" proof(simp add: step_red) assume "\<not> is_final (steps (Suc 0, tp) (A, 0) stp')" " step (steps (Suc 0, tp) (A, 0) stp') (A, 0) = (0, tp')" moreover hence "(steps0 (1, tp) (A |+| B) stp') = (steps0 (1, tp) A stp')" apply(rule_tac tm_comp_pre_eq) apply(simp_all add: a_ht) done ultimately show "step (steps (Suc 0, tp) (A |+| B, 0) stp') (A |+| B, 0) = (Suc (length A div 2), tp')" apply(case_tac " steps (Suc 0, tp) (A, 0) stp'", simp) apply(rule tmcomp_exec_after_first, simp_all add: a_wf) apply(erule_tac steps_in_range, auto simp: a_wf) done qed with a show thesis by blastqedlemma tm_comp_fetch_second_zero: "\<lbrakk>fetch B sa' x = (a, 0); tm_wf (A, 0); tm_wf (B, 0); sa' > 0\<rbrakk> \<Longrightarrow> fetch (A |+| B) (sa' + (length A div 2)) x = (a, 0)"apply(case_tac x)apply(case_tac [!] sa', auto simp: fetch.simps tm_comp_length length_adjust nth_append tm_comp.simps tm_wf.simps shift.simps split: if_splits)done lemma tm_comp_fetch_second_inst: "\<lbrakk>sa > 0; s > 0; tm_wf (A, 0); tm_wf (B, 0); fetch B sa x = (a, s)\<rbrakk> \<Longrightarrow> fetch (A |+| B) (sa + length A div 2) x = (a, s + length A div 2)"apply(case_tac x)apply(case_tac [!] sa, auto simp: fetch.simps tm_comp_length length_adjust nth_append tm_comp.simps tm_wf.simps shift.simps split: if_splits)done lemma t_merge_second_same: assumes a_wf: "tm_wf (A, 0)" and b_wf: "tm_wf (B, 0)" and steps: "steps (Suc 0, l, r) (B, 0) stp = (s, l', r')" shows "steps (Suc (length A div 2), l, r) (A |+| B, 0) stp = (if s = 0 then 0 else s + length A div 2, l', r')"using a_wf b_wf stepsproof(induct stp arbitrary: s l' r', simp add: steps.simps, simp) fix stpa sa l'a r'a assume ind: "\<And>s l' r'. steps (Suc 0, l, r) (B, 0) stpa = (s, l', r') \<Longrightarrow> steps (Suc (length A div 2), l, r) (A |+| B, 0) stpa = (if s = 0 then 0 else s + length A div 2, l', r')" and h: "step (steps (Suc 0, l, r) (B, 0) stpa) (B, 0) = (sa, l'a, r'a)" obtain sa' l'' r'' where a: "(steps (Suc 0, l, r) (B, 0) stpa) = (sa', l'', r'')" apply(case_tac "steps (Suc 0, l, r) (B, 0) stpa", auto) done from this have b: "steps (Suc (length A div 2), l, r) (A |+| B, 0) stpa = (if sa' = 0 then 0 else sa' + length A div 2, l'', r'')" apply(erule_tac ind) done from a b h show "(sa = 0 \<longrightarrow> step (steps (Suc (length A div 2), l, r) (A |+| B, 0) stpa) (A |+| B, 0) = (0, l'a, r'a)) \<and> (0 < sa \<longrightarrow> step (steps (Suc (length A div 2), l, r) (A |+| B, 0) stpa) (A |+| B, 0) = (sa + length A div 2, l'a, r'a))" proof(case_tac "sa' = 0", auto) assume "step (sa', l'', r'') (B, 0) = (0, l'a, r'a)" "0 < sa'" thus "step (sa' + length A div 2, l'', r'') (A |+| B, 0) = (0, l'a, r'a)" using a_wf b_wf apply(simp add: step.simps) apply(case_tac "fetch B sa' (read r'')", auto) apply(simp_all add: step.simps tm_comp_fetch_second_zero) done next assume "step (sa', l'', r'') (B, 0) = (sa, l'a, r'a)" "0 < sa'" "0 < sa" thus "step (sa' + length A div 2, l'', r'') (A |+| B, 0) = (sa + length A div 2, l'a, r'a)" using a_wf b_wf apply(simp add: step.simps) apply(case_tac "fetch B sa' (read r'')", auto) apply(simp_all add: step.simps tm_comp_fetch_second_inst) done qedqedlemma t_merge_second_halt_same: "\<lbrakk>tm_wf (A, 0); tm_wf (B, 0); steps (1, l, r) (B, 0) stp = (0, l', r')\<rbrakk> \<Longrightarrow> steps (Suc (length A div 2), l, r) (A |+| B, 0) stp = (0, l', r')"using t_merge_second_same[where s = "0"]apply(auto)doneend