1368   We have formalised the main computability results from Chapters 3 to 8 in the

  1368   In previous works we were unable to formalise results about

  1369   textbook by Boolos et al \cite{Boolos87}.  Following in the

  1369   computability because in a Isabelle/HOL we cannot represent the

  1370   footsteps of another paper \cite{Nipkow98} formalising the results

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

  1371   from a semantics textbook, we could have titled our paper ``Boolos et al are

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

  1372   (almost) Right''. We have not attempted to formalise everything

  1372   concrete model of computations. We could have followed Norrish

  1373   precisely as Boolos et al present it, but use definitions that make

  1373   \cite{Norrish11} using the $\lambda$-calculus as the starting point,

  1374   mechanised proofs manageable. For example our definition of the 

  1374   but then we would have to reimplement his infrastructure for

  1375   halting state performing @{term Nop}-operations seems to be non-standard, 

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

  1376   but very much suited to a formalisation in a theorem prover where

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

  1377   the @{term steps}-function need to be total. We have found an 

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

  1378   inconsistency in

  1378 

  1379   Bolos et al's usage of definitions of \ldots 

  1379   We therefore have formalised Turing machines and the main

  1380   Our interest in Turing machines 

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

  1381   arose from correctness proofs about algorithms where we were unable

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

  1382   to formalise arguments about decidability but also undecidability

  1382   anything on the ML-level of Isabelle/HOL. While formalising

  1383   proofs in general (for example Wang's tiling problem \cite{Robinson71}).

  1383   \cite{Boolos87} have found an inconsistency in Bolos et al's usage

  1384   of definitions of what function a Turing machine calculates. In

  1385   Chapter 3 they use a definition such that the function is undefined

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

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

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

  1389   form. Following in the footsteps of another paper \cite{Nipkow98}

  1390   formalising the results from a semantics textbook, we could

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

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

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

  1394   mechanised proofs manageable. For example our definition of the

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

  1396   non-standard, but very much suited to a formalisation in a theorem

  1397   prover where the @{term steps}-function need to be total.