equal
deleted
inserted
replaced
1 (* Title: Turing machines |
1 (* Title: thys/Turing.thy |
2 Author: Xu Jian <xujian817@hotmail.com> |
2 Author: Jian Xu, Xingyuan Zhang, and Christian Urban |
3 Maintainer: Xu Jian |
|
4 *) |
3 *) |
|
4 |
|
5 header {* Turing Machines *} |
5 |
6 |
6 theory Turing |
7 theory Turing |
7 imports Main |
8 imports Main |
8 begin |
9 begin |
9 |
10 |
24 type_synonym tprog0 = "instr list" |
25 type_synonym tprog0 = "instr list" |
25 |
26 |
26 type_synonym config = "state \<times> tape" |
27 type_synonym config = "state \<times> tape" |
27 |
28 |
28 fun nth_of where |
29 fun nth_of where |
29 "nth_of xs i = (if i \<ge> length xs then None |
30 "nth_of xs i = (if i \<ge> length xs then None else Some (xs ! i))" |
30 else Some (xs ! i))" |
|
31 |
31 |
32 lemma nth_of_map [simp]: |
32 lemma nth_of_map [simp]: |
33 shows "nth_of (map f p) n = (case (nth_of p n) of None \<Rightarrow> None | Some x \<Rightarrow> Some (f x))" |
33 shows "nth_of (map f p) n = (case (nth_of p n) of None \<Rightarrow> None | Some x \<Rightarrow> Some (f x))" |
34 apply(induct p arbitrary: n) |
34 apply(induct p arbitrary: n) |
35 apply(auto) |
35 apply(auto) |
73 fun step :: "config \<Rightarrow> tprog \<Rightarrow> config" |
73 fun step :: "config \<Rightarrow> tprog \<Rightarrow> config" |
74 where |
74 where |
75 "step (s, l, r) (p, off) = |
75 "step (s, l, r) (p, off) = |
76 (let (a, s') = fetch p (s - off) (read r) in (s', update a (l, r)))" |
76 (let (a, s') = fetch p (s - off) (read r) in (s', update a (l, r)))" |
77 |
77 |
|
78 abbreviation |
|
79 "step0 c p \<equiv> step c (p, 0)" |
|
80 |
78 fun steps :: "config \<Rightarrow> tprog \<Rightarrow> nat \<Rightarrow> config" |
81 fun steps :: "config \<Rightarrow> tprog \<Rightarrow> nat \<Rightarrow> config" |
79 where |
82 where |
80 "steps c p 0 = c" | |
83 "steps c p 0 = c" | |
81 "steps c p (Suc n) = steps (step c p) p n" |
84 "steps c p (Suc n) = steps (step c p) p n" |
82 |
85 |
83 |
|
84 abbreviation |
|
85 "step0 c p \<equiv> step c (p, 0)" |
|
86 |
|
87 abbreviation |
86 abbreviation |
88 "steps0 c p n \<equiv> steps c (p, 0) n" |
87 "steps0 c p n \<equiv> steps c (p, 0) n" |
89 |
88 |
90 lemma step_red [simp]: |
89 lemma step_red [simp]: |
91 shows "steps c p (Suc n) = step (steps c p n) p" |
90 shows "steps c p (Suc n) = step (steps c p n) p" |
100 by (case_tac p, simp) |
99 by (case_tac p, simp) |
101 |
100 |
102 lemma steps_0 [simp]: |
101 lemma steps_0 [simp]: |
103 shows "steps (0, (l, r)) p n = (0, (l, r))" |
102 shows "steps (0, (l, r)) p n = (0, (l, r))" |
104 by (induct n) (simp_all) |
103 by (induct n) (simp_all) |
105 |
|
106 |
|
107 |
104 |
108 fun |
105 fun |
109 is_final :: "config \<Rightarrow> bool" |
106 is_final :: "config \<Rightarrow> bool" |
110 where |
107 where |
111 "is_final (s, l, r) = (s = 0)" |
108 "is_final (s, l, r) = (s = 0)" |
231 shows "length (A |+| B) = length A + length B" |
228 shows "length (A |+| B) = length A + length B" |
232 by auto |
229 by auto |
233 |
230 |
234 lemma tm_comp_wf[intro]: |
231 lemma tm_comp_wf[intro]: |
235 "\<lbrakk>tm_wf (A, 0); tm_wf (B, 0)\<rbrakk> \<Longrightarrow> tm_wf (A |+| B, 0)" |
232 "\<lbrakk>tm_wf (A, 0); tm_wf (B, 0)\<rbrakk> \<Longrightarrow> tm_wf (A |+| B, 0)" |
236 by (auto simp: tm_wf.simps shift.simps adjust.simps tm_comp_length tm_comp.simps) |
233 by (auto) |
237 |
|
238 |
234 |
239 lemma tm_comp_step: |
235 lemma tm_comp_step: |
240 assumes unfinal: "\<not> is_final (step0 c A)" |
236 assumes unfinal: "\<not> is_final (step0 c A)" |
241 shows "step0 c (A |+| B) = step0 c A" |
237 shows "step0 c (A |+| B) = step0 c A" |
242 proof - |
238 proof - |
332 have h: "\<not> is_final (steps0 (1, tp) A (Suc stp))" by fact |
328 have h: "\<not> is_final (steps0 (1, tp) A (Suc stp))" by fact |
333 from ih h h2 show "fst (steps0 (1, tp) A (Suc stp)) \<le> length A div 2" |
329 from ih h h2 show "fst (steps0 (1, tp) A (Suc stp)) \<le> length A div 2" |
334 by (metis step_in_range step_red) |
330 by (metis step_in_range step_red) |
335 qed |
331 qed |
336 |
332 |
337 lemma tm_comp_pre_halt_same: |
333 (* if A goes into the final state, then A |+| B will go into the first state of B *) |
|
334 lemma tm_comp_next: |
338 assumes a_ht: "steps0 (1, tp) A n = (0, tp')" |
335 assumes a_ht: "steps0 (1, tp) A n = (0, tp')" |
339 and a_wf: "tm_wf (A, 0)" |
336 and a_wf: "tm_wf (A, 0)" |
340 obtains n' where "steps0 (1, tp) (A |+| B) n' = (Suc (length A div 2), tp')" |
337 obtains n' where "steps0 (1, tp) (A |+| B) n' = (Suc (length A div 2), tp')" |
341 proof - |
338 proof - |
342 assume a: "\<And>n. steps (1, tp) (A |+| B, 0) n = (Suc (length A div 2), tp') \<Longrightarrow> thesis" |
339 assume a: "\<And>n. steps (1, tp) (A |+| B, 0) n = (Suc (length A div 2), tp') \<Longrightarrow> thesis" |
374 apply(case_tac [!] sa) |
371 apply(case_tac [!] sa) |
375 apply(auto simp: tm_comp_length nth_append) |
372 apply(auto simp: tm_comp_length nth_append) |
376 done |
373 done |
377 |
374 |
378 |
375 |
379 lemma tm_comp_second_same: |
376 lemma tm_comp_second: |
380 assumes a_wf: "tm_wf (A, 0)" |
377 assumes a_wf: "tm_wf (A, 0)" |
381 and steps: "steps0 (1, l, r) B stp = (s', l', r')" |
378 and steps: "steps0 (1, l, r) B stp = (s', l', r')" |
382 shows "steps0 (Suc (length A div 2), l, r) (A |+| B) stp |
379 shows "steps0 (Suc (length A div 2), l, r) (A |+| B) stp |
383 = (if s' = 0 then 0 else s' + length A div 2, l', r')" |
380 = (if s' = 0 then 0 else s' + length A div 2, l', r')" |
384 using steps |
381 using steps |
416 done |
413 done |
417 } |
414 } |
418 ultimately show ?case by blast |
415 ultimately show ?case by blast |
419 qed |
416 qed |
420 |
417 |
421 lemma tm_comp_second_halt_same: |
418 |
|
419 lemma tm_comp_final: |
422 assumes "tm_wf (A, 0)" |
420 assumes "tm_wf (A, 0)" |
423 and "steps0 (1, l, r) B stp = (0, l', r')" |
421 and "steps0 (1, l, r) B stp = (0, l', r')" |
424 shows "steps0 (Suc (length A div 2), l, r) (A |+| B) stp = (0, l', r')" |
422 shows "steps0 (Suc (length A div 2), l, r) (A |+| B) stp = (0, l', r')" |
425 using tm_comp_second_same[OF assms] by (simp) |
423 using tm_comp_second[OF assms] by (simp) |
426 |
424 |
427 end |
425 end |
428 |
426 |