214 "tm_wf0 p \<equiv> tm_wf (p, 0)" |
214 "tm_wf0 p \<equiv> tm_wf (p, 0)" |
215 |
215 |
216 abbreviation exponent :: "'a \<Rightarrow> nat \<Rightarrow> 'a list" ("_ \<up> _" [100, 99] 100) |
216 abbreviation exponent :: "'a \<Rightarrow> nat \<Rightarrow> 'a list" ("_ \<up> _" [100, 99] 100) |
217 where "x \<up> n == replicate n x" |
217 where "x \<up> n == replicate n x" |
218 |
218 |
219 consts tape_of :: "'a \<Rightarrow> cell list" ("<_>" 100) |
219 class tape = |
220 |
220 fixes tape_of :: "'a \<Rightarrow> cell list" ("<_>" 100) |
221 defs (overloaded) |
221 |
222 tape_of_nat_abv: "<(n::nat)> \<equiv> Oc \<up> (Suc n)" |
222 |
223 |
223 instantiation nat::tape begin |
224 fun tape_of_nat_list :: "'a list \<Rightarrow> cell list" |
224 definition tape_of_nat where "tape_of_nat (n::nat) \<equiv> Oc \<up> (Suc n)" |
225 where |
225 instance by standard |
226 "tape_of_nat_list [] = []" | |
226 end |
227 "tape_of_nat_list [n] = <n>" | |
227 |
228 "tape_of_nat_list (n#ns) = <n> @ Bk # (tape_of_nat_list ns)" |
228 type_synonym nat_list = "nat list" |
229 |
229 |
230 fun tape_of_nat_pair :: "'a \<times> 'b \<Rightarrow> cell list" |
230 instantiation list::(tape) tape begin |
231 where |
231 fun tape_of_nat_list :: "('a::tape) list \<Rightarrow> cell list" |
232 "tape_of_nat_pair (n, m) = <n> @ [Bk] @ <m>" |
232 where |
233 |
233 "tape_of_nat_list [] = []" | |
234 |
234 "tape_of_nat_list [n] = <n>" | |
235 defs (overloaded) |
235 "tape_of_nat_list (n#ns) = <n> @ Bk # (tape_of_nat_list ns)" |
236 tape_of_nl_abv: "<(ns::'a list)> \<equiv> tape_of_nat_list ns" |
236 definition tape_of_list where "tape_of_list \<equiv> tape_of_nat_list" |
237 tape_of_nat_pair: "<(np::'a\<times>'b)> \<equiv> tape_of_nat_pair np" |
237 instance by standard |
|
238 end |
|
239 |
|
240 instantiation prod:: (tape, tape) tape begin |
|
241 fun tape_of_nat_prod :: "('a::tape) \<times> ('b::tape) \<Rightarrow> cell list" |
|
242 where "tape_of_nat_prod (n, m) = <n> @ [Bk] @ <m>" |
|
243 definition tape_of_prod where "tape_of_prod \<equiv> tape_of_nat_prod" |
|
244 instance by standard |
|
245 end |
238 |
246 |
239 fun |
247 fun |
240 shift :: "instr list \<Rightarrow> nat \<Rightarrow> instr list" |
248 shift :: "instr list \<Rightarrow> nat \<Rightarrow> instr list" |
241 where |
249 where |
242 "shift p n = (map (\<lambda> (a, s). (a, (if s = 0 then 0 else s + n))) p)" |
250 "shift p n = (map (\<lambda> (a, s). (a, (if s = 0 then 0 else s + n))) p)" |
268 shows "length (A |+| B) = length A + length B" |
276 shows "length (A |+| B) = length A + length B" |
269 by auto |
277 by auto |
270 |
278 |
271 lemma tm_comp_wf[intro]: |
279 lemma tm_comp_wf[intro]: |
272 "\<lbrakk>tm_wf (A, 0); tm_wf (B, 0)\<rbrakk> \<Longrightarrow> tm_wf (A |+| B, 0)" |
280 "\<lbrakk>tm_wf (A, 0); tm_wf (B, 0)\<rbrakk> \<Longrightarrow> tm_wf (A |+| B, 0)" |
273 by (auto) |
281 by (fastforce) |
274 |
282 |
275 lemma tm_comp_step: |
283 lemma tm_comp_step: |
276 assumes unfinal: "\<not> is_final (step0 c A)" |
284 assumes unfinal: "\<not> is_final (step0 c A)" |
277 shows "step0 c (A |+| B) = step0 c A" |
285 shows "step0 c (A |+| B) = step0 c A" |
278 proof - |
286 proof - |
331 using h1 h2 h3 |
339 using h1 h2 h3 |
332 apply(case_tac c) |
340 apply(case_tac c) |
333 apply(auto simp del: tm_comp.simps) |
341 apply(auto simp del: tm_comp.simps) |
334 apply(case_tac "fetch A a Bk") |
342 apply(case_tac "fetch A a Bk") |
335 apply(simp del: tm_comp.simps) |
343 apply(simp del: tm_comp.simps) |
336 apply(subst tm_comp_fetch_in_A) |
344 apply(subst tm_comp_fetch_in_A;force) |
337 apply(auto)[4] |
345 apply(case_tac "fetch A a (hd ca)") |
338 apply(case_tac "fetch A a (hd c)") |
|
339 apply(simp del: tm_comp.simps) |
346 apply(simp del: tm_comp.simps) |
340 apply(subst tm_comp_fetch_in_A) |
347 apply(subst tm_comp_fetch_in_A) |
341 apply(auto)[4] |
348 apply(auto)[4] |
342 done |
349 done |
343 |
350 |
346 and h2: "tm_wf (A, 0)" |
353 and h2: "tm_wf (A, 0)" |
347 shows "fst (step0 c A) \<le> length A div 2" |
354 shows "fst (step0 c A) \<le> length A div 2" |
348 using h1 h2 |
355 using h1 h2 |
349 apply(case_tac c) |
356 apply(case_tac c) |
350 apply(case_tac a) |
357 apply(case_tac a) |
351 apply(auto simp add: prod_case_unfold Let_def) |
358 apply(auto simp add: Let_def case_prod_beta') |
352 apply(case_tac "hd c") |
359 apply(case_tac "hd ca") |
353 apply(auto simp add: prod_case_unfold) |
360 apply(auto simp add: case_prod_beta') |
354 done |
361 done |
355 |
362 |
356 lemma steps_in_range: |
363 lemma steps_in_range: |
357 assumes h1: "\<not> is_final (steps0 (1, tp) A stp)" |
364 assumes h1: "\<not> is_final (steps0 (1, tp) A stp)" |
358 and h2: "tm_wf (A, 0)" |
365 and h2: "tm_wf (A, 0)" |