177 (\<forall>(a, s) \<in> set p. s \<le> length p div 2 + off \<and> s \<ge> off))" |
177 (\<forall>(a, s) \<in> set p. s \<le> length p div 2 + off \<and> s \<ge> off))" |
178 |
178 |
179 abbreviation |
179 abbreviation |
180 "tm_wf0 p \<equiv> tm_wf (p, 0)" |
180 "tm_wf0 p \<equiv> tm_wf (p, 0)" |
181 |
181 |
182 lemma halt_lemma: |
|
183 "\<lbrakk>wf LE; \<forall>n. (\<not> P (f n) \<longrightarrow> (f (Suc n), (f n)) \<in> LE)\<rbrakk> \<Longrightarrow> \<exists>n. P (f n)" |
|
184 by (metis wf_iff_no_infinite_down_chain) |
|
185 |
|
186 abbreviation exponent :: "'a \<Rightarrow> nat \<Rightarrow> 'a list" ("_ \<up> _" [100, 99] 100) |
182 abbreviation exponent :: "'a \<Rightarrow> nat \<Rightarrow> 'a list" ("_ \<up> _" [100, 99] 100) |
187 where "x \<up> n == replicate n x" |
183 where "x \<up> n == replicate n x" |
188 |
184 |
189 consts tape_of :: "'a \<Rightarrow> cell list" ("<_>" 100) |
185 consts tape_of :: "'a \<Rightarrow> cell list" ("<_>" 100) |
190 |
186 |
191 fun tape_of_nat_list :: "nat list \<Rightarrow> cell list" |
187 defs (overloaded) |
|
188 tape_of_nat_abv: "<(n::nat)> \<equiv> Oc \<up> (Suc n)" |
|
189 |
|
190 fun tape_of_nat_list :: "'a list \<Rightarrow> cell list" |
192 where |
191 where |
193 "tape_of_nat_list [] = []" | |
192 "tape_of_nat_list [] = []" | |
194 "tape_of_nat_list [n] = Oc\<up>(Suc n)" | |
193 "tape_of_nat_list [n] = <n>" | |
195 "tape_of_nat_list (n#ns) = Oc\<up>(Suc n) @ Bk # (tape_of_nat_list ns)" |
194 "tape_of_nat_list (n#ns) = <n> @ Bk # (tape_of_nat_list ns)" |
196 |
195 |
197 fun tape_of_nat_pair :: "nat \<times> nat \<Rightarrow> cell list" |
196 fun tape_of_nat_pair :: "'a \<times> 'b \<Rightarrow> cell list" |
198 where |
197 where |
199 "tape_of_nat_pair (n, m) = Oc\<up>(Suc n) @ [Bk] @ Oc\<up>(Suc m)" |
198 "tape_of_nat_pair (n, m) = <n> @ [Bk] @ <m>" |
200 |
199 |
201 |
200 |
202 defs (overloaded) |
201 defs (overloaded) |
203 tape_of_nl_abv: "<ns> \<equiv> tape_of_nat_list ns" |
202 tape_of_nl_abv: "<(ns::'a list)> \<equiv> tape_of_nat_list ns" |
204 tape_of_nat_abv: "<(n::nat)> \<equiv> Oc\<up>(Suc n)" |
203 tape_of_nat_pair: "<(np::'a\<times>'b)> \<equiv> tape_of_nat_pair np" |
205 tape_of_nat_pair: "<p> \<equiv> tape_of_nat_pair p" |
|
206 |
204 |
207 fun |
205 fun |
208 shift :: "instr list \<Rightarrow> nat \<Rightarrow> instr list" |
206 shift :: "instr list \<Rightarrow> nat \<Rightarrow> instr list" |
209 where |
207 where |
210 "shift p n = (map (\<lambda> (a, s). (a, (if s = 0 then 0 else s + n))) p)" |
208 "shift p n = (map (\<lambda> (a, s). (a, (if s = 0 then 0 else s + n))) p)" |