--- a/Paper/Paper.thy	Sun Feb 03 12:24:28 2013 +0000
+++ b/Paper/Paper.thy	Sun Feb 03 13:31:14 2013 +0000
@@ -1,6 +1,6 @@
 (*<*)
 theory Paper
-imports "../thys/uncomputable"
+imports "../thys/abacus"
 begin
 
 (*
@@ -1119,9 +1119,6 @@
   to an contradiction, which means we have to abondon our assumption 
   that there exists a Turing machine @{term H} which can decide 
   whether Turing machines terminate.
-  
-
-
 *}
 
 
@@ -1135,22 +1132,22 @@
   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, but also
-  to refer to \emph{opcodes} of abacus 
-  machines. Obcodes are given by the datatype
+  to refer to \emph{statements} of abacus programs. Statements 
+  are given by the datatype
 
   \begin{center}
-  \begin{tabular}{rcll}
+  \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,\\
   & & & then decrement it by one\\
-  & & & otherwise jump to opcode $o$\\
-  & $\mid$ & @{term "Goto o\<iota>"} & jump to opcode $o$
+  & & & otherwise jump to statement $o$\\
+  & $\mid$ & @{term "Goto o\<iota>"} & jump to statement $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
+  statements. For example the program clearing the register
   $R$ (setting it to 0) can be defined as follows:
 
   \begin{center}

--- a/Paper/ROOT.ML	Sun Feb 03 12:24:28 2013 +0000
+++ b/Paper/ROOT.ML	Sun Feb 03 13:31:14 2013 +0000
@@ -1,8 +1,8 @@
 no_document 
 use_thys ["../thys/turing_basic", 
           "../thys/turing_hoare",
-          "../thys/uncomputable"(*, 
-          "../thys/abacus",
+          "../thys/uncomputable", 
+          "../thys/abacus"(*,
           "../thys/rec_def",
           "../thys/recursive"*)];
 

Binary file paper.pdf has changed

--- a/thys/abacus.thy	Sun Feb 03 12:24:28 2013 +0000
+++ b/thys/abacus.thy	Sun Feb 03 13:31:14 2013 +0000
@@ -3,9 +3,19 @@
 *}
 
 theory abacus
-imports Main turing_basic
+imports uncomputable
 begin
 
+(*
+declare tm_comp.simps [simp add] 
+declare adjust.simps[simp add] 
+declare shift.simps[simp add]
+declare tm_wf.simps[simp add]
+declare step.simps[simp add]
+declare steps.simps[simp add]
+*)
+declare replicate_Suc[simp add]
+
 text {*
   {\em Abacus} instructions:
 *}
@@ -1300,8 +1310,7 @@
    inv_locate_b.simps[simp del]
 
 lemma [intro]: "\<exists>rn. [Bk] = Bk \<up> rn"
-apply(rule_tac x = "Suc 0" in exI, simp)
-done
+by (metis replicate_0 replicate_Suc)
 
 lemma [intro]:  "at_begin_norm (as, am) (q, aaa, []) ires
              \<Longrightarrow> at_begin_norm (as, am) (q, aaa, [Bk]) ires"
@@ -1877,7 +1886,6 @@
      \<Longrightarrow> inv_after_write (as, lm) (y, l, Oc # r) ires"
 apply(auto simp: inv_on_right_moving.simps inv_after_write.simps )
 apply(case_tac mr, auto simp: split: if_splits)
-apply(case_tac [!] mr, simp_all)
 done
       
 lemma [simp]: "inv_on_right_moving (as, lm) (x, l, []) ires\<Longrightarrow>