diff -r d3400d212091 -r a1e8b94d0b93 Paper.thy
--- a/Paper.thy	Thu Jan 10 11:28:26 2013 +0000
+++ b/Paper.thy	Thu Jan 10 12:30:27 2013 +0000
@@ -4,7 +4,6 @@
 begin
 
 hide_const (open) s 
-hide_const (open) R
 
 abbreviation 
   "update p a == new_tape a p"
@@ -55,6 +54,8 @@
   W1 ("W\<^bsub>\<^raw:\hspace{-2pt}>Oc\<^esub>") and
   tstep ("step") and
   steps ("nsteps") and
+  abc_lm_v ("lookup") and
+  abc_lm_s ("set") and
   DUMMY  ("\<^raw:\mbox{$\_$}>")
 
 declare [[show_question_marks = false]]
@@ -392,18 +393,40 @@
   programs for Turing machines. Abacus machines operate
   over an unlimited number 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 and also
-  to \emph{opcodes} of abacus machines. Obcodes are
-  defined as the datatype
+  We use natural numbers to refer to registers, but also
+  to refer to \emph{opcodes} of abacus 
+  machines. Obcodes are given by the datatype
 
   \begin{center}
   \begin{tabular}{rcll}
-  @{text "o"} & $::=$  & @{term "Inc R"} & increment register $R$ by one\\
-  & $\mid$ & @{term "Dec R n"} & if content of $R$ is non-zero, then decrement it by one\\
+  @{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,\\
+  & & & then decrement it by one\\
   & & & otherwise jump to opcode $o$\\
-  & $\mid$ & @{term "Goto n"} & jump to opcode $o$
+  & $\mid$ & @{term "Goto o\<iota>"} & jump to opcode $o$
   \end{tabular}
   \end{center}
+
+  \noindent
+  A \emph{program} of an abacus machine is a list of such
+  obcodes. For example the program clearing the register
+  $R$ (setting it to 0) can be defined as follows:
+
+  \begin{center}
+  @{thm clear.simps[where n="R\<iota>" and e="o\<iota>", THEN eq_reflection]}
+  \end{center}
+
+  \noindent
+  The second opcode @{term "Goto 0"} in this programm means we 
+  jump back to the first opcode, namely @{text "Dec R o"}.
+  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.
 *}