63 with convenient reasoning infrastructures (for

    63 with convenient reasoning infrastructures (for example induction

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

    64 principles, recursion combinators and so on).  But this is \emph{not}

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

    65 the case with Turing machines (and also not with register machines):

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

    66 underlying their definition is a set of states together with a

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

    67 transition function, both of which are not structurally defined.  This

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

    68 means we have to implement our own reasoning infrastructure in order

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

    69 to prove properties about them. This leads to annoyingly fiddly

    70 leads to annoyingly fiddly formalisations.  We noticed

    70 formalisations.  We noticed first the difference between both,

    71 first the difference between both, structural and non-structural,

    71 structural and non-structural, ``worlds'' when formalising the

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

    72 Myhill-Nerode theorem, where regular expressions fared much better

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

    73 than automata \cite{WuZhangUrban11}.  However, with Turing machines

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

    74 there seems to be no alternative if one wants to formalise the great

    75 wants to formalise the great many proofs from the literature that use them.

    75 many proofs from the literature that use them.  We will analyse one

    76 We will analyse one example---undecidability of Wang tilings---in 

    76 example---undecidability of Wang tilings---in Section~\ref{Wang}. The

    77 Section~\ref{Wang}. The standard proof of this property uses 

    77 standard proof of this property uses the notion of \emph{universal

    78 the notion of \emph{universal Turing machines}.

    78 Turing machines}.

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

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

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

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

    84 machine. They report 

    84 Turing machine. They report that the informal proofs from which they

    85 that the informal proofs from which they started are not 

    85 started are not ``sufficiently accurate to be directly used as a

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

    86 guideline for formalization'' \cite[Page 2]{AspertiRicciotti12}. For

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

    87 our formalisation we followed the proofs from the textbook

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

    88 \cite{Boolos87} and found that the description there is quite

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

    89 detailed. Some details are left out however: for example, it is only

    90 example, it is only shown how the universal

    90 shown how the universal Turing machine is constructed for Turing

    91 Turing machine is constructed for Turing machines computing unary 

    91 machines computing unary functions. We had to figure out a way to

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

    92 generalize this result to $n$-ary functions. Similarly, when compiling

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

    93 recursive functions to abacus machines, the textbook again only shows

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

    94 how it can be done for 2- and 3-ary functions, but in the

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

    95 formalisation we need arbitrary functions. But the general ideas for

    96 functions. But the general ideas for how to do this are clear enough in 

    96 how to do this are clear enough in \cite{Boolos87}. However, one

    97 \cite{Boolos87}.

    97 aspect that is completely left out from the informal description in

    98 \cite{Boolos87}, and similar ones we are aware of, are arguments why certain Turing

    99 machines are correct. We will introduce Hoare-style proof rules

   100 which help us with such correctness arguments of Turing machines.

    99 The main difference between our formalisation and the one by Asperti and

   102 The main difference between our formalisation and the one by Asperti

   100 Ricciotti  is that their universal Turing 

   103 and Ricciotti is that their universal Turing machine uses a different

   101 machine uses a different alphabet than the machines it simulates. They

   104 alphabet than the machines it simulates. They write \cite[Page

   102 write \cite[Page 23]{AspertiRicciotti12}:

   105 23]{AspertiRicciotti12}:

   111 In this paper we follow the approach by Boolos et al \cite{Boolos87}

   114 In this paper we follow the approach by Boolos et al \cite{Boolos87},

   112 where Turing machines (and our

   115 which goes back to Post \cite{Post36}, where all Turing machines

   113 universal Turing machine) operates on tapes that contain only blank

   116 operate on tapes that contain only blank or filled cells (represented 

   114 or filled cells (respectively represented by 0 and 1---or in our 

   117 by @{term Bk} and @{term Oc}, respectively, in our

   115 formalisation by @{term Bk} and @{term Oc}).

   118 formalisation). Traditionally the content of a cell can be any

   119 character from a finite alphabet. Although computationally

   120 equivalennt, the more restrictive notion of Turing machines make

   121 the reasoning more uniform. Unfortunately, it also makes it

   122 harder to design programs for Turing machines. Therefore

   123 in order to construct a \emph{universal Turing machine} we follow

   124 the proof in \cite{Boolos87} by relating abacus machines to

   125 turing machines and in turn recursive functions to abacus machines. 

   117 

   127 \medskip

   118 

   124 section {* Formalisation *}

   133 section {* Turing Machines *}

   141   The most closely related work is by Norrish. He bases his approach on 

   176   The most closely related work is by Norrish \cite{Norrish11}, and Asperti and 

   177   Ricciotti \cite{AspertiRicciotti12}. Norrish bases his approach on