47 Cons ("_::_" [48,47] 68) and |
47 Cons ("_::_" [48,47] 68) and |
48 append ("_@_" [65, 64] 65) and |
48 append ("_@_" [65, 64] 65) and |
49 Oc ("1") and |
49 Oc ("1") and |
50 Bk ("0") and |
50 Bk ("0") and |
51 exponent ("_\<^bsup>_\<^esup>" [107] 109) and |
51 exponent ("_\<^bsup>_\<^esup>" [107] 109) and |
52 inv_begin0 ("I\<^isub>0") and |
52 inv_begin0 ("I\<^sub>0") and |
53 inv_begin1 ("I\<^isub>1") and |
53 inv_begin1 ("I\<^sub>1") and |
54 inv_begin2 ("I\<^isub>2") and |
54 inv_begin2 ("I\<^sub>2") and |
55 inv_begin3 ("I\<^isub>3") and |
55 inv_begin3 ("I\<^sub>3") and |
56 inv_begin4 ("I\<^isub>4") and |
56 inv_begin4 ("I\<^sub>4") and |
57 inv_begin ("I\<^bsub>cbegin\<^esub>") and |
57 inv_begin ("I\<^bsub>cbegin\<^esub>") and |
58 inv_loop1 ("J\<^isub>1") and |
58 inv_loop1 ("J\<^sub>1") and |
59 inv_loop0 ("J\<^isub>0") and |
59 inv_loop0 ("J\<^sub>0") and |
60 inv_end1 ("K\<^isub>1") and |
60 inv_end1 ("K\<^sub>1") and |
61 inv_end0 ("K\<^isub>0") and |
61 inv_end0 ("K\<^sub>0") and |
62 recf.id ("Id\<^raw:\makebox[0mm]{\,\,\,\,>\<^isup>_\<^raw:}>\<^isub>_") and |
62 recf.id ("Id\<^raw:\makebox[0mm]{\,\,\,\,>\<^sup>_\<^raw:}>\<^sub>_") and |
63 Pr ("Pr\<^isup>_") and |
63 Pr ("Pr\<^sup>_") and |
64 Cn ("Cn\<^isup>_") and |
64 Cn ("Cn\<^sup>_") and |
65 Mn ("Mn\<^isup>_") and |
65 Mn ("Mn\<^sup>_") and |
66 tcopy ("copy") and |
66 tcopy ("copy") and |
67 tcontra ("contra") and |
67 tcontra ("contra") and |
68 tape_of ("\<langle>_\<rangle>") and |
68 tape_of ("\<langle>_\<rangle>") and |
69 code_tcontra ("code contra") and |
69 code_tcontra ("code contra") and |
70 tm_comp ("_ ; _") |
70 tm_comp ("_ ; _") |
561 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
561 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
562 *} |
562 *} |
563 |
563 |
564 (*<*) |
564 (*<*) |
565 lemmas HR1 = |
565 lemmas HR1 = |
566 Hoare_plus_halt[where ?S.0="R\<iota>" and ?A="p\<^isub>1" and B="p\<^isub>2"] |
566 Hoare_plus_halt[where ?S.0="R\<iota>" and ?A="p\<^sub>1" and B="p\<^sub>2"] |
567 |
567 |
568 lemmas HR2 = |
568 lemmas HR2 = |
569 Hoare_plus_unhalt[where ?A="p\<^isub>1" and B="p\<^isub>2"] |
569 Hoare_plus_unhalt[where ?A="p\<^sub>1" and B="p\<^sub>2"] |
570 (*>*) |
570 (*>*) |
571 |
571 |
572 text_raw {* |
572 text_raw {* |
573 \definecolor{mygrey}{rgb}{.80,.80,.80} |
573 \definecolor{mygrey}{rgb}{.80,.80,.80} |
574 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
574 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
613 of @{text contra} halts, then\smallskip |
613 of @{text contra} halts, then\smallskip |
614 |
614 |
615 \begin{center}\small |
615 \begin{center}\small |
616 \begin{tabular}{@ {}l@ {}} |
616 \begin{tabular}{@ {}l@ {}} |
617 \begin{tabular}[t]{@ {\hspace{-5mm}}l@ {}} |
617 \begin{tabular}[t]{@ {\hspace{-5mm}}l@ {}} |
618 @{term "P\<^isub>1 \<equiv> \<lambda>tp. tp = ([]::cell list, <code_tcontra>)"}\\ |
618 @{term "P\<^sub>1 \<equiv> \<lambda>tp. tp = ([]::cell list, <code_tcontra>)"}\\ |
619 @{term "P\<^isub>2 \<equiv> \<lambda>tp. tp = ([Bk], <(code_tcontra, code_tcontra)>)"}\\ |
619 @{term "P\<^sub>2 \<equiv> \<lambda>tp. tp = ([Bk], <(code_tcontra, code_tcontra)>)"}\\ |
620 @{term "P\<^isub>3 \<equiv> \<lambda>tp. \<exists>k. tp = (Bk \<up> k, <0::nat>)"} |
620 @{term "P\<^sub>3 \<equiv> \<lambda>tp. \<exists>k. tp = (Bk \<up> k, <0::nat>)"} |
621 \end{tabular}\bigskip\bigskip |
621 \end{tabular}\bigskip\bigskip |
622 \\ |
622 \\ |
623 \begin{tabular}[b]{@ {\hspace{20mm}}l@ {}} |
623 \begin{tabular}[b]{@ {\hspace{20mm}}l@ {}} |
624 $\inferrule*{ |
624 $\inferrule*{ |
625 \inferrule*{@{term "{P\<^isub>1} tcopy {P\<^isub>2}"} \\ @{term "{P\<^isub>2} H {P\<^isub>3}"}} |
625 \inferrule*{@{term "{P\<^sub>1} tcopy {P\<^sub>2}"} \\ @{term "{P\<^sub>2} H {P\<^sub>3}"}} |
626 {@{term "{P\<^isub>1} (tcopy |+| H) {P\<^isub>3}"}} |
626 {@{term "{P\<^sub>1} (tcopy |+| H) {P\<^sub>3}"}} |
627 \\ @{term "{P\<^isub>3} dither \<up>"} |
627 \\ @{term "{P\<^sub>3} dither \<up>"} |
628 } |
628 } |
629 {@{term "{P\<^isub>1} tcontra \<up>"}} |
629 {@{term "{P\<^sub>1} tcontra \<up>"}} |
630 $ |
630 $ |
631 \end{tabular} |
631 \end{tabular} |
632 \end{tabular} |
632 \end{tabular} |
633 \end{center} |
633 \end{center} |
634 \end{itemize}} |
634 \end{itemize}} |
638 of @{text contra} does \emph{not} halt, then\\[-8mm]\mbox{} |
638 of @{text contra} does \emph{not} halt, then\\[-8mm]\mbox{} |
639 |
639 |
640 \begin{center}\small |
640 \begin{center}\small |
641 \begin{tabular}{@ {}l@ {}} |
641 \begin{tabular}{@ {}l@ {}} |
642 \begin{tabular}[t]{@ {\hspace{-1mm}}l@ {}} |
642 \begin{tabular}[t]{@ {\hspace{-1mm}}l@ {}} |
643 @{term "Q\<^isub>1 \<equiv> \<lambda>tp. tp = ([]::cell list, <code_tcontra>)"}\\ |
643 @{term "Q\<^sub>1 \<equiv> \<lambda>tp. tp = ([]::cell list, <code_tcontra>)"}\\ |
644 @{term "Q\<^isub>2 \<equiv> \<lambda>tp. tp = ([Bk], <(code_tcontra, code_tcontra)>)"}\\ |
644 @{term "Q\<^sub>2 \<equiv> \<lambda>tp. tp = ([Bk], <(code_tcontra, code_tcontra)>)"}\\ |
645 @{term "Q\<^isub>3 \<equiv> \<lambda>tp. \<exists>k. tp = (Bk \<up> k, <1::nat>)"} |
645 @{term "Q\<^sub>3 \<equiv> \<lambda>tp. \<exists>k. tp = (Bk \<up> k, <1::nat>)"} |
646 \end{tabular}\bigskip\bigskip |
646 \end{tabular}\bigskip\bigskip |
647 \\ |
647 \\ |
648 \begin{tabular}[b]{@ {\hspace{20mm}}l@ {}} |
648 \begin{tabular}[b]{@ {\hspace{20mm}}l@ {}} |
649 $\inferrule*{ |
649 $\inferrule*{ |
650 \inferrule*{@{term "{Q\<^isub>1} tcopy {Q\<^isub>2}"} \\ @{term "{Q\<^isub>2} H {Q\<^isub>3}"}} |
650 \inferrule*{@{term "{Q\<^sub>1} tcopy {Q\<^sub>2}"} \\ @{term "{Q\<^sub>2} H {Q\<^sub>3}"}} |
651 {@{term "{Q\<^isub>1} (tcopy |+| H) {Q\<^isub>3}"}} |
651 {@{term "{Q\<^sub>1} (tcopy |+| H) {Q\<^sub>3}"}} |
652 \\ @{term "{Q\<^isub>3} dither {Q\<^isub>3}"} |
652 \\ @{term "{Q\<^sub>3} dither {Q\<^sub>3}"} |
653 } |
653 } |
654 {@{term "{Q\<^isub>1} tcontra {Q\<^isub>3}"}} |
654 {@{term "{Q\<^sub>1} tcontra {Q\<^sub>3}"}} |
655 $ |
655 $ |
656 \end{tabular} |
656 \end{tabular} |
657 \end{tabular} |
657 \end{tabular} |
658 \end{center} |
658 \end{center} |
659 \end{itemize}} |
659 \end{itemize}} |
816 \end{tabular} |
816 \end{tabular} |
817 \end{center} |
817 \end{center} |
818 |
818 |
819 \small |
819 \small |
820 \begin{tabular}{l} |
820 \begin{tabular}{l} |
821 @{text "if_zero e \<equiv> \<Lambda> exit. Inst (W\<^isub>0, e), (W\<^isub>1, exit); Label exit"}\\ |
821 @{text "if_zero e \<equiv> \<Lambda> exit. Inst (W\<^sub>0, e), (W\<^sub>1, exit); Label exit"}\\ |
822 \hspace{5mm}@{text "jmp e \<equiv> Inst (W\<^isub>0, e), (W\<^isub>1, e)"} |
822 \hspace{5mm}@{text "jmp e \<equiv> Inst (W\<^sub>0, e), (W\<^sub>1, e)"} |
823 \end{tabular} |
823 \end{tabular} |
824 |
824 |
825 \end{frame}} |
825 \end{frame}} |
826 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
826 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
827 *} |
827 *} |
911 |
911 |
912 \begin{itemize} |
912 \begin{itemize} |
913 \item we introduced some tactics for handling sequential programs\bigskip |
913 \item we introduced some tactics for handling sequential programs\bigskip |
914 |
914 |
915 \begin{center} |
915 \begin{center} |
916 @{text "\<lbrace>p\<rbrace> i:[c\<^isub>1 ; ... ; c\<^isub>n]:j \<lbrace>q\<rbrace>"} |
916 @{text "\<lbrace>p\<rbrace> i:[c\<^sub>1 ; ... ; c\<^sub>n]:j \<lbrace>q\<rbrace>"} |
917 \end{center}\bigskip\bigskip |
917 \end{center}\bigskip\bigskip |
918 |
918 |
919 \item for loops we often only have to do inductions on the length |
919 \item for loops we often only have to do inductions on the length |
920 of the input (e.g.~how many @{text "1"}s are on the tape)\pause |
920 of the input (e.g.~how many @{text "1"}s are on the tape)\pause |
921 |
921 |