--- a/Paper/Paper.thy	Sun Feb 03 13:31:14 2013 +0000
+++ b/Paper/Paper.thy	Mon Feb 04 01:17:09 2013 +0000
@@ -1117,7 +1117,7 @@
   This time the Hoare-triple states that @{term tcontra} terminates 
   with the ``output'' @{term "<(1::nat)>"}. In both case we come
   to an contradiction, which means we have to abondon our assumption 
-  that there exists a Turing machine @{term H} which can decide 
+  that there exists a Turing machine @{term H} which can in general decide 
   whether Turing machines terminate.
 *}
 
@@ -1126,14 +1126,13 @@
 
 text {*
   \noindent
-  Boolos et al \cite{Boolos87} use abacus machines as a 
-  stepping stone for making it less laborious to write
-  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, but also
-  to refer to \emph{statements} of abacus programs. Statements 
-  are given by the datatype
+  Boolos et al \cite{Boolos87} use abacus machines as a stepping stone
+  for making it less laborious to write Turing machine
+  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, but also to
+  refer to \emph{statements} of abacus programs. Statements are given
+  by the datatype
 
   \begin{center}
   \begin{tabular}{rcl@ {\hspace{10mm}}l}
@@ -1148,15 +1147,15 @@
   \noindent
   A \emph{program} of an abacus machine is a list of such
   statements. For example the program clearing the register
-  $R$ (setting it to 0) can be defined as follows:
+  $R$ (setting 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="o\<iota>", THEN eq_reflection]}
   \end{center}
 
   \noindent
   The second opcode @{term "Goto 0"} in this program means we 
-  jump back to the first opcode, namely @{text "Dec R o"}.
+  jump back to the first statement, 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>"},

Binary file paper.pdf has changed

--- a/thys/abacus.thy	Sun Feb 03 13:31:14 2013 +0000
+++ b/thys/abacus.thy	Mon Feb 04 01:17:09 2013 +0000
@@ -6,14 +6,6 @@
 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 {*
@@ -1731,23 +1723,6 @@
 lemma wf_inc_le[intro]: "wf inc_LE"
 by(auto intro:wf_inv_image simp: inc_LE_def lex_triple_def lex_pair_def)
 
-lemma numeral_5_eq_5: "5 = Suc (Suc (Suc (Suc (Suc 0))))"
-by arith
-
-lemma numeral_6_eq_6: "6 = Suc (Suc (Suc (Suc (Suc 1))))"
-by arith
-
-lemma numeral_7_eq_7: "7 = Suc (Suc (Suc (Suc (Suc 2))))"
-by arith
-
-lemma numeral_8_eq_8: "8 = Suc (Suc (Suc (Suc (Suc 3))))"
-by arith
-
-lemma numeral_9_eq_9: "9 = Suc (Suc (Suc (Suc (Suc (Suc 3)))))"
-by arith
-
-lemma numeral_10_eq_10: "10 = Suc (Suc (Suc (Suc (Suc (Suc (Suc 3))))))"
-by arith
 
 lemma inv_locate_b_2_after_write[simp]: 
       "inv_locate_b (as, am) (n, aaa, Bk # xs) ires
@@ -2153,9 +2128,8 @@
       apply(simp add:Q)
       apply(simp add: inc_inv.simps)
       apply(case_tac c, case_tac [2] aa)
-      apply(auto simp: Let_def step.simps tinc_b_def numeral_2_eq_2 numeral_3_eq_3  split: if_splits)
-      apply(simp_all add: inc_inv.simps inc_LE_def lex_triple_def lex_pair_def inc_measure_def numeral_5_eq_5
-                          numeral_6_eq_6 numeral_7_eq_7 numeral_8_eq_8 numeral_9_eq_9)         
+      apply(auto simp: Let_def step.simps tinc_b_def numeral  split: if_splits)
+      apply(simp_all add: inc_inv.simps inc_LE_def lex_triple_def lex_pair_def inc_measure_def numeral)         
       done
   qed
 qed
@@ -3682,7 +3656,7 @@
         apply(simp_all split: if_splits)
         using fetch layout dec_suc
         apply(auto simp: step.simps P dec_inv_2.simps Let_def abc_dec_2_LE_def lex_triple_def lex_pair_def lex_square_def
-                         fix_add numeral_3_eq_3) 
+                         fix_add numeral) 
         done
     qed
   qed

--- a/thys/uncomputable.thy	Sun Feb 03 13:31:14 2013 +0000
+++ b/thys/uncomputable.thy	Mon Feb 04 01:17:09 2013 +0000
@@ -15,7 +15,12 @@
   and "3 = Suc 2"
   and "4 = Suc 3" 
   and "5 = Suc 4" 
-  and "6 = Suc 5" by arith+
+  and "6 = Suc 5" 
+  and "7 = Suc 6"
+  and "8 = Suc 7" 
+  and "9 = Suc 8" 
+  and "10 = Suc 9" 
+  by arith+
 
 text {*
   The {\em Copying} TM, which duplicates its input.