56 In this paper we took on this daunting prospect and provide a formalisation

    56 In this paper we took on this daunting prospect and provide a

    57 of Turing machines, as well as Abacus machines (a kind of register machine)

    57 formalisation of Turing machines, as well as abacus machines (a kind

    58 and recursive functions. To see the difficulties involved with this work one

    58 of register machines) and recursive functions. To see the difficulties

    59 has to understantd that interactive theorem provers, like Isabelle/HOL, are at 

    59 involved with this work, one has to understand that interactive

    60 their best when the data-structures 

    60 theorem provers, like Isabelle/HOL, are at their best when the

    61 at hand are ``structurally'' defined (like lists, natural numbers,

    61 data-structures at hand are ``structurally'' defined, like lists,

    62 regular expressions, etc). For them, they come with a convenient reasoning 

    62 natural numbers, regular expressions, etc. Such data-structures come

    63 infrastructure (for example induction principles, recursion combinators and so on).

    63 in theorem provers with convenient reasoning infrastructures (for

    64 But this is not the case with Turing machines  (and also register machines): 

    64 example induction principles, recursion combinators and so on).  But

    65 underlying their definition is a set of states

    65 this is \emph{not} the case with Turing machines (and also not with

    66 together with a transition function, both of which are not structurally defined. 

    66 register machines): underlying their definition is a set of states

    67 This means we have to implement our own reasoning infrastructure. This often

    67 together with a transition function, both of which are not

    68 leads to annoyingly lengthy and detailed formalisations.  We noticed first 

    68 structurally defined.  This means we have to implement our own

    69 the difference between both ``worlds'' when formalising the Myhill-Nerode 

    69 reasoning infrastructure in order to prove properties about them. This

    70 theorem ??? where regular expressions fared much better than automata. 

    70 leads to annoyingly lengthy and detailed formalisations.  We noticed

    71 However, with Turing machines there seems to be no alternative, because they

    71 first the difference between both structural and non-structural

    72 feature frequently in proofs. We will analyse one case, Wang tilings, at the end 

    72 ``worlds'' when formalising the Myhill-Nerode theorem, where regular

    73 of the paper, which uses also the notion of a Universal Turing Machine.

    73 expressions fared much better than automata \cite{WuZhangUrban11}.

    74 However, with Turing machines there seems to be no alternative if one

    75 wants to formalise the great many proofs that use them. We give as

    76 example one proof---undecidability of Wang tilings---in Section

    77 \ref{Wang}. The standard proof of this property uses the notion of

    78 \emph{universal Turing machines}.

    75 The reason why reasoning about Turing machines 

    80 We are not the first who formalised Turing machines in a theorem

    76 is challenging is because they are essentially ... 

    81 prover: we are aware of the preliminary work by Asperti and Ricciotti

    82 \cite{AspertiRicciotti12}. They describe a formalisation of Turing

    83 machines in the Matita theorem prover. They report 

    84 that the informal proofs from which they started are not 

    85 ``sufficiently accurate to be directly used as a guideline for 

    86 formalization'' \cite[Page 2]{AspertiRicciotti12}. For our formalisation 

    87 we followed the proofs from the textbook \cite{Boolos87} and found that the description

    88 is quite detailed. Some details are left out however: for 

    89 example, it is only shown how the universal

    90 Turing machine is constructed for Turing machines computing unary 

    91 functions. We had to figure out a way to generalize this result to

    92 $n$-ary functions. Similarly, when compiling recursive functions to 

    93 abacus machines, the textbook again only shows how it can be done for 

    94 2- and 3-ary functions, but in the formalisation we need arbitrary 

    95 function. But the general ideas for how to do this are clear enough in 

    96 \cite{Boolos87}.

    79 For this we followed mainly the informal

   101 that their universal machines 

    80 proof given in the textbook \cite{Boolos87}.

   102 

   103 \begin{quote}

   104 ``In particular, the fact that the universal machine operates with a

   105 different alphabet with respect to the machines it simulates is

   106 annoying.'' 

   107 \end{quote}

   104 section {* Wang Tiles *}

   124 section {* Wang Tiles\label{Wang} *}