325 machines that are needed in this proof; such correctness proofs are

   325 machines that are needed in this proof; such correctness proofs are

   326 left out in the informal literature.  For reasoning about Turing

   326 left out in the informal literature.  For reasoning about Turing

   327 machine programs we derive Hoare-rules.  We also construct the

   327 machine programs we derive Hoare-rules.  We also construct the

   328 universal Turing machine from \cite{Boolos87} by translating recursive

   328 universal Turing machine from \cite{Boolos87} by translating recursive

   329 functions to abacus machines and abacus machines to Turing

   329 functions to abacus machines and abacus machines to Turing

   331 we stumbled upon an inconsistent use of the definition of

   333 we stumbled upon an inconsistent use of the definition of

   333 %Since we have set up in

   336 %Since we have set up in

   334 %Isabelle/HOL a very general computability model and undecidability

   337 %Isabelle/HOL a very general computability model and undecidability

   335 %result, we are able to formalise other results: we describe a proof of

   338 %result, we are able to formalise other results: we describe a proof of

   336 %the computational equivalence of single-sided Turing machines, which

   339 %the computational equivalence of single-sided Turing machines, which

   337 %is not given in \cite{Boolos87}, but needed for example for

   340 %is not given in \cite{Boolos87}, but needed for example for

  1527   but then we would have to reimplement his infrastructure for

  1530   but then we would have to reimplement his infrastructure for

  1528   reducing $\lambda$-terms on the ML-level. We would still need to

  1531   reducing $\lambda$-terms on the ML-level. We would still need to

  1529   connect his work to Turing machines for proofs that make essential use of them

  1532   connect his work to Turing machines for proofs that make essential use of them

  1530   (for example the undecidability proof for Wang's tiling problem \cite{Robinson71}).

  1533   (for example the undecidability proof for Wang's tiling problem \cite{Robinson71}).

  1531 

  1534 

  1533   computability results from Chapters 3 to 8 in the textbook by Boolos

  1536   computability results from Chapters 3 to 8 in the textbook by Boolos

  1534   et al \cite{Boolos87}.  For this we did not need to implement

  1537   et al \cite{Boolos87}.  For this we did not need to implement

  1535   anything on the ML-level of Isabelle/HOL. While formalising the six chapters

  1538   anything on the ML-level of Isabelle/HOL. While formalising the six chapters

  1537   definitions of what function a Turing machine calculates. In

  1540   definitions of what function a Turing machine calculates. In

  1538   Chapter 3 they use a definition that states a function is undefined

  1541   Chapter 3 they use a definition that states a function is undefined

  1539   if the Turing machine loops \emph{or} halts with a non-standard

  1542   if the Turing machine loops \emph{or} halts with a non-standard

  1540   tape. Whereas in Chapter 8 about the universal Turing machine, the

  1543   tape. Whereas in Chapter 8 about the universal Turing machine, the

  1541   Turing machines will \emph{not} halt unless the tape is in standard

  1544   Turing machines will \emph{not} halt unless the tape is in standard

  1543   have titled our paper ``Boolos et al are (almost)

  1546   have titled our paper ``Boolos et al are (almost)

  1544   Right''. We have not attempted to formalise everything precisely as

  1547   Right''. We have not attempted to formalise everything precisely as

  1545   Boolos et al present it, but use definitions that make our

  1548   Boolos et al present it, but use definitions that make our

  1546   mechanised proofs manageable. For example our definition of the

  1549   mechanised proofs manageable. For example our definition of the

  1547   halting state performing @{term Nop}-operations seems to be

  1550   halting state performing @{term Nop}-operations seems to be