303 One concete model of computation are Turing machines. We use them 

   303 We like to enable Isabelle/HOL users to reason about computability

   304 in the theorem prover Isabelle/HOL for mechanising  results from 

   304 theory.  Reasoning about decidability of predicates, for example, is not as

   305 computability theory, for example the undecidability of the halting problem.

   305 straightforward as one might think in Isabelle/HOL and other HOL

   306 Reasoning about decidability is not as straightforward  as one might think

   306 theorem provers, since they are based on classical logic where the law

   307 in Isabelle/HOL and other HOL theorem provers,

   307 of excluded middle ensures that \mbox{@{term "P \<or> \<not>P"}} is always

   308 since they are based on classical logic where the law of excluded

   308 provable no matter whether the predicate @{text P} is constructed by

   309 middle ensures that \mbox{@{term "P \<or> \<not>P"}} is always provable no

   309 computable means.

   310 matter whether the predicate @{text P} is constructed by computable means.

   422 machine can then be constructed by translating from a recursive function. 

   421 machine can then be constructed by translating from a (universal) recursive function. 

   678   @{text r} is empty it returns @{term Bk}.  It is impossible in

   677   @{text r} is empty it returns @{term Bk}.  

   679   Isabelle/HOL to lift the @{term step}-function in order to realise a

   678   We lift this definition to an evaluation function that performs 

   680   general evaluation function for Turing machines programs. The reason

   679   exactly @{text n} steps:

   681   is that functions in HOL-based provers need to be terminating, and

   682   clearly there are programs that are not.\footnote{There is the alternative

   683   to use partial functions, which do not necessarily need to terminate, but

   684   this does not provide us with a useful induction principle \cite{Krauss10}.} We can however define a

   685   recursive evaluation function that performs exactly @{text n} steps:

  1660   computability because in Isabelle/HOL we cannot represent the

  1654   computability because in Isabelle/HOL we cannot, for example,

  1661   decidability of a predicate @{text P}, say, as the formula @{term "P

  1655   represent the decidability of a predicate @{text P}, say, as the

  1662   \<or> \<not>P"}. For reasoning about computability we need to formalise a

  1656   formula @{term "P \<or> \<not>P"}. For reasoning about computability we need

  1663   concrete model of computations. We could have followed Norrish

  1657   to formalise a concrete model of computations. We could have

  1664   \cite{Norrish11} using the $\lambda$-calculus as the starting point for computability theory,

  1658   followed Norrish \cite{Norrish11} using the $\lambda$-calculus as

  1665   but then we would still have 

  1659   the starting point for computability theory, but then we would have

  1666   %to reimplement his infrastructure for

  1660   to reimplement on the ML-level his infrastructure for rewriting

  1667   %reducing $\lambda$-terms on the ML-level. 

  1661   $\lambda$-terms modulo $\beta$-equality: HOL4 has a simplifer that

  1668   %We would still need 

  1662   can rewrite terms modulo an arbitrary equivalence relation, which

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

  1663   Isabelle unfortunately does not yet have.  Even though we would

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

  1664   still need to connect $\lambda$-terms somehow to Turing machines for

  1665   proofs that make essential use of them (for example the

  1666   undecidability proof for Wang's tiling problem \cite{Robinson71}).

  1682   form. If the title had not already been taken in \cite{Nipkow98}, we could

  1678   form. Like Nipkow \cite{Nipkow98} observed with his formalisation

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

  1679   of a textbook, we found that Boolos et al are (almost)

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

  1680   right. We have not attempted to formalise everything precisely as

  1691   %The most closely related work is by Norrish \cite{Norrish11}, and by

  1687    Norrish mentions that formalising Turing machines would be a

  1692   %Asperti and Ricciotti \cite{AspertiRicciotti12}. 

  1688   ``\emph{daunting prospect}'' \cite[Page 310]{Norrish11}. While

  1693   Norrish mentions

  1689   $\lambda$-terms indeed lead to some slick mechanised proofs, our

  1694   that formalising Turing machines would be a ``\emph{daunting prospect}''

  1690   experience is that Turing machines are not too daunting if one is

  1695   \cite[Page 310]{Norrish11}. While $\lambda$-terms indeed lead to

  1691   only concerned with formalising the undecidability of the halting

  1696   some slick mechanised proofs, our experience is that Turing machines

  1692   problem for Turing machines.  As a point of comparison, the halting

  1697   are not too daunting if one is only concerned with formalising the

  1693   problem took us around 1500 loc of Isar-proofs, which is just

  1698   undecidability of the halting problem for Turing machines.  As a point of 

  1694   one-and-a-half times of a mechanised proof pearl about the

  1699   comparison, the halting problem

  1695   Myhill-Nerode theorem. So our conclusion is that this part is not as

  1700   took us around 1500 loc of Isar-proofs, which is just one-and-a-half

  1696   daunting as we estimated when reading the paper by Norrish

  1701   times of a mechanised proof pearl about the Myhill-Nerode

  1697   \cite{Norrish11}. The work involved with constructing a universal

  1702   theorem. So our conclusion is that this part is not as daunting 

  1698   Turing machine via recursive functions and abacus machines, we

  1703   as we estimated when reading the paper by Norrish \cite{Norrish11}. The work

  1699   agree, is not a project one wants to undertake too many times (our

  1704   involved with constructing a universal Turing machine via recursive

  1700   formalisation of abacus machines and their correct translation is

  1705   functions and abacus machines, we agree, is not a project

  1701   approximately 4600 loc; recursive functions 2800 loc and the

  1706   one wants to undertake too many times (our formalisation of abacus

  1702   universal Turing machine 10000 loc).

  1707   machines and their correct translation is approximately 4600 loc;

  1708   recursive functions 2800 loc and the universal Turing machine 10000 loc).

  1741   automation beyond the standard automation tools available in Isabelle/HOL. 

  1735   automation beyond the standard automation tools available in

  1742   There is however a tantalising connection

  1736   Isabelle/HOL.  There is however a tantalising connection between our

  1743   between our work and very recent work by Jensen et al \cite{Jensen13} on verifying

  1737   work and very recent work by Jensen et al \cite{Jensen13} on

  1744   X86 assembly code that might change that. They observed a similar phenomenon with assembly

  1738   verifying X86 assembly code that might change that. They observed a

  1745   programs where Hoare-style reasoning is sometimes possible, but

  1739   similar phenomenon with assembly programs where Hoare-style

  1746   sometimes it is not. In order to ease their reasoning, they

  1740   reasoning is sometimes possible, but sometimes it is not. In order

  1747   introduced a more primitive specification logic, on which

  1741   to ease their reasoning, they introduced a more primitive

  1748   Hoare-rules can be provided for special cases.  It remains to be

  1742   specification logic, on which Hoare-rules can be provided for

  1749   seen whether their specification logic for assembly code can make it

  1743   special cases.  It remains to be seen whether their specification

  1750   easier to reason about our Turing programs. Myreen ??? That would be an

  1744   logic for assembly code can make it easier to reason about our

  1751   attractive result, because Turing machine programs are very much

  1745   Turing programs. That would be an attractive result, because Turing

  1752   like assembly programs and it would connect some very classic work on

  1746   machine programs are very much like assembly programs and it would

  1753   Turing machines to very cutting-edge work on machine code

  1747   connect some very classic work on Turing machines to very

  1754   verification. In order to try out such ideas, our formalisation provides the

  1748   cutting-edge work on machine code verification. In order to try out

  1755   ``playground''. The code of our formalisation is available from the

  1749   such ideas, our formalisation provides the ``playground''. The code

  1750   of our formalisation is available from the