--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/thys/Abacus_Defs.thy	Tue Feb 26 12:47:03 2013 +0000
@@ -0,0 +1,64 @@
+(* Title: thys/Abacus.thy
+   Author: Jian Xu, Xingyuan Zhang, and Christian Urban
+*)
+
+header {* Alternative Definitions for Translating Abacus Machines to TMs *}
+
+theory Abacus_Defs
+imports Abacus
+begin
+
+abbreviation
+  "layout \<equiv> layout_of"
+
+fun address :: "abc_prog \<Rightarrow> nat \<Rightarrow> nat"
+  where
+  "address p x = (Suc (listsum (take x (layout p)))) "
+
+abbreviation
+  "TMGoto \<equiv> [(Nop, 1), (Nop, 1)]"
+
+abbreviation 
+  "TMInc \<equiv> [(W1, 1), (R, 2), (W1, 3), (R, 2), (W1, 3), (R, 4), 
+            (L, 7), (W0, 5), (R, 6), (W0, 5), (W1, 3), (R, 6),
+            (L, 8), (L, 7), (R, 9), (L, 7), (R, 10), (W0, 9)]"
+
+abbreviation
+  "TMDec \<equiv> [(W1, 1), (R, 2), (L, 14), (R, 3), (L, 4), (R, 3),
+             (R, 5), (W0, 4), (R, 6), (W0, 5), (L, 7), (L, 8),
+             (L, 11), (W0, 7), (W1, 8), (R, 9), (L, 10), (R, 9),
+             (R, 5), (W0, 10), (L, 12), (L, 11), (R, 13), (L, 11),
+             (R, 17), (W0, 13), (L, 15), (L, 14), (R, 16), (L, 14),
+             (R, 0), (W0, 16)]"
+
+abbreviation
+  "TMFindnth \<equiv> findnth"
+
+fun compile_goto :: "nat \<Rightarrow> instr list" 
+  where
+  "compile_goto s = shift TMGoto (s - 1)"
+
+fun compile_inc :: "nat \<Rightarrow> nat \<Rightarrow> instr list"
+  where
+  "compile_inc s n = (shift (TMFindnth n) (s - 1)) @ (shift (shift TMInc (2 * n)) (s - 1))"
+
+fun compile_dec :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> instr list"
+  where
+  "compile_dec s n e = (shift (TMFindnth n) (s - 1)) @ (adjust (shift (shift TMDec (2 * n)) (s - 1)) e)"
+
+fun compile :: "abc_prog \<Rightarrow> nat \<Rightarrow> abc_inst \<Rightarrow> instr list"
+  where
+  "compile ap s (Inc n) = compile_inc s n"
+| "compile ap s (Dec n e) = compile_dec s n (address ap e)"
+| "compile ap s (Goto e) = compile_goto (address ap e)"
+
+lemma
+  "compile ap s i = ci (layout ap) s i"
+apply(cases i)
+apply(simp add: ci.simps shift.simps start_of.simps tinc_b_def)
+apply(simp add: ci.simps shift.simps start_of.simps tdec_b_def)
+apply(simp add: ci.simps shift.simps start_of.simps)
+done
+
+
+end
\ No newline at end of file