diff -r 120091653998 -r 653426ed4b38 thys/abacus.thy
--- a/thys/abacus.thy	Mon Feb 04 11:14:03 2013 +0000
+++ b/thys/abacus.thy	Mon Feb 04 21:11:43 2013 +0000
@@ -6,6 +6,14 @@
 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 {*
@@ -1723,6 +1731,23 @@
 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
@@ -2128,8 +2153,9 @@
       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  split: if_splits)
-      apply(simp_all add: inc_inv.simps inc_LE_def lex_triple_def lex_pair_def inc_measure_def numeral)         
+      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)         
       done
   qed
 qed
@@ -3656,7 +3682,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) 
+                         fix_add numeral_3_eq_3) 
         done
     qed
   qed