91 where |
91 where |
92 "tm_wf (p, off) = (length p \<ge> 2 \<and> length p mod 2 = 0 \<and> |
92 "tm_wf (p, off) = (length p \<ge> 2 \<and> length p mod 2 = 0 \<and> |
93 (\<forall>(a, s) \<in> set p. s \<le> length p div 2 |
93 (\<forall>(a, s) \<in> set p. s \<le> length p div 2 |
94 + off \<and> s \<ge> off))" |
94 + off \<and> s \<ge> off))" |
95 |
95 |
96 |
|
97 (* FIXME: needed? *) |
96 (* FIXME: needed? *) |
98 lemma halt_lemma: |
97 lemma halt_lemma: |
99 "\<lbrakk>wf LE; \<forall>n. (\<not> P (f n) \<longrightarrow> (f (Suc n), (f n)) \<in> LE)\<rbrakk> \<Longrightarrow> \<exists>n. P (f n)" |
98 "\<lbrakk>wf LE; \<forall>n. (\<not> P (f n) \<longrightarrow> (f (Suc n), (f n)) \<in> LE)\<rbrakk> \<Longrightarrow> \<exists>n. P (f n)" |
100 by (metis wf_iff_no_infinite_down_chain) |
99 by (metis wf_iff_no_infinite_down_chain) |
101 |
100 |
102 abbreviation exponent :: "'a \<Rightarrow> nat \<Rightarrow> 'a list" ("_ \<up> _" [100, 99] 100) |
101 abbreviation exponent :: "'a \<Rightarrow> nat \<Rightarrow> 'a list" ("_ \<up> _" [100, 99] 100) |
103 where "x \<up> n == replicate n x" |
102 where "x \<up> n == replicate n x" |
|
103 |
|
104 consts tape_of :: "'a \<Rightarrow> cell list" ("<_>" 100) |
|
105 |
|
106 fun tape_of_nat_list :: "nat list \<Rightarrow> cell list" |
|
107 where |
|
108 "tape_of_nat_list [] = []" | |
|
109 "tape_of_nat_list [n] = Oc\<up>(Suc n)" | |
|
110 "tape_of_nat_list (n#ns) = Oc\<up>(Suc n) @ Bk # (tape_of_nat_list ns)" |
|
111 |
|
112 defs (overloaded) |
|
113 tape_of_nl_abv: "<am> \<equiv> tape_of_nat_list am" |
|
114 tape_of_nat_abv : "<(n::nat)> \<equiv> Oc\<up>(Suc n)" |
104 |
115 |
105 definition tinres :: "cell list \<Rightarrow> cell list \<Rightarrow> bool" |
116 definition tinres :: "cell list \<Rightarrow> cell list \<Rightarrow> bool" |
106 where |
117 where |
107 "tinres xs ys = (\<exists>n. xs = ys @ Bk \<up> n \<or> ys = xs @ Bk \<up> n)" |
118 "tinres xs ys = (\<exists>n. xs = ys @ Bk \<up> n \<or> ys = xs @ Bk \<up> n)" |
108 |
119 |