--- a/Paper/Paper.thy	Thu Jan 24 10:53:43 2013 +0100
+++ b/Paper/Paper.thy	Thu Jan 24 11:38:07 2013 +0100
@@ -23,6 +23,9 @@
   update2 ("update") and
   tm_wf0 ("wf") and
   is_even ("iseven") and
+  tcopy_init ("copy\<^bsub>begin\<^esub>") and
+  tcopy_loop ("copy\<^bsub>loop\<^esub>") and
+  tcopy_end ("copy\<^bsub>end\<^esub>") and
 (*  abc_lm_v ("lookup") and
   abc_lm_s ("set") and*)
   haltP ("stdhalt") and 
@@ -166,7 +169,7 @@
 Turing machine. They report that the informal proofs from which they
 started are \emph{not} ``sufficiently accurate to be directly usable as a
 guideline for formalization'' \cite[Page 2]{AspertiRicciotti12}. For
-our formalisation we followed mainly the proofs from the textbook
+our formalisation we follow mainly the proofs from the textbook
 \cite{Boolos87} and found that the description there is quite
 detailed. Some details are left out however: for example, it is only
 shown how the universal Turing machine is constructed for Turing
@@ -352,9 +355,9 @@
   %states.\footnote{The usual disjoint union operation in Isabelle/HOL
   %cannot be used as it does not preserve types.} This renaming can be
   %quite cumbersome to reason about. 
-  We followed the choice made in \cite{AspertiRicciotti12} 
+  We follow the choice made in \cite{AspertiRicciotti12} 
   representing a state by a natural number and the states in a Turing
-  machine programme by the initial segment of natural numbers starting from @{text 0}.
+  machine program by the initial segment of natural numbers starting from @{text 0}.
   In doing so we can compose two Turing machine programs by
   shifting the states of one by an appropriate amount to a higher
   segment and adjusting some ``next states'' in the other. 
@@ -367,7 +370,10 @@
   \begin{equation}
   \begin{tikzpicture}
   \node [anchor=base] at (0,0) {@{thm dither_def}};
-  \node [anchor=west] at (-1.5,-0.42) {$\underbrace{\hspace{21mm}}_{\text{1st state}}$};
+  \node [anchor=west] at (-1.5,-0.64) 
+  {$\underbrace{\hspace{21mm}}_{\text{\begin{tabular}{@ {}l@ {}}1st state\\[-2mm] 
+  = starting state\end{tabular}}}$};
+  
   \node [anchor=west] at ( 1.1,-0.42) {$\underbrace{\hspace{17mm}}_{\text{2nd state}}$};
   \node [anchor=west] at (-1.5,0.65) {$\overbrace{\hspace{10mm}}^{\text{@{term Bk}-case}}$};
   \node [anchor=west] at (-0.1,0.65) {$\overbrace{\hspace{6mm}}^{\text{@{term Oc}-case}}$};
@@ -460,7 +466,7 @@
 
   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 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
   calculate what the next configuration is by fetching the appropriate
@@ -491,18 +497,49 @@
   \end{tabular}
   \end{center}
 
+  \noindent Recall our definition of @{term fetch} (shown in
+  \eqref{fetch}) with the default value for the @{text 0}-state. In
+  case a Turing program takes according to the usual textbook
+  definition \cite{Boolos87} less than @{text n} steps before it
+  halts, then in our setting the @{term steps}-evaluation does not
+  actually halt, but rather transitions to the @{text 0}-state (the
+  final state) and remains there performing @{text Nop}-actions until
+  @{text n} is reached.
+  
+  \begin{figure}[t]
+  \begin{center}
+  \begin{tabular}{@ {}p{3.6cm}@ {\hspace{4mm}}p{3.6cm}@ {\hspace{4mm}}p{3.6cm}@ {}}
+  @{thm (lhs) tcopy_init_def} @{text "\<equiv>"} &
+  @{thm (lhs) tcopy_loop_def} @{text "\<equiv>"} &
+  @{thm (lhs) tcopy_end_def} @{text "\<equiv>"}\\
+  @{thm (rhs) tcopy_init_def} &
+  @{thm (rhs) tcopy_loop_def} &
+  @{thm (rhs) tcopy_end_def}
+  \end{tabular}
+  \end{center}
+  \caption{Copy machine}\label{copy}
+  \end{figure}
+
+  Before we can prove the undecidability of the halting problem for
+  Turing machines, we need to analyse two concrete Turing machine
+  programs and establish that they are correct, that is they are
+  ``doing what they are supposed to be doing''.  This is usually left
+  out in the informal computability literature, for example
+  \cite{Boolos87}.  One program we prove correct is the @{term dither}
+  program shown in \eqref{dither} and the other program @{term
+  "tcopy"} is defined as
+
+  \begin{center}
+  \begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {}}
+  @{thm (lhs) tcopy_def} & @{text "\<equiv>"} & @{thm (rhs) tcopy_def}
+  \end{tabular}
+  \end{center}
+
   \noindent
-  Recall our definition of @{term fetch} (shown in \ref{fetch}) with the default value for
-  the @{text 0}-state. In case a Turing program takes in \cite{Boolos87} less 
-  then @{text n} steps before it halts, then in our setting the @{term steps}-evaluation
-  does not actually halt, but rather transitions to the @{text 0}-state and 
-  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 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
+  whose three components are given in Figure~\ref{copy}.
+  To prove the correctness, we 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}
   @{thm Hoare_halt_def}
@@ -515,22 +552,10 @@
   In the following we will consider the following Turing machine program
   that makes a copies a value on the tape.
 
-  \begin{figure}
-  \begin{center}
-  \begin{tabular}{@ {}p{3.6cm}@ {\hspace{4mm}}p{3.6cm}@ {\hspace{4mm}}p{3.6cm}@ {}}
-  @{thm tcopy_init_def} &
-  @{thm tcopy_loop_def} &
-  @{thm tcopy_end_def}
-  \end{tabular}
-  \end{center}
-  \end{figure}
+ 
 
 
-  \begin{center}
-  \begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}p{6.9cm}@ {}}
-  @{thm (lhs) tcopy_def} & @{text "\<equiv>"} & @{thm (rhs) tcopy_def}
-  \end{tabular}
-  \end{center}
+  
 
 
   assertion holds for all tapes
@@ -594,7 +619,7 @@
   \end{center}
 
   \noindent
-  The second opcode @{term "Goto 0"} in this programm means we 
+  The second opcode @{term "Goto 0"} in this program means we 
   jump back to the first opcode, namely @{text "Dec R o"}.
   The \emph{memory} $m$ of an abacus machine holding the values
   of the registers is represented as a list of natural numbers.