--- a/Paper/Paper.thy	Wed Jan 30 09:33:06 2013 +0000
+++ b/Paper/Paper.thy	Wed Jan 30 23:00:09 2013 +0000
@@ -723,7 +723,7 @@
   ``doing what they are supposed to be doing''.  Such correctness proofs are usually left
   out in the informal literature, for example \cite{Boolos87}.  The first program 
   we need to prove correct is the @{term dither} program shown in \eqref{dither} 
-  and the other program is @{term "tcopy"} defined as
+  and the second program is @{term "tcopy"} defined as
 
   \begin{equation}
   \mbox{\begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {}}
@@ -732,18 +732,18 @@
   \end{equation}
 
   \noindent
-  whose three components are given in Figure~\ref{copy}. We introduce
-  the notion of total correctness defined in terms of
-  \emph{Hoare-triples}, written @{term "{P} p {Q}"} (this notion is
-  very similar to \emph{realisability} in \cite{AspertiRicciotti12}).
-  The Hoare-triples implement the idea that a program @{term p}
-  started in state @{term "1::nat"} with a tape satisfying @{term P}
-  will after some @{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>"} implementing 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}. For our
+  correctness proofs, we introduce the notion of total correctness
+  defined in terms of \emph{Hoare-triples}, written @{term "{P} p
+  {Q}"}.  They implement the idea that a program @{term
+  p} started in state @{term "1::nat"} with a tape satisfying @{term
+  P} will after some @{text n} steps halt (have transitioned into the
+  halting state) with a tape satisfying @{term Q}. This idea is very
+  similar to \emph{realisability} in \cite{AspertiRicciotti12}. We
+  also have \emph{Hoare-pairs} of the form @{term "{P} p \<up>"}
+  implementing 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@ {}}
@@ -765,7 +765,7 @@
   \end{center}
   
   \noindent
-  For our Hoare-triples we can easily prove the following consequence rule
+  For our Hoare-triples we can easily prove the following Hoare-consequence rule
 
   \begin{equation}
   @{thm[mode=Rule] Hoare_consequence}
@@ -784,10 +784,10 @@
   example, completely separately from @{term "tcopy_loop"} and @{term
   "tcopy_end"}.
 
-  It is realatively straightforward to prove that the small Turing program 
+  It is realatively straightforward to prove that the Turing program 
   @{term "dither"} shown in \eqref{dither} is correct. This program
   should be the ``identity'' when started with a standard tape representing 
-  @{text "1"} but loop when started with @{text 0} instead, as pictured 
+  @{text "1"} but loops when started with @{text 0} instead, as pictured 
   below.
 
 
@@ -851,7 +851,7 @@
   \end{center}
 
   \noindent
-  The first is by a simple calculation. The second is by induction on the
+  The first is by a simple calculation. The second is by an induction on the
   number of steps we can perform starting from the input tape.
 
   The program @{term tcopy} defined in \eqref{tcopy} has 15 states;
@@ -878,18 +878,20 @@
 
   \noindent
   The first corresponds to the usual Hoare-rule for composition of two
-  terminating programs. The second rule is for cases where the first program
-  terminates generating a tape for which the second program loops.
-  The side-condition about @{thm (prem 3) HR2} is needed in both rules
-  in order to ensure that the redirection of the halting and initial
-  state in @{term "p\<^isub>1"} and @{term "p\<^isub>2"} match up correctly.
+  terminating programs. The second rule gives the conditions for when
+  the first program terminates generating a tape for which the second
+  program loops.  The side-conditions about @{thm (prem 3) HR2} are
+  needed in order to ensure that the redirection of the halting and
+  initial state in @{term "p\<^isub>1"} and @{term "p\<^isub>2"} match up correctly.
 
-  The Hoare-rules above allow us to prove the correctness of @{term tcopy}
-  by considering the correctness of the components @{term "tcopy_begin"}, @{term "tcopy_loop"} 
-  and @{term "tcopy_end"} in isolation. We will show the details for 
-  the program @{term "tcopy_begin"}. Given the invariants @{term "inv_begin0"},\ldots, @{term "inv_begin4"} 
-  shown in Figure~\ref{invbegin},
-  we define the following invariant for @{term "tcopy_begin"}.
+  The Hoare-rules allow us to prove the correctness of @{term
+  tcopy} by considering the correctness of the components @{term
+  "tcopy_begin"}, @{term "tcopy_loop"} and @{term "tcopy_end"} in
+  isolation. We will show the details for the program @{term
+  "tcopy_begin"}. Given the invariants @{term "inv_begin0"},\ldots,
+  @{term "inv_begin4"} shown in Figure~\ref{invbegin} corresponding to 
+  each state of @{term tcopy_begin}, we define the
+  following invariant for the whole program:
 
   \begin{figure}
   \begin{center}
@@ -922,10 +924,10 @@
   \end{center}
 
   \noindent
-  This definition depends on @{term n}, which represents the number
-  of @{term Oc}s on the tape. It is not hard (26 lines of automated proof script)
-  to show that for @{term "n > (0::nat)"} this invariant is preserved under @{term step} and @{term steps}.
-  
+  This invariant depends on @{term n} representing the number of
+  @{term Oc}s on the tape. It is not hard (26 lines of automated proof
+  script) to show that for @{term "n > (0::nat)"} this invariant is
+  preserved under computation rules @{term step} and @{term steps}.
 
   measure for the copying TM, which we however omit.
 

Binary file paper.pdf has changed

--- a/thys/uncomputable.thy	Wed Jan 30 09:33:06 2013 +0000
+++ b/thys/uncomputable.thy	Wed Jan 30 23:00:09 2013 +0000
@@ -104,6 +104,9 @@
 apply(simp_all add: assms)
 done
 
+lemma begin_partial_correctness:
+  assumes "\<exists>stp. steps0 cf tcopy_begin stp = (0, l, r)"
+
 fun measure_begin_state :: "config \<Rightarrow> nat"
   where
   "measure_begin_state (s, l, r) = (if s = 0 then 0 else 5 - s)"