--- a/Paper/Paper.thy	Thu Jan 24 00:20:26 2013 +0100
+++ b/Paper/Paper.thy	Thu Jan 24 10:53:43 2013 +0100
@@ -96,7 +96,7 @@
 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 computability.
+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
@@ -218,7 +218,8 @@
 occupied cells. We mechanise the undecidability of the halting problem and
 prove the correctness of concrete Turing machines that are needed
 in this proof; such correctness proofs are left out in the informal literature.  
-We construct the universal Turing machine from \cite{Boolos87} by
+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
 Turing machines. Since we have set up in Isabelle/HOL a very general computability
 model and undecidability result, we are able to formalise other
@@ -425,12 +426,47 @@
   state, and the third that every next-state is one of the states mentioned in
   the program or being the @{text 0}-state.
 
-  A \emph{configuration} @{term c} of a Turing machine is a state together with 
-  a tape. This is written as @{text "(s, (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 the function @{term step}
+  We need to be able to sequentially compose Turing machine programs. Given our
+  concrete representation, this is relatively straightforward, if
+  slightly fiddly. We use the following two auxiliary functions:
+
+  \begin{center}
+  \begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {}}
+  @{thm (lhs) shift.simps} @{text "\<equiv>"} @{thm (rhs) shift.simps}\\
+  @{thm (lhs) adjust.simps} @{text "\<equiv>"} @{thm (rhs) adjust.simps}\\
+  \end{tabular}
+  \end{center}
+
+  \noindent
+  The first adds @{text n} to all states, exept the @{text 0}-state,
+  thus moving all ``regular'' states to the segment starting at @{text
+  n}; the second adds @{term "Suc(length p div 2)"} to the @{text
+  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"}
+
+  \begin{center}
+  @{thm tm_comp.simps[where ?p1.0="p\<^isub>1" and ?p2.0="p\<^isub>2", THEN eq_reflection]}
+  \end{center}
+
+  \noindent
+  %This means @{text "p\<^isub>1"} is executed first. Whenever it originally
+  %transitioned to the @{text 0}-state, it will in the composed program transition to the starting
+  %state of @{text "p\<^isub>2"} instead. All the states of @{text "p\<^isub>2"}
+  %have been shifted in order to make sure that the states of the composed 
+  %program @{text "p\<^isub>1 \<oplus> p\<^isub>2"} still only ``occupy'' 
+  %an initial segment of the natural numbers.
+
+  A \emph{configuration} @{term c} of a Turing machine is a state
+  together with a tape. This is written as @{text "(s, (l, r))"}.  We
+  say a configuration is \emph{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
+  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
+  the function @{term step}
 
   \begin{center}
   \begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}l}
@@ -463,38 +499,19 @@
   remains there performing @{text Nop}-actions until @{text n} is reached. 
 
   Before we can prove the undecidability of the halting problem for Turing machines, 
-  we have to define how to compose two Turing machine programs. Given our setup, this is 
-  relatively straightforward, if slightly fiddly. We use the following two
-  auxiliary functions:
+  we need to analyse two concrete Turing machine programs and establish that
+  they ``doing what they are supposed to be doing''. To do so we will derive
+  some Hoare-style reasoning rules for Turing machine programs. A \emph{Hoare-triple}
+  for a terminating Turing machine program is defined as
 
   \begin{center}
-  \begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {}}
-  @{thm (lhs) shift.simps} @{text "\<equiv>"} @{thm (rhs) shift.simps}\\
-  @{thm (lhs) adjust.simps} @{text "\<equiv>"} @{thm (rhs) adjust.simps}\\
-  \end{tabular}
+  @{thm Hoare_halt_def}
   \end{center}
 
-  \noindent
-  The first adds @{text n} to all states, exept the @{text 0}-state,
-  thus moving all ``regular'' states to the segment starting at @{text
-  n}; the second adds @{term "Suc(length p div 2)"} to the @{text
-  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"}
-
   \begin{center}
-  @{thm tm_comp.simps[where ?p1.0="p\<^isub>1" and ?p2.0="p\<^isub>2", THEN eq_reflection]}
+  @{thm Hoare_unhalt_def}
   \end{center}
 
-  \noindent
-  %This means @{text "p\<^isub>1"} is executed first. Whenever it originally
-  %transitioned to the @{text 0}-state, it will in the composed program transition to the starting
-  %state of @{text "p\<^isub>2"} instead. All the states of @{text "p\<^isub>2"}
-  %have been shifted in order to make sure that the states of the composed 
-  %program @{text "p\<^isub>1 \<oplus> p\<^isub>2"} still only ``occupy'' 
-  %an initial segment of the natural numbers.
-
   In the following we will consider the following Turing machine program
   that makes a copies a value on the tape.