# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1360012303 0
# Node ID 653426ed4b38676f6bd38ef80bd54c1ed8415c84
# Parent  120091653998dd66fddb2868c833e931f27dcca2
started with abacus section

diff -r 120091653998 -r 653426ed4b38 Paper/Paper.thy
--- a/Paper/Paper.thy	Mon Feb 04 11:14:03 2013 +0000
+++ b/Paper/Paper.thy	Mon Feb 04 21:11:43 2013 +0000
@@ -151,6 +151,14 @@
 using assms by auto
 
 
+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)"
+by(auto simp add: layout_of.simps length_of.simps)
+
+
 (*>*)
 
 section {* Introduction *}
@@ -1162,6 +1170,15 @@
   this way it is easy to define a function @{term steps} that
   executes @{term n} statements 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
+  seems difficult to build Turing machine programs using @{text "\<oplus>"}.
+  To overcome this difficulty we calculate a \emph{layout} as follows
+
+  \begin{center}
+  @{thm layout}
+  \end{center}
+
 
 
   %Running an abacus program means to start 
diff -r 120091653998 -r 653426ed4b38 paper.pdf
Binary file paper.pdf has changed
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