equal
deleted
inserted
replaced
192 where |
192 where |
193 "tape_of_nat_list [] = []" | |
193 "tape_of_nat_list [] = []" | |
194 "tape_of_nat_list [n] = Oc\<up>(Suc n)" | |
194 "tape_of_nat_list [n] = Oc\<up>(Suc n)" | |
195 "tape_of_nat_list (n#ns) = Oc\<up>(Suc n) @ Bk # (tape_of_nat_list ns)" |
195 "tape_of_nat_list (n#ns) = Oc\<up>(Suc n) @ Bk # (tape_of_nat_list ns)" |
196 |
196 |
|
197 fun tape_of_nat_pair :: "nat \<times> nat \<Rightarrow> cell list" |
|
198 where |
|
199 "tape_of_nat_pair (n, m) = Oc\<up>(Suc n) @ [Bk] @ Oc\<up>(Suc m)" |
|
200 |
|
201 |
197 defs (overloaded) |
202 defs (overloaded) |
198 tape_of_nl_abv: "<am> \<equiv> tape_of_nat_list am" |
203 tape_of_nl_abv: "<ns> \<equiv> tape_of_nat_list ns" |
199 tape_of_nat_abv : "<(n::nat)> \<equiv> Oc\<up>(Suc n)" |
204 tape_of_nat_abv: "<(n::nat)> \<equiv> Oc\<up>(Suc n)" |
200 |
205 tape_of_nat_pair: "<p> \<equiv> tape_of_nat_pair p" |
201 definition tinres :: "cell list \<Rightarrow> cell list \<Rightarrow> bool" |
|
202 where |
|
203 "tinres xs ys = (\<exists>n. xs = ys @ Bk \<up> n \<or> ys = xs @ Bk \<up> n)" |
|
204 |
206 |
205 fun |
207 fun |
206 shift :: "instr list \<Rightarrow> nat \<Rightarrow> instr list" |
208 shift :: "instr list \<Rightarrow> nat \<Rightarrow> instr list" |
207 where |
209 where |
208 "shift p n = (map (\<lambda> (a, s). (a, (if s = 0 then 0 else s + n))) p)" |
210 "shift p n = (map (\<lambda> (a, s). (a, (if s = 0 then 0 else s + n))) p)" |