--- a/Paper/Paper.thy	Mon Feb 04 23:12:17 2013 +0000
+++ b/Paper/Paper.thy	Tue Feb 05 08:57:55 2013 +0000
@@ -83,7 +83,9 @@
   inv_loop0 ("J\<^isub>0") and
   inv_end1 ("K\<^isub>1") and
   inv_end0 ("K\<^isub>0") and
-  measure_begin_step ("M\<^bsub>cbegin\<^esub>")
+  measure_begin_step ("M\<^bsub>cbegin\<^esub>") and
+  layout_of ("layout") and
+  findnth ("find'_nth")
 
  
 lemma inv_begin_print:
@@ -154,8 +156,8 @@
 lemma layout:
   shows "layout_of [] = []"
   and   "layout_of ((Inc R\<iota>)#os) = (2 * R\<iota> + 9)#(layout_of os)"
-  and   "layout_of ((Dec R\<iota> o\<iota>)#os) = (2 * R\<iota> + 16)#(layout_of os)"
-  and   "layout_of ((Goto o\<iota>)#os) = 1#(layout_of os)"
+  and   "layout_of ((Dec R\<iota> i)#os) = (2 * R\<iota> + 16)#(layout_of os)"
+  and   "layout_of ((Goto i)#os) = 1#(layout_of os)"
 by(auto simp add: layout_of.simps length_of.simps)
 
 
@@ -1140,15 +1142,15 @@
   $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 
-  program is a list of \emph{statements} defined by the datatype:
+  program is a list of \emph{instructions} defined by the datatype:
 
   \begin{center}
   \begin{tabular}{rcl@ {\hspace{10mm}}l}
-  @{text "o"} & $::=$  & @{term "Inc R\<iota>"} & increment register $R$ by one\\
-  & $\mid$ & @{term "Dec R\<iota> o\<iota>"} & if content of $R$ is non-zero,\\
+  @{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\\
-  & & & otherwise jump to statement $o$\\
-  & $\mid$ & @{term "Goto o\<iota>"} & jump to statement $o$
+  & & & otherwise jump to instruction $i$\\
+  & $\mid$ & @{term "Goto i"} & jump to instruction $i$
   \end{tabular}
   \end{center}
 
@@ -1157,42 +1159,87 @@
   it to @{term "(0::nat)"}) can be defined as follows:
 
   \begin{center}
-  @{thm clear.simps[where n="R\<iota>" and e="o\<iota>", THEN eq_reflection]}
+  @{thm clear.simps[where n="R\<iota>" and e="i", THEN eq_reflection]}
   \end{center}
 
   \noindent
   Running such a program means we start with the first instruction
-  then execute one statements after the other, unless there is a jump.  For
-  example the second statement the jump @{term "Goto 0"} in @{term clear} means
-  we jump back to the first statement closing the loop.  Like with our
-  Turing machines, we fetch statements from an abacus program such
+  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
+  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
-  executes @{term n} statements of an abacus program.
+  executes @{term n} instructions of an abacus program.
   
   The main point of abacus programs is to be able to translate them to 
-  Turing machine programs. Because of the jumps in abacus programs, it
+  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>"}.
-  To overcome this difficulty we calculate a \emph{layout} as follows
+  To overcome this difficulty, we calculate a \emph{layout} as follows
+
+  \begin{center}
+  \begin{tabular}[t]{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {}}
+  @{thm (lhs) layout(1)} & @{text "\<equiv>"} & @{thm (rhs) layout(1)}\\
+  @{thm (lhs) layout(2)} & @{text "\<equiv>"} & @{thm (rhs) layout(2)}\\
+  @{thm (lhs) layout(3)} & @{text "\<equiv>"} & @{thm (rhs) layout(3)}\\
+  @{thm (lhs) layout(4)} & @{text "\<equiv>"} & @{thm (rhs) layout(4)}\\
+  \end{tabular}
+  \end{center}
+
+  \noindent
+  This gives us a list of natural numbers specifying how many states
+  are needed to translate each abacus instruction. The @{text Goto}
+  instruction is easiest to translate requiring only one state in
+  the corresponding Turing machine:
 
   \begin{center}
-  @{thm layout}
+  @{thm (rhs) tgoto.simps[where n="i"]}
+  \end{center}
+
+  \noindent
+  where @{term "i"} is the corresponding state in the Turing machine program 
+  to jump to. For translating the instruction @{term Inc}
+  one has to remember that the content of the registers are encoded
+  in the Turing machine as standard tape. Therefore the translated Turing machine 
+  needs to first find the number corresponding to the register @{text "R"}. This needs a machine
+  with @{term "(2::nat) * R\<iota>"} states and can be constructed as follows: 
+
+  \begin{center}
+  \begin{tabular}[t]{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {}}
+  @{thm (lhs) findnth.simps(1)} & @{text "\<equiv>"} & @{thm (rhs) findnth.simps(1)}\\
+  @{thm (lhs) findnth.simps(2)} & @{text "\<equiv>"}\\
+  \multicolumn{3}{@ {}l@ {}}{\hspace{8mm}@{thm (rhs) findnth.simps(2)}}\\
+  \end{tabular}
   \end{center}
 
+  \noindent
+  Then we need to increase the ``number'' on the tape by one,
+  and adjust the following registers. By adjusting we only need to 
+  replace the first @{term Oc} of each number by @{term Bk} and the last
+  one from @{term Bk} to @{term Oc}.
+  Finally we need to transition the head of the
+  Turing machine back into the standard position. This requires a Turing machine
+  with 9 states. Similarly for the translation of @{term Dec}, where the 
+  translated Turing machine needs to first check whether the content of the
+  corresponding register is @{text 0}. For this we have a Turing machine program
+  with @{text 16} states. 
+
+  Finally, having a turing machine for each abacus instruction we need
+  to ``stitch'' the Turing machines together into one so that each
+  Turing machine component transitions to next one, just like in
+  are needed to translate each abacus instructionabacus
+  programs. While generating the Turing machine program for an abacus
+  program is not too difficult to formalise, the problem is that it
+  contains @{text Goto}s all over the place. The unfortunate result is
+  are needed to translate each abacus instructionthat we cannot
+  use our Hoare-rules for reasoning about sequentially composed
+  programs. Instead we have to treat the Turing machine as one ``block''
+  and show as invariant that it performs the same operations
+  as the abacus program.
 
 
-  %Running an abacus program means to start 
-  %A \emph{program} of an abacus machine is a list of such
-  %statements. 
-  %The \emph{memory} $m$ of an abacus machine holding the values
-  %of the registers is represented as a list of natural numbers.
-  %We have a lookup function for this memory, written @{term "abc_lm_v m R\<iota>"},
-  %which looks up the content of register $R$; if $R$
-  %is not in this list, then we return 0. Similarly we
-  %have a setting function, written @{term "abc_lm_s m R\<iota> n"}, which
-  %sets the value of $R$ to $n$, and if $R$ was not yet in $m$
-  %it pads it approriately with 0s.
-  %Abacus machine halts when it jumps out of range.
 *}
 
 

Binary file paper.pdf has changed