--- a/Paper/Paper.thy	Thu Jan 24 15:04:11 2013 +0100
+++ b/Paper/Paper.thy	Thu Jan 24 17:14:39 2013 +0100
@@ -7,7 +7,6 @@
 hide_const (open) s 
 *)
 
-
 hide_const (open) Divides.adjust
 
 abbreviation
@@ -524,10 +523,10 @@
 
   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
+  programs and establish that they are correct, that means they are
   ``doing what they are supposed to be doing''.  This is usually left
   out in the informal literature, for example \cite{Boolos87}.  One program 
-  we prove correct is the @{term dither} program shown in \eqref{dither} 
+  we need to prove correct is the @{term dither} program shown in \eqref{dither} 
   and the other program @{term "tcopy"} is defined as
 
   \begin{center}
@@ -537,28 +536,58 @@
   \end{center}
 
   \noindent
-  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
+  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
 
   \begin{center}
-  @{thm Hoare_halt_def}
+  \begin{tabular}{@ {}c@ {\hspace{4mm}}c@ {}}
+  \begin{tabular}[t]{@ {}l@ {}}
+  @{thm (lhs) Hoare_halt_def} @{text "\<equiv>"}\\
+  \hspace{5mm}@{text "\<forall>"} @{term "(l, r)"}.\\
+  \hspace{7mm}if @{term "P (l, r)"} holds then\\
+  \hspace{7mm}@{text "\<exists>"} @{term n}. such that\\
+  \hspace{7mm}@{text "is_final (steps (1, (l, r)) p n)"} \hspace{1mm}@{text "\<and>"}\\
+  \hspace{7mm}@{text "Q holds_for (steps (1, (l, r)) p n)"}
+  \end{tabular} &
+  \begin{tabular}[t]{@ {}l@ {}}
+  @{thm (lhs) Hoare_unhalt_def} @{text "\<equiv>"}\\
+  \hspace{5mm}@{text "\<forall>"} @{term "(l, r)"}.\\ 
+  \hspace{7mm}if @{term "P (l, r)"} holds then\\
+  \hspace{7mm}@{text "\<forall>"} @{term n}. @{text "\<not> is_final (steps (1, (l, r)) p n)"}
+  \end{tabular}
+  \end{tabular}
+  \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.
+
+  It is rather straightforward to prove that the Turing program 
+  @{term "dither"} satisfies the following correctness properties
+
+  \begin{center}
+  \begin{tabular}{l}
+  @{thm dither_halts}\\
+  @{thm dither_loops}
+  \end{tabular}
   \end{center}
 
-  A \emph{Hoare-pair} for a non-terminating Turing machine program is defined 
-  as
-
-  \begin{center}
-  @{thm Hoare_unhalt_def}
-  \end{center}
-
-
+  \noindet
+  {\it unfold} The first states that on a tape @{term "(Bk \<up> n,  [Oc, Oc])"}
+  halts in tree steps leaving the tape unchanged. In the other states
+  that @{term dither} started with tape @{term "(Bk \<up> n,  [Oc, Oc])"} loops.
+  
 
 
   In the following we will consider the following Turing machine program

Binary file paper.pdf has changed

--- a/thys/uncomputable.thy	Thu Jan 24 15:04:11 2013 +0100
+++ b/thys/uncomputable.thy	Thu Jan 24 17:14:39 2013 +0100
@@ -1070,10 +1070,10 @@
 
 (* invariants of dither *)
 abbreviation
-  "dither_halt_inv \<equiv> \<lambda>(l, r). (\<exists>nd. l = Bk \<up> nd) \<and> r = [Oc, Oc]"
+  "dither_halt_inv \<equiv> \<lambda>(l, r). (\<exists>n. l = Bk \<up> n) \<and> r = [Oc, Oc]"
 
 abbreviation
-  "dither_unhalt_inv \<equiv> \<lambda>(l, r). (\<exists>nd. l = Bk \<up> nd) \<and> r = [Oc]"
+  "dither_unhalt_inv \<equiv> \<lambda>(l, r). (\<exists>n. l = Bk \<up> n) \<and> r = [Oc]"
 
 lemma dither_unhalt_state: 
   "(steps0 (1, Bk \<up> m, [Oc]) dither stp = (1, Bk \<up> m, [Oc])) \<or>