equal
deleted
inserted
replaced
116 apply(case_tac ns) |
116 apply(case_tac ns) |
117 apply(auto simp add: tape_of_nat_pair tape_of_nat_abv) |
117 apply(auto simp add: tape_of_nat_pair tape_of_nat_abv) |
118 done |
118 done |
119 |
119 |
120 lemmas HR1 = |
120 lemmas HR1 = |
121 Hoare_plus_halt_simple[where ?P1.0="P" and ?P2.0="Q" and ?P3.0="R\<iota>" and ?A="p\<^isub>1" and B="p\<^isub>2"] |
121 Hoare_plus_halt[where ?S.0="R\<iota>" and ?A="p\<^isub>1" and B="p\<^isub>2"] |
122 |
122 |
123 lemmas HR2 = |
123 lemmas HR2 = |
124 Hoare_plus_unhalt_simple[where ?P1.0="P" and ?P2.0="Q" and ?A="p\<^isub>1" and B="p\<^isub>2"] |
124 Hoare_plus_unhalt[where ?A="p\<^isub>1" and B="p\<^isub>2"] |
125 |
125 |
126 lemma inv_begin01: |
126 lemma inv_begin01: |
127 assumes "n > 1" |
127 assumes "n > 1" |
128 shows "inv_begin0 n (l, r) = (n > 1 \<and> (l, r) = (Oc \<up> (n - 2), [Oc, Oc, Bk, Oc]))" |
128 shows "inv_begin0 n (l, r) = (n > 1 \<and> (l, r) = (Oc \<up> (n - 2), [Oc, Oc, Bk, Oc]))" |
129 using assms by auto |
129 using assms by auto |
762 \hspace{7mm}@{text "\<forall>"} @{term n}. @{text "\<not> is_final (steps (1, (l, r)) p n)"} |
762 \hspace{7mm}@{text "\<forall>"} @{term n}. @{text "\<not> is_final (steps (1, (l, r)) p n)"} |
763 \end{tabular} |
763 \end{tabular} |
764 \end{tabular} |
764 \end{tabular} |
765 \end{center} |
765 \end{center} |
766 |
766 |
|
767 \noindent |
|
768 For our Hoare-triples we can easily prove the following consequence rule |
|
769 |
|
770 \begin{equation} |
|
771 @{thm[mode=Rule] Hoare_consequence} |
|
772 \end{equation} |
|
773 |
|
774 |
767 \noindent |
775 \noindent |
768 Like Asperti and Ricciotti with their notion of realisability, we |
776 Like Asperti and Ricciotti with their notion of realisability, we |
769 have set up our Hoare-rules so that we can deal explicitly |
777 have set up our Hoare-rules so that we can deal explicitly |
770 with total correctness and non-terminantion, rather than have |
778 with total correctness and non-terminantion, rather than have |
771 notions for partial correctness and termination. Although the latter |
779 notions for partial correctness and termination. Although the latter |
926 \end{center} |
934 \end{center} |
927 |
935 |
928 |
936 |
929 |
937 |
930 \begin{center} |
938 \begin{center} |
931 @{thm haltP_def[where lm="ns"]} |
939 @{thm haltP_def} |
932 \end{center} |
940 \end{center} |
933 |
941 |
934 |
942 |
935 Undecidability of the halting problem. |
943 Undecidability of the halting problem. |
936 |
944 |