71 apply(auto simp add: tshift.simps) |
71 apply(auto simp add: tshift.simps) |
72 done |
72 done |
73 |
73 |
74 lemma change_termi_state_def2: |
74 lemma change_termi_state_def2: |
75 "change_termi_state p == |
75 "change_termi_state p == |
76 (map (\<lambda> (a, s). (a, if s = 0 then Suc ((length s) div 2)) else s) t)" |
76 (map (\<lambda> (a, s). (a, if s = 0 then ((length p) div 2) + 1 else s)) p)" |
77 apply(rule eq_reflection) |
77 apply(rule eq_reflection) |
78 apply(auto simp add: change_termi_state.simps) |
78 apply(auto simp add: change_termi_state.simps) |
79 done |
79 done |
80 |
80 |
81 |
81 |
91 tstep ("step") and |
91 tstep ("step") and |
92 steps ("nsteps") and |
92 steps ("nsteps") and |
93 abc_lm_v ("lookup") and |
93 abc_lm_v ("lookup") and |
94 abc_lm_s ("set") and |
94 abc_lm_s ("set") and |
95 haltP ("stdhalt") and |
95 haltP ("stdhalt") and |
|
96 tshift ("shift") and |
96 change_termi_state ("adjust") and |
97 change_termi_state ("adjust") and |
97 tape_of_nat_list ("\<ulcorner>_\<urcorner>") and |
98 tape_of_nat_list ("\<ulcorner>_\<urcorner>") and |
|
99 t_add ("_ \<oplus> _") and |
98 DUMMY ("\<^raw:\mbox{$\_$}>") |
100 DUMMY ("\<^raw:\mbox{$\_$}>") |
99 |
101 |
100 declare [[show_question_marks = false]] |
102 declare [[show_question_marks = false]] |
101 (*>*) |
103 (*>*) |
102 |
104 |
529 tape corresponding to a value @{term n} and producing |
531 tape corresponding to a value @{term n} and producing |
530 a new tape corresponding to the value @{term l} (the number of @{term Oc}s |
532 a new tape corresponding to the value @{term l} (the number of @{term Oc}s |
531 clustered on the output tape). |
533 clustered on the output tape). |
532 |
534 |
533 Before we can prove the undecidability of the halting problem for Turing machines, |
535 Before we can prove the undecidability of the halting problem for Turing machines, |
534 we have to define how to compose Turing machines. Given our setup, this is relatively |
536 we have to define how to compose two Turing machines. Given our setup, this is |
535 straightforward, if slightly fiddly. |
537 relatively straightforward, if slightly fiddly. We have the following two |
536 |
538 auxiliary functions: |
537 \begin{center} |
539 |
538 @{thm tshift_def2} |
540 \begin{center} |
539 \end{center} |
541 \begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {}} |
540 |
542 @{thm (lhs) tshift_def2} @{text "\<equiv>"}\\ |
541 (* HERE *) |
543 \hspace{4mm}@{thm (rhs) tshift_def2}\\ |
542 |
544 @{thm (lhs) change_termi_state_def2} @{text "\<equiv>"}\\ |
543 shift and change of a p |
545 \hspace{4mm}@{text "map (\<lambda> (a, s)."}\\ |
544 |
546 \hspace{14mm}@{text "(a, if s = 0 then length p div 2 + 1 else s)) p"}\\ |
545 composition of two ps |
547 \end{tabular} |
|
548 \end{center} |
|
549 |
|
550 \noindent |
|
551 With this we can define the \emph{sequential composition} of two |
|
552 Turing machines @{text "M\<^isub>1"} and @{text "M\<^isub>2"} |
|
553 |
|
554 \begin{center} |
|
555 @{thm t_add.simps[where ?t1.0="M\<^isub>1" and ?t2.0="M\<^isub>2", THEN eq_reflection]} |
|
556 \end{center} |
|
557 |
|
558 |
546 |
559 |
547 assertion holds for all tapes |
560 assertion holds for all tapes |
548 |
561 |
549 Hoare rule for composition |
562 Hoare rule for composition |
550 |
563 |