34 apply - |
34 apply - |
35 apply(rule_tac [!] eq_reflection) |
35 apply(rule_tac [!] eq_reflection) |
36 apply(auto split: taction.splits simp add: new_tape.simps) |
36 apply(auto split: taction.splits simp add: new_tape.simps) |
37 done |
37 done |
38 |
38 |
|
39 |
|
40 abbreviation |
|
41 "read r == if (r = []) then Bk else hd r" |
|
42 |
39 lemma tstep_def2: |
43 lemma tstep_def2: |
40 shows "tstep (s, l, []) p == (let (ac, ns) = fetch p s Bk in (ns, new_tape ac (l, [])))" |
44 shows "tstep (s, l, r) p == (let (a, s') = fetch p s (read r) in (s', new_tape a (l, r)))" |
41 and "tstep (s, l, x#xs) p == (let (ac, ns) = fetch p s x in (ns, new_tape ac (l, x#xs)))" |
|
42 apply - |
45 apply - |
43 apply(rule_tac [!] eq_reflection) |
46 apply(rule_tac [!] eq_reflection) |
44 by (auto split: prod.split list.split simp add: tstep.simps) |
47 by (auto split: if_splits prod.split list.split simp add: tstep.simps) |
45 |
48 |
46 consts DUMMY::'a |
49 consts DUMMY::'a |
47 |
50 |
48 notation (latex output) |
51 notation (latex output) |
49 Cons ("_::_" [78,77] 73) and |
52 Cons ("_::_" [78,77] 73) and |
50 W0 ("W\<^bsub>\<^raw:\hspace{-2pt}>Bk\<^esub>") and |
53 W0 ("W\<^bsub>\<^raw:\hspace{-2pt}>Bk\<^esub>") and |
51 W1 ("W\<^bsub>\<^raw:\hspace{-2pt}>Oc\<^esub>") and |
54 W1 ("W\<^bsub>\<^raw:\hspace{-2pt}>Oc\<^esub>") and |
|
55 tstep ("step") and |
|
56 steps ("nsteps") and |
52 DUMMY ("\<^raw:\mbox{$\_$}>") |
57 DUMMY ("\<^raw:\mbox{$\_$}>") |
53 |
58 |
54 declare [[show_question_marks = false]] |
59 declare [[show_question_marks = false]] |
55 (*>*) |
60 (*>*) |
56 |
61 |
304 of natural numbers starting from @{text 0} up to number of states |
309 of natural numbers starting from @{text 0} up to number of states |
305 of the machine minus @{text 1}. In doing so we can compose |
310 of the machine minus @{text 1}. In doing so we can compose |
306 two Turing machine by ``shifting'' the states of one by an appropriate |
311 two Turing machine by ``shifting'' the states of one by an appropriate |
307 amount to a higher segment. |
312 amount to a higher segment. |
308 |
313 |
309 An \emph{instruction} of a Turing machine is a pair consisting of a |
314 An \emph{instruction} @{term i} of a Turing machine is a pair consisting of a |
310 natural number (the next state) and an action. A \emph{program} of a Turing |
315 natural number (the next state) and an action. A \emph{program} @{term p} of a Turing |
311 machine is then a list of such pairs. Given a program @{term p}, a state |
316 machine is then a list of such pairs. Given a program @{term p}, a state |
312 and the cell being read by the read-write unit, we need to fetch |
317 and the cell being read by the read-write unit, we need to fetch |
313 the corresponding instruction from the program. For this we define |
318 the corresponding instruction from the program. For this we define |
314 the function @{term fetch} |
319 the function @{term fetch} |
315 |
320 |
335 @{thm dither_def} |
340 @{thm dither_def} |
336 \end{center} |
341 \end{center} |
337 |
342 |
338 |
343 |
339 A \emph{configuration} @{term c} of a Turing machine is a state together with |
344 A \emph{configuration} @{term c} of a Turing machine is a state together with |
340 a tape. If we have a configuration and a program, we can calculate |
345 a tape. This is written as the triple @{term "(s, l, r)"}. If we have a |
|
346 configuration and a program, we can calculate |
341 what the next configuration is by fetching the appropriate next state |
347 what the next configuration is by fetching the appropriate next state |
342 and action from the program. Such a single step of execution can be defined as |
348 and action from the program. Such a single step of execution can be defined as |
343 |
349 |
344 \begin{center} |
350 \begin{center} |
345 @{thm tstep_def2(1)}\\ |
351 @{thm tstep_def2(1)}\\ |
346 @{thm tstep_def2(2)}\\ |
352 \end{center} |
347 \end{center} |
353 |
|
354 No evaluator in HOL, because of totality. |
|
355 |
|
356 \begin{center} |
|
357 @{thm steps.simps(1)}\\ |
|
358 @{thm steps.simps(2)}\\ |
|
359 \end{center} |
|
360 |
|
361 \emph{well-formedness} of a Turing program |
|
362 |
|
363 programs halts |
|
364 |
|
365 shift and change of a p |
|
366 |
|
367 composition of two ps |
|
368 |
|
369 assertion holds for all tapes |
|
370 |
|
371 Hoare rule for composition |
348 |
372 |
349 For showing the undecidability of the halting problem, we need to consider |
373 For showing the undecidability of the halting problem, we need to consider |
350 two specific Turing machines. |
374 two specific Turing machines. copying TM and dithering TM |
351 |
375 |
352 |
376 correctness of the copying TM |
353 No evaluator in HOL, because of totality. |
377 |
|
378 measure for the copying TM, which we however omit. |
|
379 |
|
380 standard configuration |
|
381 |
|
382 halting problem |
354 *} |
383 *} |
355 |
384 |
356 section {* Abacus Machines *} |
385 section {* Abacus Machines *} |
357 |
386 |
358 section {* Recursive Functions *} |
387 section {* Recursive Functions *} |