173
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1 |
(* Title: thys/Abacus.thy
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
2 |
Author: Jian Xu, Xingyuan Zhang, and Christian Urban
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
3 |
*)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
4 |
|
197
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
5 |
header {* Alternative Definitions for Translating Abacus Machines to TMs *}
|
173
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
6 |
|
197
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
7 |
theory Abacus_Defs
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
8 |
imports Abacus
|
47
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
9 |
begin
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
10 |
|
197
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
11 |
abbreviation
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
12 |
"layout \<equiv> layout_of"
|
47
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
13 |
|
197
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
14 |
fun address :: "abc_prog \<Rightarrow> nat \<Rightarrow> nat"
|
47
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
15 |
where
|
197
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
16 |
"address p x = (Suc (listsum (take x (layout p)))) "
|
60
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
17 |
|
197
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
18 |
abbreviation
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
19 |
"TMGoto \<equiv> [(Nop, 1), (Nop, 1)]"
|
60
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
20 |
|
197
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
21 |
abbreviation
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
22 |
"TMInc \<equiv> [(W1, 1), (R, 2), (W1, 3), (R, 2), (W1, 3), (R, 4),
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
23 |
(L, 7), (W0, 5), (R, 6), (W0, 5), (W1, 3), (R, 6),
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
24 |
(L, 8), (L, 7), (R, 9), (L, 7), (R, 10), (W0, 9)]"
|
60
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
25 |
|
197
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
26 |
abbreviation
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
27 |
"TMDec \<equiv> [(W1, 1), (R, 2), (L, 14), (R, 3), (L, 4), (R, 3),
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
28 |
(R, 5), (W0, 4), (R, 6), (W0, 5), (L, 7), (L, 8),
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
29 |
(L, 11), (W0, 7), (W1, 8), (R, 9), (L, 10), (R, 9),
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
30 |
(R, 5), (W0, 10), (L, 12), (L, 11), (R, 13), (L, 11),
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
31 |
(R, 17), (W0, 13), (L, 15), (L, 14), (R, 16), (L, 14),
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
32 |
(R, 0), (W0, 16)]"
|
47
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
33 |
|
197
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
34 |
abbreviation
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
35 |
"TMFindnth \<equiv> findnth"
|
60
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
36 |
|
197
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
37 |
fun compile_goto :: "nat \<Rightarrow> instr list"
|
60
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
38 |
where
|
197
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
39 |
"compile_goto s = shift TMGoto (s - 1)"
|
60
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
40 |
|
197
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
41 |
fun compile_inc :: "nat \<Rightarrow> nat \<Rightarrow> instr list"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
42 |
where
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
43 |
"compile_inc s n = (shift (TMFindnth n) (s - 1)) @ (shift (shift TMInc (2 * n)) (s - 1))"
|
60
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
44 |
|
197
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
45 |
fun compile_dec :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> instr list"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
46 |
where
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
47 |
"compile_dec s n e = (shift (TMFindnth n) (s - 1)) @ (adjust (shift (shift TMDec (2 * n)) (s - 1)) e)"
|
60
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
48 |
|
197
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
49 |
fun compile :: "abc_prog \<Rightarrow> nat \<Rightarrow> abc_inst \<Rightarrow> instr list"
|
60
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
50 |
where
|
197
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
51 |
"compile ap s (Inc n) = compile_inc s n"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
52 |
| "compile ap s (Dec n e) = compile_dec s n (address ap e)"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
53 |
| "compile ap s (Goto e) = compile_goto (address ap e)"
|
60
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
54 |
|
197
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
55 |
lemma
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
56 |
"compile ap s i = ci (layout ap) s i"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
57 |
apply(cases i)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
58 |
apply(simp add: ci.simps shift.simps start_of.simps tinc_b_def)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
59 |
apply(simp add: ci.simps shift.simps start_of.simps tdec_b_def)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
60 |
apply(simp add: ci.simps shift.simps start_of.simps)
|
60
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
61 |
done
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
62 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
63 |
|
197
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
64 |
end |