equal
deleted
inserted
replaced
1 (* Title: thys/Abacus.thy |
1 (* Title: thys/Abacus.thy |
2 Author: Jian Xu, Xingyuan Zhang, and Christian Urban |
2 Author: Jian Xu, Xingyuan Zhang, and Christian Urban |
3 *) |
3 *) |
4 |
4 |
5 header {* Alternative Definitions for Translating Abacus Machines to TMs *} |
5 chapter {* Alternative Definitions for Translating Abacus Machines to TMs *} |
6 |
6 |
7 theory Abacus_Defs |
7 theory Abacus_Defs |
8 imports Abacus |
8 imports Abacus |
9 begin |
9 begin |
10 |
10 |
11 abbreviation |
11 abbreviation |
12 "layout \<equiv> layout_of" |
12 "layout \<equiv> layout_of" |
13 |
13 |
14 fun address :: "abc_prog \<Rightarrow> nat \<Rightarrow> nat" |
14 fun address :: "abc_prog \<Rightarrow> nat \<Rightarrow> nat" |
15 where |
15 where |
16 "address p x = (Suc (listsum (take x (layout p)))) " |
16 "address p x = (Suc (sum_list (take x (layout p)))) " |
17 |
17 |
18 abbreviation |
18 abbreviation |
19 "TMGoto \<equiv> [(Nop, 1), (Nop, 1)]" |
19 "TMGoto \<equiv> [(Nop, 1), (Nop, 1)]" |
20 |
20 |
21 abbreviation |
21 abbreviation |