diff -r a63c3f8d7234 -r 67063c5365e1 thys/turing_basic.thy --- a/thys/turing_basic.thy Thu Feb 07 06:39:06 2013 +0000 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,428 +0,0 @@ -(* Title: Turing machines - Author: Xu Jian - Maintainer: Xu Jian -*) - -theory turing_basic -imports Main -begin - -section {* Basic definitions of Turing machine *} - -datatype action = W0 | W1 | L | R | Nop - -datatype cell = Bk | Oc - -type_synonym tape = "cell list \ cell list" - -type_synonym state = nat - -type_synonym instr = "action \ state" - -type_synonym tprog = "instr list \ nat" - -type_synonym tprog0 = "instr list" - -type_synonym config = "state \ tape" - -fun nth_of where - "nth_of xs i = (if i \ 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 \ None | Some x \ Some (f x))" -apply(induct p arbitrary: n) -apply(auto) -apply(case_tac n) -apply(auto) -done - -fun - fetch :: "instr list \ state \ cell \ instr" -where - "fetch p 0 b = (Nop, 0)" -| "fetch p (Suc s) Bk = - (case nth_of p (2 * s) of - Some i \ i - | None \ (Nop, 0))" -|"fetch p (Suc s) Oc = - (case nth_of p ((2 * s) + 1) of - Some i \ i - | None \ (Nop, 0))" - -lemma fetch_Nil [simp]: - shows "fetch [] s b = (Nop, 0)" -apply(case_tac s) -apply(auto) -apply(case_tac b) -apply(auto) -done - -fun - update :: "action \ tape \ 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 \ tprog \ 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 \ tprog \ nat \ config" - where - "steps c p 0 = c" | - "steps c p (Suc n) = steps (step c p) p n" - - -abbreviation - "step0 c p \ step c (p, 0)" - -abbreviation - "steps0 c p n \ 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 \ 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 after_is_final: - assumes "is_final c" - shows "is_final (steps c p n)" -using assms -apply(induct n) -apply(case_tac [!] c) -apply(auto) -done - -lemma not_is_final: - assumes a: "\ is_final (steps c p n1)" - and b: "n2 \ n1" - shows "\ is_final (steps c p n2)" -proof (rule notI) - obtain n3 where eq: "n1 = n2 + n3" using b by (metis le_iff_add) - assume "is_final (steps c p n2)" - then have "is_final (steps c p n1)" unfolding eq - by (simp add: after_is_final) - with a show "False" by simp -qed - -(* 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 "\ n'. \ is_final (steps0 (1, tp) A n') \ steps0 (1, tp) A (Suc n') = (0, tp')" -using assms -proof(induct n arbitrary: tp') - case (0 tp') - have asm: "steps0 (1, tp) A 0 = (0, tp')" by fact - then show "\n'. \ is_final (steps0 (1, tp) A n') \ steps0 (1, tp) A (Suc n') = (0, tp')" - by simp -next - case (Suc n tp') - have ih: "\tp'. steps0 (1, tp) A n = (0, tp') \ - \n'. \ is_final (steps0 (1, tp) A n') \ 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 "\n'. \ is_final (steps0 (1, tp) A n') \ 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 "\ is_final (steps0 (1, tp) A n) \ steps0 (1, tp) A (Suc n) = (0, tp')" - using asm cases by simp - then show ?thesis by auto - qed -qed - -(* well-formedness of Turing machine programs *) -abbreviation "is_even n \ (n::nat) mod 2 = 0" - -fun - tm_wf :: "tprog \ bool" -where - "tm_wf (p, off) = (length p \ 2 \ is_even (length p) \ - (\(a, s) \ set p. s \ length p div 2 + off \ s \ off))" - -abbreviation - "tm_wf0 p \ tm_wf (p, 0)" - -abbreviation exponent :: "'a \ nat \ 'a list" ("_ \ _" [100, 99] 100) - where "x \ n == replicate n x" - -consts tape_of :: "'a \ cell list" ("<_>" 100) - -defs (overloaded) - tape_of_nat_abv: "<(n::nat)> \ Oc \ (Suc n)" - -fun tape_of_nat_list :: "'a list \ cell list" - where - "tape_of_nat_list [] = []" | - "tape_of_nat_list [n] = " | - "tape_of_nat_list (n#ns) = @ Bk # (tape_of_nat_list ns)" - -fun tape_of_nat_pair :: "'a \ 'b \ cell list" - where - "tape_of_nat_pair (n, m) = @ [Bk] @ " - - -defs (overloaded) - tape_of_nl_abv: "<(ns::'a list)> \ tape_of_nat_list ns" - tape_of_nat_pair: "<(np::'a\'b)> \ tape_of_nat_pair np" - -fun - shift :: "instr list \ nat \ instr list" -where - "shift p n = (map (\ (a, s). (a, (if s = 0 then 0 else s + n))) p)" - -fun - adjust :: "instr list \ instr list" -where - "adjust p = map (\ (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 simp - -lemma length_adjust [simp]: - shows "length (adjust p) = length p" -by (induct p) (auto) - - -(* composition of two Turing machines *) -fun - tm_comp :: "instr list \ instr list \ 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 auto - -lemma tm_comp_wf[intro]: - "\tm_wf (A, 0); tm_wf (B, 0)\ \ tm_wf (A |+| B, 0)" -by (auto simp: tm_wf.simps shift.simps adjust.simps tm_comp_length tm_comp.simps) - - -lemma tm_comp_step: - assumes unfinal: "\ 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 "\ is_final (step0 (s, l, r) A)" using unfinal eq by simp - then have "case (fetch A s (read r)) of (a, s) \ s \ 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) -qed - -lemma tm_comp_steps: - assumes "\ is_final (steps0 c A n)" - shows "steps0 c (A |+| B) n = steps0 c A n" -using assms -proof(induct n) - case 0 - then show "steps0 c (A |+| B) 0 = steps0 c A 0" by auto -next - case (Suc n) - have ih: "\ is_final (steps0 c A n) \ steps0 c (A |+| B) n = steps0 c A n" by fact - have fin: "\ is_final (steps0 c A (Suc n))" by fact - then have fin1: "\ is_final (step0 (steps0 c A n) A)" - by (auto simp only: step_red) - then have fin2: "\ is_final (steps0 c A n)" - by (metis is_final_eq step_0 surj_pair) - - have "steps0 c (A |+| B) (Suc n) = step0 (steps0 c (A |+| B) n) (A |+| B)" - by (simp only: step_red) - also have "... = step0 (steps0 c A n) (A |+| B)" by (simp only: ih[OF fin2]) - also have "... = step0 (steps0 c A n) A" by (simp only: tm_comp_step[OF fin1]) - finally show "steps0 c (A |+| B) (Suc n) = steps0 c A (Suc n)" - by (simp only: step_red) -qed - -lemma tm_comp_fetch_in_A: - assumes h1: "fetch A s x = (a, 0)" - and h2: "s \ length A div 2" - and h3: "s \ 0" - shows "fetch (A |+| B) s x = (a, Suc (length A div 2))" -using h1 h2 h3 -apply(case_tac s) -apply(case_tac [!] x) -apply(auto simp: tm_comp_length nth_append) -done - -lemma tm_comp_exec_after_first: - assumes h1: "\ is_final c" - and h2: "step0 c A = (0, tp)" - and h3: "fst c \ length A div 2" - shows "step0 c (A |+| B) = (Suc (length A div 2), tp)" -using h1 h2 h3 -apply(case_tac c) -apply(auto simp del: tm_comp.simps) -apply(case_tac "fetch A a Bk") -apply(simp del: tm_comp.simps) -apply(subst tm_comp_fetch_in_A) -apply(auto)[4] -apply(case_tac "fetch A a (hd c)") -apply(simp del: tm_comp.simps) -apply(subst tm_comp_fetch_in_A) -apply(auto)[4] -done - -lemma step_in_range: - assumes h1: "\ is_final (step0 c A)" - and h2: "tm_wf (A, 0)" - shows "fst (step0 c A) \ length A div 2" -using h1 h2 -apply(case_tac c) -apply(case_tac a) -apply(auto simp add: prod_case_unfold Let_def) -apply(case_tac "hd c") -apply(auto simp add: prod_case_unfold) -done - -lemma steps_in_range: - assumes h1: "\ is_final (steps0 (1, tp) A stp)" - and h2: "tm_wf (A, 0)" - shows "fst (steps0 (1, tp) A stp) \ length A div 2" -using h1 -proof(induct stp) - case 0 - then show "fst (steps0 (1, tp) A 0) \ length A div 2" using h2 - by (auto simp add: steps.simps tm_wf.simps) -next - case (Suc stp) - have ih: "\ is_final (steps0 (1, tp) A stp) \ fst (steps0 (1, tp) A stp) \ length A div 2" by fact - have h: "\ is_final (steps0 (1, tp) A (Suc stp))" by fact - from ih h h2 show "fst (steps0 (1, tp) A (Suc stp)) \ length A div 2" - by (metis step_in_range step_red) -qed - -lemma tm_comp_pre_halt_same: - assumes a_ht: "steps0 (1, tp) A n = (0, tp')" - and a_wf: "tm_wf (A, 0)" - obtains n' where "steps0 (1, tp) (A |+| B) n' = (Suc (length A div 2), tp')" -proof - - assume a: "\n. steps (1, tp) (A |+| B, 0) n = (Suc (length A div 2), tp') \ thesis" - obtain stp' where fin: "\ is_final (steps0 (1, tp) A stp')" and h: "steps0 (1, tp) A (Suc stp') = (0, tp')" - using before_final[OF a_ht] by blast - from fin have h1:"steps0 (1, tp) (A |+| B) stp' = steps0 (1, tp) A stp'" - by (rule tm_comp_steps) - from h have h2: "step0 (steps0 (1, tp) A stp') A = (0, tp')" - by (simp only: step_red) - - have "steps0 (1, tp) (A |+| B) (Suc stp') = step0 (steps0 (1, tp) (A |+| B) stp') (A |+| B)" - by (simp only: step_red) - also have "... = step0 (steps0 (1, tp) A stp') (A |+| B)" using h1 by simp - also have "... = (Suc (length A div 2), tp')" - by (rule tm_comp_exec_after_first[OF fin h2 steps_in_range[OF fin a_wf]]) - finally show thesis using a by blast -qed - -lemma tm_comp_fetch_second_zero: - assumes h1: "fetch B s x = (a, 0)" - and hs: "tm_wf (A, 0)" "s \ 0" - shows "fetch (A |+| B) (s + (length A div 2)) x = (a, 0)" -using h1 hs -apply(case_tac x) -apply(case_tac [!] s) -apply(auto simp: tm_comp_length nth_append) -done - -lemma tm_comp_fetch_second_inst: - assumes h1: "fetch B sa x = (a, s)" - and hs: "tm_wf (A, 0)" "sa \ 0" "s \ 0" - shows "fetch (A |+| B) (sa + length A div 2) x = (a, s + length A div 2)" -using h1 hs -apply(case_tac x) -apply(case_tac [!] sa) -apply(auto simp: tm_comp_length nth_append) -done - - -lemma tm_comp_second_same: - assumes a_wf: "tm_wf (A, 0)" - and steps: "steps0 (1, l, r) B stp = (s', l', r')" - shows "steps0 (Suc (length A div 2), l, r) (A |+| B) stp - = (if s' = 0 then 0 else s' + length A div 2, l', r')" -using steps -proof(induct stp arbitrary: s' l' r') - case 0 - then show ?case by (simp add: steps.simps) -next - case (Suc stp s' l' r') - obtain s'' l'' r'' where a: "steps0 (1, l, r) B stp = (s'', l'', r'')" - by (metis is_final.cases) - then have ih1: "s'' = 0 \ steps0 (Suc (length A div 2), l, r) (A |+| B) stp = (0, l'', r'')" - and ih2: "s'' \ 0 \ steps0 (Suc (length A div 2), l, r) (A |+| B) stp = (s'' + length A div 2, l'', r'')" - using Suc by (auto) - have h: "steps0 (1, l, r) B (Suc stp) = (s', l', r')" by fact - - { assume "s'' = 0" - then have ?case using a h ih1 by (simp del: steps.simps) - } moreover - { assume as: "s'' \ 0" "s' = 0" - from as a h - have "step0 (s'', l'', r'') B = (0, l', r')" by (simp del: steps.simps) - with as have ?case - apply(simp add: ih2[OF as(1)] step.simps del: tm_comp.simps steps.simps) - apply(case_tac "fetch B s'' (read r'')") - apply(auto simp add: tm_comp_fetch_second_zero[OF _ a_wf] simp del: tm_comp.simps) - done - } moreover - { assume as: "s'' \ 0" "s' \ 0" - from as a h - have "step0 (s'', l'', r'') B = (s', l', r')" by (simp del: steps.simps) - with as have ?case - apply(simp add: ih2[OF as(1)] step.simps del: tm_comp.simps steps.simps) - apply(case_tac "fetch B s'' (read r'')") - apply(auto simp add: tm_comp_fetch_second_inst[OF _ a_wf as] simp del: tm_comp.simps) - done - } - ultimately show ?case by blast -qed - -lemma tm_comp_second_halt_same: - assumes "tm_wf (A, 0)" - and "steps0 (1, l, r) B stp = (0, l', r')" - shows "steps0 (Suc (length A div 2), l, r) (A |+| B) stp = (0, l', r')" -using tm_comp_second_same[OF assms] by (simp) - -end -