--- a/Paper/Paper.thy	Mon Feb 04 01:47:26 2013 +0000
+++ b/Paper/Paper.thy	Mon Feb 04 11:14:03 2013 +0000
@@ -213,7 +213,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 to
-Basic programs involving the infamous goto \cite{Dijkstra68}. This
+Basic programs containing the infamous goto-statement \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
@@ -1191,32 +1191,25 @@
 section {* Related Work *}
 
 text {*
-  The most closely related work is by Norrish \cite{Norrish11}, and Asperti and 
-  Ricciotti \cite{AspertiRicciotti12}. Norrish bases his approach on 
-  lambda-terms. For this he introduced a clever rewriting technology
-  based on combinators and de-Bruijn indices for
-  rewriting modulo $\beta$-equivalence (to keep it manageable)
+  We have formalised the main results from three chapters in the
+  textbook by Boolos et al \cite{Boolos87}.  Following in the
+  footsteps of another paper \cite{Nipkow98} formalising the results
+  from a textbook, we could have titled our paper ``Boolos et al are
+  (almost) Right''. We have not attempted to formalise everything
+  precisely as Boolos et al present it, but find definitions that make
+  mechanised proofs manageable. We have found a small inconsitency in
+  the usage of definitions of \ldots Our interest in this subject
+  arose from correctness proofs about algorithms where we were unable
+  to formalise argumants about decidability.
 
 
-  
-  Given some input tape @{text "(l\<^isub>i,r\<^isub>i)"}, we can define when a program 
-  @{term p} generates a specific  output tape @{text "(l\<^isub>o,r\<^isub>o)"}
+  The most closely related work is by Norrish \cite{Norrish11}, and
+  Asperti and Ricciotti \cite{AspertiRicciotti12}. Norrish bases his
+  approach on lambda-terms. For this he introduced a clever rewriting
+  technology based on combinators and de-Bruijn indices for rewriting
+  modulo $\beta$-equivalence (to keep it manageable)
 
-  \begin{center}
-  \begin{tabular}{l}
-  @{term "runs p (l\<^isub>i, r\<^isub>i) (l\<^isub>o,r\<^isub>o)"} @{text "\<equiv>"}\\
-  \hspace{6mm}@{text "\<exists>n. nsteps (1, (l\<^isub>i,r\<^isub>i)) p n = (0, (l\<^isub>o,r\<^isub>o))"}
-  \end{tabular}
-  \end{center}
 
-  \noindent
-  where @{text 1} stands for the starting state and @{text 0} for our final state.
-  A program @{text p} with input tape @{term "(l\<^isub>i, r\<^isub>i)"} \emph{halts} iff
-
-  \begin{center}
-  @{term "halts p (l\<^isub>i, r\<^isub>i) \<equiv>
-  \<exists>l\<^isub>o r\<^isub>o. runs p (l\<^isub>i, r\<^isub>i) (l\<^isub>o,r\<^isub>o)"}
-  \end{center}
 
   \noindent
   Later on we need to consider specific Turing machines that 
@@ -1226,21 +1219,6 @@
   that translates lists of natural numbers into tapes. 
 
   
-  \begin{center}
-  \begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}l}
-  %@ { thm (lhs) tape_of_nat_list_def2(1)} & @{text "\<equiv>"} & @ { thm (rhs) tape_of_nat_list_def2(1)}\\
-  %@ { thm (lhs) tape_of_nat_list_def2(2)} & @{text "\<equiv>"} & @ { thm (rhs) tape_of_nat_list_def2(2)}\\
-  %@ { thm (lhs) tape_of_nat_list_def2(3)} & @{text "\<equiv>"} & @ { thm (rhs) tape_of_nat_list_def2(3)}\\
-  \end{tabular}
-  \end{center}
-
-  
- By this we mean
-
-  \begin{center}
-  %@ {thm haltP_def2[where p="p" and n="n", THEN eq_reflection]}
-  \end{center}
-
   \noindent
   This means the Turing machine starts with a tape containg @{text n} @{term Oc}s
   and the head pointing to the first one; the Turing machine
@@ -1255,18 +1233,16 @@
 
   
   Magnus: invariants -- Section 5.4.5 on page 75.
-*}
 
 
-(*
-Questions:
+  There is a tantalising connection with recent work \cite{Jensen13}
+  about verifying X86 assembly code. They observed 
+  It remains to be seen whether their specification logic
+  for assmebly code can make it easier to reason about our Turing
+  programs.
+  
+*}
 
-Can this be done: Ackerman function is not primitive 
-recursive (Nora Szasz)
-
-Tape is represented as two lists (finite - usually infinite tape)?
-
-*)
 
 
 (*<*)

--- a/Paper/document/root.bib	Mon Feb 04 01:47:26 2013 +0000
+++ b/Paper/document/root.bib	Mon Feb 04 11:14:03 2013 +0000
@@ -1,3 +1,23 @@
+@article{Nipkow98,
+  author={T.~Nipkow},
+  title={{W}inskel is (almost) {R}ight: {T}owards a {M}echanized {S}emantics {T}extbook},
+  journal={Formal Aspects of Computing},
+  volume=10,
+  pages={171--186},
+  year=1998
+}
+
+@inproceedings{Jensen13,
+  author    = {J.~Braband Jensen and
+               N.~Benton and
+               A.~Kennedy},
+  title     = {{H}igh-{L}evel {S}eparation {L}ogic for {L}ow-{L}evel {C}ode},
+  booktitle = {Proc.~of the 40th Symposium on Principles
+               of Programming Languages (POPL)},
+  year      = {2013},
+  pages     = {301--314}
+}
+
 @article{UrbanCheneyBerghofer11,
   author = {C.~Urban and J.~Cheney and S.~Berghofer},
   title = {{M}echanizing the {M}etatheory of {LF}},

Binary file paper.pdf has changed