diff -r 8f89170bb076 -r e0a7ee9842d6 Paper/Paper.thy
--- a/Paper/Paper.thy	Fri Mar 29 01:36:45 2013 +0000
+++ b/Paper/Paper.thy	Fri Mar 29 02:40:38 2013 +0000
@@ -280,36 +280,39 @@
 %formalise in Isabelle/HOL computability arguments about the
 %algorithms. 
 
+%Suppose you want to mechanise a proof for whether a predicate @{term P}, 
+%say, is decidable or not. Decidability of @{text P} usually
+%amounts to showing whether \mbox{@{term "P \<or> \<not>P"}} holds. But this
+%does \emph{not} work in 
 
-\noindent
-Suppose you want to mechanise a proof for whether a predicate @{term
-P}, say, is decidable or not. Decidability of @{text P} usually
-amounts to showing whether \mbox{@{term "P \<or> \<not>P"}} holds. But this
-does \emph{not} work in Isabelle/HOL and other HOL theorem provers,
-since they are based on classical logic where the law of excluded
-middle ensures that \mbox{@{term "P \<or> \<not>P"}} is always provable no
-matter whether @{text P} is constructed by computable means. We hit on
-this limitation previously when we mechanised the correctness proofs
-of two algorithms \cite{UrbanCheneyBerghofer11,WuZhangUrban12}, but
-were unable to formalise arguments about decidability or undecidability.
+
+%Since Isabelle/HOL and other HOL theorem provers,
+%are based on classical logic where the law of excluded
+%middle ensures that \mbox{@{term "P \<or> \<not>P"}} is always provable no
+%matter whether @{text P} is constructed by computable means. We hit on
+%this limitation previously when we mechanised the correctness proofs
+%of two algorithms \cite{UrbanCheneyBerghofer11,WuZhangUrban12}, but
+%were unable to formalise arguments about decidability or undecidability.
 
 %The same problem would arise if we had formulated
 %the algorithms as recursive functions, because internally in
 %Isabelle/HOL, like in all HOL-based theorem provers, functions are
 %represented as inductively defined predicates too.
 
-The only satisfying way out of this problem in a theorem prover based
-on classical logic is to formalise a theory of computability. Norrish
-provided such a formalisation for HOL4. He choose the
-$\lambda$-calculus as the starting point for his formalisation because
-of its ``simplicity'' \cite[Page 297]{Norrish11}.  Part of his
-formalisation is a clever infrastructure for reducing
-$\lambda$-terms. He also established the computational equivalence
-between the $\lambda$-calculus and recursive functions.  Nevertheless
-he concluded that it would be appealing to have formalisations for
-more operational models of computations, such as Turing machines or
-register machines.  One reason is that many proofs in the literature
-use them.  He noted however that \cite[Page 310]{Norrish11}:
+\noindent
+The motivation of this paper is to bring the ability to reason
+about results from computability theory, for example decidability of the halting problem,
+to the theorem prover Isabelle/HOL.  Norrish formalised computability
+theory in HOL4. He choose the $\lambda$-calculus as the starting point
+for his formalisation because of its ``simplicity'' \cite[Page
+297]{Norrish11}.  Part of his formalisation is a clever infrastructure
+for reducing $\lambda$-terms. He also established the computational
+equivalence between the $\lambda$-calculus and recursive functions.
+Nevertheless he concluded that it would be appealing to have
+formalisations for more operational models of computations, such as
+Turing machines or register machines.  One reason is that many proofs
+in the literature use them.  He noted however that \cite[Page
+310]{Norrish11}:
 
 \begin{quote}
 \it``If register machines are unappealing because of their 
@@ -410,6 +413,10 @@
 \cite{Boolos87} by translating abacus machines to Turing machines and in
 turn recursive functions to abacus machines. The universal Turing
 machine can then be constructed by translating from a recursive function. 
+The part of mechanising the translation of recursive function to register 
+machines has already been done by Zammit in HOL \cite{Zammit99}, 
+although his register machines use a slightly different instruction
+set than the one described in \cite{Boolos87}.
 
 \smallskip
 \noindent
@@ -1244,7 +1251,7 @@
 
   \noindent
   This time the Hoare-triple states that @{term tcontra} terminates 
-  with the ``output'' @{term "<(1::nat)>"}. In both case we come
+  with the ``output'' @{term "<(1::nat)>"}. In both cases we come
   to a contradiction, which means we have to abandon our assumption 
   that there exists a Turing machine @{term H} which can in general decide 
   whether Turing machines terminate.
@@ -1519,7 +1526,7 @@
   unexpected since \cite{Boolos87} is a classic textbook which has
   undergone several editions (we used the fifth edition; the material 
   containing the inconsistency was introduced in the fourth edition
-  \cite{BoolosFourth}). The central
+  of this book). The central
   idea about Turing machines is that when started with standard tapes
   they compute a partial arithmetic function.  The inconsistency arises
   when they define the case when this function should \emph{not} return a
@@ -1740,6 +1747,11 @@
   verification. In order to try out such ideas, our formalisation provides the
   ``playground''. The code of our formalisation is available from the
   Mercurial repository at \url{http://www.dcs.kcl.ac.uk/staff/urbanc/cgi-bin/repos.cgi/tm/}.
+  \medskip
+
+  \noindent
+  {\bf Acknowledgements:} We are very grateful for the extremely helpful
+  comments by the anonymous reviewers.
 *}