--- a/Paper/Paper.thy	Thu Jan 24 17:40:04 2013 +0100
+++ b/Paper/Paper.thy	Thu Jan 24 18:59:49 2013 +0100
@@ -92,15 +92,16 @@
 
 
 \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 this limitation previously when we mechanised the correctness
-proofs of two algorithms \cite{UrbanCheneyBerghofer11,WuZhangUrban12}, 
-but were unable to formalise arguments about decidability.
+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.
 
 %The same problem would arise if we had formulated
 %the algorithms as recursive functions, because internally in
@@ -138,8 +139,8 @@
 programs.  We provide such Hoare-rules for when it \emph{is} possible to
 reason in a compositional manner (which is fortunately quite often), but also tackle 
 the more complicated case when we translate abacus programs into 
-Turing programs.  These difficulties when reasoning about computability theory 
-are usually completely left out in the informal literature, e.g.~\cite{Boolos87}.
+Turing programs.  This reasoning about Turing machine programs is
+usually completely left out in the informal literature, e.g.~\cite{Boolos87}.
 
 %To see the difficulties
 %involved with this work, one has to understand that interactive
@@ -224,7 +225,7 @@
 in this proof; such correctness proofs are left out in the informal literature.  
 For reasoning about Turing machine programs we derive Hoare-rules.
 We also construct the universal Turing machine from \cite{Boolos87} by
-relating recursive functions to abacus machines and abacus machines to
+translating recursive functions to abacus machines and abacus machines to
 Turing machines. Since we have set up in Isabelle/HOL a very general computability
 model and undecidability result, we are able to formalise other
 results: we describe a proof of the computational equivalence
@@ -279,7 +280,7 @@
   Note that by using lists each side of the tape is only finite. The
   potential infinity is achieved by adding an appropriate blank or occupied cell 
   whenever the head goes over the ``edge'' of the tape. To 
-  make this formal we define five possible \emph{actions}, @{text a} 
+  make this formal we define five possible \emph{actions} 
   the Turing machine can perform:
 
   \begin{center}
@@ -384,7 +385,7 @@
 
   \noindent
   the reader can see we have organised our Turing machine programs so
-  that segments of two belong to a state. The first component of the
+  that segments of two belong to a state. The first component of such a
   segment determines what action should be taken and which next state
   should be transitioned to in case the head reads a @{term Bk};
   similarly the second component determines what should be done in
@@ -451,7 +452,7 @@
   0}-state, thus redirecting all references to the ``halting state''
   to the first state after the program @{text p}.  With these two
   functions in place, we can define the \emph{sequential composition}
-  of two Turing machine programs @{text "p\<^isub>1"} and @{text "p\<^isub>2"}
+  of two Turing machine programs @{text "p\<^isub>1"} and @{text "p\<^isub>2"} as
 
   \begin{center}
   @{thm tm_comp.simps[where ?p1.0="p\<^isub>1" and ?p2.0="p\<^isub>2", THEN eq_reflection]}
@@ -469,7 +470,7 @@
   together with a tape. This is written as @{text "(s, (l, r))"}.  We
   say a configuration \emph{is final} if @{term "s = (0::nat)"} and we
   say a predicate @{text P} \emph{holds for} a configuration if @{text
-  "P (l, r)"} holds.  If we have a configuration and a program, we can
+  "P"} holds for the tape @{text "(l, r)"}.  If we have a configuration and a program, we can
   calculate what the next configuration is by fetching the appropriate
   action and next state from the program, and by updating the state
   and tape accordingly.  This single step of execution is defined as
@@ -485,11 +486,11 @@
   \noindent
   where @{term "read r"} returns the head of the list @{text r}, or if @{text r} is
   empty it returns @{term Bk}.
-  It is impossible in Isabelle/HOL to lift the @{term step}-function realising
+  It is impossible in Isabelle/HOL to lift the @{term step}-function to realise
   a general evaluation function for Turing machines. The reason is that functions in HOL-based
   provers need to be terminating, and clearly there are Turing machine 
   programs that are not. We can however define an evaluation
-  function so that it performs exactly @{text n} steps:
+  function that performs exactly @{text n} steps:
 
   \begin{center}
   \begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}l}
@@ -521,13 +522,15 @@
   \caption{Copy machine}\label{copy}
   \end{figure}
 
-  Before we can prove the undecidability of the halting problem for
+  {\it tapes in standard form}
+
+  Before we can prove the undecidability of the halting problem for our
   Turing machines, we need to analyse two concrete Turing machine
-  programs and establish that they are correct, that means they are
-  ``doing what they are supposed to be doing''.  This is usually left
+  programs and establish that they are correct---that means they are
+  ``doing what they are supposed to be doing''.  Such correctness proofs are usually left
   out in the informal literature, for example \cite{Boolos87}.  One program 
   we need to prove correct is the @{term dither} program shown in \eqref{dither} 
-  and the other program @{term "tcopy"} is defined as
+  and the other program is @{term "tcopy"} is defined as
 
   \begin{center}
   \begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {}}
@@ -536,16 +539,17 @@
   \end{center}
 
   \noindent
-  whose three components are given in Figure~\ref{copy}. To prove correctness, 
-  we introduce the notion of total correctness defined in terms of 
-  \emph{Hoare-triples}, written @{term "{P} p {Q}"}. They realise the idea
-  that a program @{term p} started in state @{term "1::nat"} with a tape 
-  satisfying @{term P} will after @{text n} steps halt (have transitioned into 
-  the halting state) with a tape satisfying @{term Q}. We also have 
-  \emph{Hoare-pairs} of the form @{term "{P} p \<up>"} realising the case that a 
-  program @{term p} started with a tape satisfying @{term P} will loop 
-  (never transition into the halting state). Both notion are formally 
-  defined as
+  whose three components are given in Figure~\ref{copy}. To the prove
+  correctness of these Turing machine programs, we introduce the
+  notion of total correctness defined in terms of
+  \emph{Hoare-triples}, written @{term "{P} p {Q}"}. They realise the
+  idea that a program @{term p} started in state @{term "1::nat"} with
+  a tape satisfying @{term P} will after @{text n} steps halt (have
+  transitioned into the halting state) with a tape satisfying @{term
+  Q}. We also have \emph{Hoare-pairs} of the form @{term "{P} p \<up>"}
+  realising the case that a program @{term p} started with a tape
+  satisfying @{term P} will loop (never transition into the halting
+  state). Both notion are formally defined as
 
   \begin{center}
   \begin{tabular}{@ {}c@ {\hspace{4mm}}c@ {}}
@@ -567,11 +571,13 @@
   \end{center}
   
   \noindent
-  We have set up our Hoare-style reasoning to deal explicitly with 
-  looping and total correctness, rather separate notions for partial 
-  correctness and termination, is because we can derive simple rules 
-  for sequentially composed Turing programs. They allow us to reason
-  about correctness of components completely separately.
+  We have set up our Hoare-style reasoning so that we can deal explicitly 
+  with looping and total correctness, rather than have notions for partial 
+  correctness and termination. Although the latter would allow us to reason
+  more uniformly (only using Hoare-triples), we prefer our definitions because 
+  we can derive simple Hoare-rules for sequentially composed Turing programs. 
+  In this way we can reason about the correctness of @{term "tcopy_init"},
+  for example, completely separately from @{term "tcopy_loop"}.
 
   It is rather straightforward to prove that the Turing program 
   @{term "dither"} satisfies the following correctness properties