# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1360059098 0
# Node ID db518aba152a31adf08211e604d9685f08ddcd78
# Parent  af44c8b2e57f137b08907edd5702f2e57b1e8e7b
updated

diff -r af44c8b2e57f -r db518aba152a Paper/Paper.thy
--- a/Paper/Paper.thy	Tue Feb 05 09:36:21 2013 +0000
+++ b/Paper/Paper.thy	Tue Feb 05 10:11:38 2013 +0000
@@ -1141,14 +1141,13 @@
   programs. Abacus machines operate over a set of registers $R_0$,
   $R_1$, \ldots{} each being able to hold an arbitrary large natural
   number.  We use natural numbers to refer to registers; we also use a natural number
-  to represent a program counter and jumping ``addresses''. An abacus 
+  to represent a program counter and to represent jumping ``addresses''. An abacus 
   program is a list of \emph{instructions} defined by the datatype:
 
   \begin{center}
   \begin{tabular}{rcl@ {\hspace{10mm}}l}
   @{text "i"} & $::=$  & @{term "Inc R\<iota>"} & increment register $R$ by one\\
-  & $\mid$ & @{term "Dec R\<iota> i"} & if content of $R$ is non-zero,\\
-  & & & then decrement it by one\\
+  & $\mid$ & @{term "Dec R\<iota> i"} & if content of $R$ is non-zero, then decrement it by one\\
   & & & otherwise jump to instruction $i$\\
   & $\mid$ & @{term "Goto i"} & jump to instruction $i$
   \end{tabular}
@@ -1165,13 +1164,13 @@
   \noindent
   Running such a program means we start with the first instruction
   then execute one instructions after the other, unless there is a jump.  For
-  example the second instruction the jump @{term "Goto 0"} in @{term clear} means
-  we jump back to the first instruction closing the loop.  Like with our
+  example the second instruction @{term "Goto 0"} in @{term clear} means
+  we jump back to the first instruction thereby closing the loop.  Like with our
   Turing machines, we fetch instructions from an abacus program such
   that a jump out of ``range'' behaves like a @{term "Nop"}-action. In
-  this way it is easy to define a function @{term steps} that
+  this way it is again easy to define a function @{term steps} that
   executes @{term n} instructions of an abacus program. A \emph{configuration}
-  of an abacus machine is the program counter together with a snapshot of 
+  of an abacus machine is the current program counter together with a snapshot of 
   all registers.
   By convention
   the value calculated by an abacus program is stored in the
@@ -1179,9 +1178,9 @@
   
   The main point of abacus programs is to be able to translate them to 
   Turing machine programs. Registers and their content are represented by
-  standard tapes.
-  Because of the jumps in abacus programs, it
-  seems difficult to build Turing machine programs using @{text "\<oplus>"}.
+  standard tapes. Because of the jumps in abacus programs, it
+  seems difficult to build a Turing machine programs out of components 
+  using our @{text "\<oplus>"}-operation.
   To overcome this difficulty, we calculate a \emph{layout} as follows
 
   \begin{center}
@@ -1251,9 +1250,9 @@
   as the abacus program. For this we have to show that for each
   configuration of an abacus machine the @{term step}-function
   is simulated by zero or more steps in our constructed Turing
-  machine. This leads to a rather large ``monolithic'' overall
-  correctness proof that on the conceptual level is difficult to 
-  break down into smaller components. 
+  machine. This leads to a rather large ``monolithic'' 
+  correctness proof (4600 loc and 380 sublemmas) that on the conceptual 
+  level is difficult to break down into smaller components. 
   
   %We were able to simplify the proof somewhat
 *}
diff -r af44c8b2e57f -r db518aba152a paper.pdf
Binary file paper.pdf has changed