diff -r b92529dc95c5 -r 90bc8cccc218 Paper.thy
--- a/Paper.thy	Sat Jan 05 00:31:43 2013 +0000
+++ b/Paper.thy	Sun Jan 06 23:50:24 2013 +0000
@@ -60,27 +60,28 @@
 theorem provers, like Isabelle/HOL, are at their best when the
 data-structures at hand are ``structurally'' defined, like lists,
 natural numbers, regular expressions, etc. Such data-structures come
-in theorem provers with convenient reasoning infrastructures (for
+convenient reasoning infrastructures (for
 example induction principles, recursion combinators and so on).  But
 this is \emph{not} the case with Turing machines (and also not with
 register machines): underlying their definition is a set of states
 together with a transition function, both of which are not
 structurally defined.  This means we have to implement our own
 reasoning infrastructure in order to prove properties about them. This
-leads to annoyingly lengthy and detailed formalisations.  We noticed
+leads to annoyingly lengthy and fiddly formalisations.  We noticed
 first the difference between both structural and non-structural
 ``worlds'' when formalising the Myhill-Nerode theorem, where regular
 expressions fared much better than automata \cite{WuZhangUrban11}.
 However, with Turing machines there seems to be no alternative if one
-wants to formalise the great many proofs that use them. We give as
-example one proof---undecidability of Wang tilings---in Section
-\ref{Wang}. The standard proof of this property uses the notion of
-\emph{universal Turing machines}.
+wants to formalise the great many proofs from the literature that use them.
+We will analyse one example---undecidability of Wang tilings---in 
+detail in Section~\ref{Wang}. The standard proof of this property uses 
+the notion of \emph{universal Turing machines}.
 
 We are not the first who formalised Turing machines in a theorem
 prover: we are aware of the preliminary work by Asperti and Ricciotti
-\cite{AspertiRicciotti12}. They describe a formalisation of Turing
-machines in the Matita theorem prover. They report 
+\cite{AspertiRicciotti12}. They describe a complete formalisation of Turing
+machines in the Matita theorem prover, including an universal Turing
+machine. They report 
 that the informal proofs from which they started are not 
 ``sufficiently accurate to be directly used as a guideline for 
 formalization'' \cite[Page 2]{AspertiRicciotti12}. For our formalisation 
@@ -92,20 +93,26 @@
 $n$-ary functions. Similarly, when compiling recursive functions to 
 abacus machines, the textbook again only shows how it can be done for 
 2- and 3-ary functions, but in the formalisation we need arbitrary 
-function. But the general ideas for how to do this are clear enough in 
+functions. But the general ideas for how to do this are clear enough in 
 \cite{Boolos87}.
 
 The main difference between our formalisation and the one by Asperti and
-Ricciotti is 
+Ricciotti  is that their universal Turing 
+machine uses a different alphabet than the machines it simulates. They
+write \cite[Page XXX]{AspertiRicciotti12}:
 
-that their universal machines 
-
-\begin{quote}
+\begin{quote}\it
 ``In particular, the fact that the universal machine operates with a
 different alphabet with respect to the machines it simulates is
 annoying.'' 
 \end{quote}
 
+\noindent
+In this paper we follow the approach by Boolos et al \cite{Boolos87}
+where Turing machines (and our
+universal Turing machine) operates on tapes that contain only blank
+or filled cells (respectively represented by 0 and 1---or in our 
+formalisation by @{term Bk} or @{term Oc}).