--- a/Paper/Paper.thy	Tue Jan 22 14:46:02 2013 +0000
+++ b/Paper/Paper.thy	Wed Jan 23 08:01:35 2013 +0100
@@ -1,6 +1,6 @@
 (*<*)
 theory Paper
-imports "../thys/recursive"
+imports "../thys/uncomputable" "~~/src/HOL/Library/LaTeXsugar"
 begin
 
 (*
@@ -21,6 +21,7 @@
   W0 ("W\<^bsub>\<^raw:\hspace{-2pt}>Bk\<^esub>") and
   W1 ("W\<^bsub>\<^raw:\hspace{-2pt}>Oc\<^esub>") and
   update2 ("update") and
+  tm_wf0 ("wf") and
 (*  abc_lm_v ("lookup") and
   abc_lm_s ("set") and*)
   haltP ("stdhalt") and 
@@ -90,7 +91,7 @@
 of register machines) and recursive functions. To see the difficulties
 involved with this work, one has to understand that Turing machine
 programs can be completely \emph{unstructured}, behaving 
-similar Basic programs involving the infamous goto \cite{Dijkstra68}. This precludes in the
+similar to Basic programs involving the infamous goto \cite{Dijkstra68}. This precludes in the
 general case a compositional Hoare-style reasoning about Turing
 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 
@@ -309,14 +310,14 @@
   %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 by \cite{AspertiRicciotti12} 
+  We followed the choice made in \cite{AspertiRicciotti12} 
   representing a state by a natural number and the states of a Turing
   machine by the initial segment of natural numbers starting from @{text 0}.
   In doing so we can compose two Turing machine by
   shifting the states of one by an appropriate amount to a higher
   segment and adjusting some ``next states'' in the other. {\it composition here?}
 
-  An \emph{instruction} @{term i} of a Turing machine is a pair consisting of 
+  An \emph{instruction} of a Turing machine is a pair consisting of 
   an action and a natural number (the next state). A \emph{program} @{term p} of a Turing
   machine is then a list of such pairs. Using as an example the following Turing machine
   program, which consists of four instructions
@@ -398,13 +399,12 @@
   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 tstep}
+  This single step of execution is defined as the function @{term step}
 
   \begin{center}
-  \begin{tabular}{l}
-  @{text "step (s, (l, r)) p"} @{text "\<equiv>"}\\
-  \hspace{10mm}@{text "let (a, s) = fetch p s (read r)"}\\
-  \hspace{10mm}@{text "in (s', update (l, r) a)"}
+  \begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}l}
+  @{text "step (s, (l, r)) p"} & @{text "\<equiv>"} & @{text "let (a, s') = fetch p s (read r)"}\\
+  & & @{text "in (s', update (l, r) a)"}
   \end{tabular}
   \end{center}
 
@@ -540,6 +540,20 @@
   halting problem
 *}
 
+text {*
+  \begin{center}
+  \begin{tabular}{@ {}p{3cm}p{3cm}@ {}}
+  @{thm[mode=Rule] 
+  Hoare_plus_halt[where ?P1.0="P\<^isub>1" and ?P2.0="P\<^isub>2" and ?Q1.0="Q\<^isub>1" and ?Q2.0="Q\<^isub>2" and ?A="p\<^isub>1" and B="p\<^isub>2"]}
+  &
+  @{thm[mode=Rule] 
+  Hoare_plus_unhalt[where ?P1.0="P\<^isub>1" and ?P2.0="P\<^isub>2" and ?Q1.0="Q\<^isub>1" and ?A="p\<^isub>1" and B="p\<^isub>2"]}
+  \end{tabular}
+  \end{center}
+
+
+*}
+
 section {* Abacus Machines *}
 
 text {*