79 apply(case_tac ns)

    79 apply(case_tac ns)

    80 apply(auto)

    80 apply(auto)

    81 done

    81 done

    82 

    82 

    83 lemmas HR1 = 

    83 lemmas HR1 = 

    85 

    85 

    86 lemmas HR2 =

    86 lemmas HR2 =

    88 

    88 

    89 (*>*)

    89 (*>*)

    90 

    90 

    91 section {* Introduction *}

    91 section {* Introduction *}

    92 

    92 

   178 %example---undecidability of Wang's tiling problem---in Section~\ref{Wang}. The

   178 %example---undecidability of Wang's tiling problem---in Section~\ref{Wang}. The

   179 %standard proof of this property uses the notion of universal

   179 %standard proof of this property uses the notion of universal

   180 %Turing machines.

   180 %Turing machines.

   181 

   181 

   182 We are not the first who formalised Turing machines: we are aware 

   182 We are not the first who formalised Turing machines: we are aware 

   184 \cite{AspertiRicciotti12}. They describe a complete formalisation of

   184 \cite{AspertiRicciotti12}. They describe a complete formalisation of

   185 Turing machines in the Matita theorem prover, including a universal

   185 Turing machines in the Matita theorem prover, including a universal

   186 Turing machine. However, they do \emph{not} formalise the undecidability of the 

   186 Turing machine. However, they do \emph{not} formalise the undecidability of the 

   187 halting problem since their main focus is complexity, rather than

   187 halting problem since their main focus is complexity, rather than

   188 computability theory. They also report that the informal proofs from which they

   188 computability theory. They also report that the informal proofs from which they

   635   \draw[fill]     ( 0.35,0.1) rectangle (0.65,0.4);

   635   \draw[fill]     ( 0.35,0.1) rectangle (0.65,0.4);

   636   \draw[fill]     ( 0.85,0.1) rectangle (1.15,0.4);

   636   \draw[fill]     ( 0.85,0.1) rectangle (1.15,0.4);

   637   \end{scope}

   637   \end{scope}

   638   \end{tikzpicture}\\[-8mm]\mbox{} 

   638   \end{tikzpicture}\\[-8mm]\mbox{} 

   639   \end{center}

   639   \end{center}

   642   the end of the right tape; the second then ``moves'' all @{term Oc}s except the 

   642   the end of the right tape; the second then ``moves'' all @{term Oc}s except the 

   643   first from the beginning of the tape to the end; the third ``refills'' the original 

   643   first from the beginning of the tape to the end; the third ``refills'' the original 

   644   block of @{term "Oc"}s. The resulting tape is @{term "([Bk], <[2::nat, 2::nat]>)"}.}

   644   block of @{term "Oc"}s. The resulting tape is @{term "([Bk], <[2::nat, 2::nat]>)"}.}

   645   \label{copy}

   645   \label{copy}

   646   \end{figure}

   646   \end{figure}

   660   \end{center}

   660   \end{center}

   661 

   661 

   662   \noindent

   662   \noindent

   663   A standard tape is then of the form @{text "(Bk\<^isup>l,\<langle>[n\<^isub>1,...,n\<^isub>m]\<rangle>)"} for some @{text l} 

   663   A standard tape is then of the form @{text "(Bk\<^isup>l,\<langle>[n\<^isub>1,...,n\<^isub>m]\<rangle>)"} for some @{text l} 

   664   and @{text "n\<^isub>i"}. Note that the head in a standard tape ``points'' to the 

   664   and @{text "n\<^isub>i"}. Note that the head in a standard tape ``points'' to the 

   667 

   667 

   668   Before we can prove the undecidability of the halting problem for our

   668   Before we can prove the undecidability of the halting problem for our

   669   Turing machines, we need to analyse two concrete Turing machine

   669   Turing machines, we need to analyse two concrete Turing machine

   670   programs and establish that they are correct---that means they are

   670   programs and establish that they are correct---that means they are

   671   ``doing what they are supposed to be doing''.  Such correctness proofs are usually left

   671   ``doing what they are supposed to be doing''.  Such correctness proofs are usually left

   726   "tcopy_end"}.

   726   "tcopy_end"}.

   727 

   727 

   728   It is realatively straightforward to prove that the Turing program 

   728   It is realatively straightforward to prove that the Turing program 

   729   @{term "dither"} shown in \eqref{dither} is correct. This program

   729   @{term "dither"} shown in \eqref{dither} is correct. This program

   730   should be the ``identity'' when started with a standard tape representing 

   730   should be the ``identity'' when started with a standard tape representing 

   732 

   733 

   733 

   734 

   734   \begin{center}

   735   \begin{center}

   735   \begin{tabular}{l@ {\hspace{3mm}}lcl}

   736   \begin{tabular}{l@ {\hspace{3mm}}lcl}

   736   & \multicolumn{1}{c}{start tape}\\[1mm]

   737   & \multicolumn{1}{c}{start tape}\\[1mm]

   800   a value on the tape.  Reasoning about this program is substantially

   801   a value on the tape.  Reasoning about this program is substantially

   801   harder than about @{term dither}. To ease the burden, we prove

   802   harder than about @{term dither}. To ease the burden, we prove

   802   the following two Hoare-rules for sequentially composed programs.

   803   the following two Hoare-rules for sequentially composed programs.

   803 

   804 

   804   \begin{center}

   805   \begin{center}

   808   {@{thm (concl) HR1}}

   809   {@{thm (concl) HR1}}

   809   $ &

   810   $ &

   810   $

   811   $

   813   {@{thm (concl) HR2}}

   814   {@{thm (concl) HR2}}

   814   $

   815   $

   815   \end{tabular}

   816   \end{tabular}

   816   \end{center}

   817   \end{center}

   817 

   818 

   818   \noindent

   819   \noindent

   819   The first corresponds to the usual Hoare-rule for composition of two

   820   The first corresponds to the usual Hoare-rule for composition of two

   823   terminates generating a tape for which the second program loops.

   822   terminates generating a tape for which the second program loops.

   825   in order to ensure that the redirection of the halting and initial

   824   in order to ensure that the redirection of the halting and initial

   826   state in @{term "p\<^isub>1"} and @{term "p\<^isub>2"} match up correctly.

   825   state in @{term "p\<^isub>1"} and @{term "p\<^isub>2"} match up correctly.

   827 

   826 

   828 

   827 

   829   The Hoare-rules above allow us to prove the correctness of @{term tcopy}

   828   The Hoare-rules above allow us to prove the correctness of @{term tcopy}

   830   by considering the correctness of @{term "tcopy_begin"}, @{term "tcopy_loop"} 

   829   by considering the correctness of @{term "tcopy_begin"}, @{term "tcopy_loop"} 

   832   the program @{term "tcopy_begin"}. 

   831   the program @{term "tcopy_begin"}. 

   833 

   832 

   834 

   833 

   835   measure for the copying TM, which we however omit.

   834   measure for the copying TM, which we however omit.

   836 

   835