
diff -r 07730607b0ca -r 38d8e0e37b7d Paper/Paper.thy
--- a/Paper/Paper.thy	Thu Feb 07 01:00:55 2013 +0000
+++ b/Paper/Paper.thy	Thu Feb 07 03:01:51 2013 +0000
@@ -1,6 +1,6 @@
 (*<*)
 theory Paper
-imports "../thys/recursive"
+imports "../thys/UTM"
 begin
 
 
@@ -1329,6 +1329,33 @@
   with the standard tape @{term "([Bk, Bk], <ns::nat list>)"} will terminate
   with the standard tape @{term "(Bk \<up> k, <n::nat> @ Bk \<up> l)"} for some @{text k} and @{text l}.
 
+  Having 
+
+  we can prove that if 
+
+  \begin{center}
+  @{thm (prem 3) UTM_halt_lemma2}
+  \end{center}
+  then 
+
+  \begin{center}
+  @{thm (concl) UTM_halt_lemma2} 
+  \end{center}
+
+  under the assumption that @{text p}
+  is well-formed and the arguments are not empty.
+
+
+  \begin{center}
+  @{thm (prem 2) UTM_unhalt_lemma2}
+  \end{center}
+  then 
+
+  \begin{center}
+  @{thm (concl) UTM_unhalt_lemma2} 
+  \end{center}
+
+
   and the also the definition of the
   universal function (we refer the reader to our formalisation).
 
@@ -1358,6 +1385,7 @@
   but with @{term "([], [Oc])"} according to def Chap 8
 *}
 
+(*
 section {* XYZ *}
 
 text {*
@@ -1406,6 +1434,7 @@
 \]
 In summary, according to Chapter 3, the Turing machine in \eqref{contrived_tm} computes non-result and according to Chapter 8, it computes an identify function. 
 *}
+*)
 
 (*
 section {* Wang Tiles\label{Wang} *}
@@ -1432,39 +1461,39 @@
   We therefore have formalised Turing machines and the main
   computability results from Chapters 3 to 8 in the textbook by Boolos
   et al \cite{Boolos87}.  For this we did not need to implement
-  anything on the ML-level of Isabelle/HOL. While formalising
+  anything on the ML-level of Isabelle/HOL. While formalising the six chapters
   \cite{Boolos87} we have found an inconsistency in Bolos et al's 
   definitions of what function a Turing machine calculates. In
   Chapter 3 they use a definition that states a function is undefined
   if the Turing machine loops \emph{or} halts with a non-standard
   tape. Whereas in Chapter 8 about the universal Turing machine, the
   Turing machines will \emph{not} halt unless the tape is in standard
-  form. Following in the footsteps of another paper \cite{Nipkow98}
-  formalising the results from a semantics textbook, we could
-  therefore have titled our paper ``Boolos et al are (almost)
+  form. If the title had not already been taken \cite{Nipkow98}, we could
+  have titled our paper ``Boolos et al are (almost)
   Right''. We have not attempted to formalise everything precisely as
   Boolos et al present it, but use definitions that make our
   mechanised proofs manageable. For example our definition of the
   halting state performing @{term Nop}-operations seems to be
   non-standard, but very much suited to a formalisation in a theorem
-  prover where the @{term steps}-function need to be total.
+  prover where the @{term steps}-function needs to be total.
 
-  The most closely related work is by Norrish \cite{Norrish11}, and by
-  Asperti and Ricciotti \cite{AspertiRicciotti12}. Norrish mentions
-  that formalising Turing machines would be a ``daunting prospect''
+  %The most closely related work is by Norrish \cite{Norrish11}, and by
+  %Asperti and Ricciotti \cite{AspertiRicciotti12}. 
+  Norrish mentions
+  that formalising Turing machines would be a ``\emph{daunting prospect}''
   \cite[Page 310]{Norrish11}. While $\lambda$-terms indeed lead to
   some slick mechanised proofs, our experience is that Turing machines
   are not too daunting if one is only concerned with formalising the
   undecidability of the halting problem for Turing machines.  This
   took us around 1500 loc of Isar-proofs, which is just one-and-a-half
   times of a mechanised proof pearl about the Myhill-Nerode
-  theorem. So our conclusion is it not as daunting as we estimated
-  when reading the paper by Norrish \cite{Norrish11}. The work
+  theorem. So our conclusion is that it not as daunting for this part of the
+  work as we estimated when reading the paper by Norrish \cite{Norrish11}. The work
   involved with constructing a universal Turing machine via recursive
-  functions and abacus machines, on the other hand, is not a project
+  functions and abacus machines, we agree, is not a project
   one wants to undertake too many times (our formalisation of abacus
   machines and their correct translation is approximately 4300 loc;
-  recursive functions XX loc and the universal Turing machine XX loc).
+  recursive functions 5000 loc and the universal Turing machine 10000 loc).
   
   Our work was also very much inspired by the formalisation of Turing
   machines by Asperti and Ricciotti \cite{AspertiRicciotti12} in the
@@ -1481,38 +1510,38 @@
   For us the most interesting aspect of our work are the correctness
   proofs for Turing machines. Informal presentations of computability
   theory often leave the constructions of particular Turing machines
-  as exercise to the reader, as for example \cite{Boolos87}, deeming
+  as exercise to the reader, for example \cite{Boolos87}, deeming
   it to be just a chore. However, as far as we are aware all informal
   presentations leave out any arguments why these Turing machines
-  should be correct.  This means the reader or formalsiser is left
+  should be correct.  This means the reader is left
   with the task of finding appropriate invariants and measures for
   showing correctness and termination of these Turing machines.
   Whenever we can use Hoare-style reasoning, the invariants are
   relatively straightforward and much smaller than for example the
   invariants used by Myreen in a correctness proof of a garbage collector
-  written in machine code \cite[Page 76]{Myreen09}. Howvere, the invariant 
+  written in machine code \cite[Page 76]{Myreen09}. However, the invariant 
   needed for the abacus proof, where Hoare-style reasoning does not work, is
   similar in size as the one by Myreen and finding a sufficiently
   strong one took us, like Myreen for his, something on the magnitude of
   weeks.
 
   Our reasoning about the invariants is not much supported by the
-  automation in Isabelle. There is however a tantalising connection
+  automation beyond the standard automation tools available in Isabelle/HOL. 
+  There is however a tantalising connection
   between our work and very recent work \cite{Jensen13} on verifying
-  X86 assembly code. They observed a similar phenomenon with assembly
+  X86 assembly code that might change that. They observed a similar phenomenon with assembly
   programs that Hoare-style reasoning is sometimes possible, but
-  sometimes it is not. In order to ease their reasoning they
+  sometimes it is not. In order to ease their reasoning, they
   introduced a more primitive specification logic, on which
   Hoare-rules can be provided for special cases.  It remains to be
   seen whether their specification logic for assembly code can make it
   easier to reason about our Turing programs. That would be an
   attractive result, because Turing machine programs are very much
-  like assmbly programs and it would connect some very classic work on
-  Turing machines with very cutting-edge work on machine code
+  like assembly programs and it would connect some very classic work on
+  Turing machines to very cutting-edge work on machine code
   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/}.
+  Mercurial repository at \url{http://www.dcs.kcl.ac.uk/staff/urbanc/cgi-bin/repos.cgi/tm/}.
 *}
 
 




