27 "code_tp [] = []" |
27 "code_tp [] = []" |
28 | "code_tp (c # tp) = (cell_num c) # code_tp tp" |
28 | "code_tp (c # tp) = (cell_num c) # code_tp tp" |
29 |
29 |
30 fun Code_tp where |
30 fun Code_tp where |
31 "Code_tp tp = lenc (code_tp tp)" |
31 "Code_tp tp = lenc (code_tp tp)" |
|
32 |
|
33 lemma code_tp_length [simp]: |
|
34 "length (code_tp tp) = length tp" |
|
35 by (induct tp) (simp_all) |
|
36 |
|
37 lemma code_tp_nth [simp]: |
|
38 "n < length tp \<Longrightarrow> (code_tp tp) ! n = cell_num (tp ! n)" |
|
39 apply(induct n arbitrary: tp) |
|
40 apply(simp_all) |
|
41 apply(case_tac [!] tp) |
|
42 apply(simp_all) |
|
43 done |
32 |
44 |
33 fun Code_conf where |
45 fun Code_conf where |
34 "Code_conf (s, l, r) = (s, Code_tp l, Code_tp r)" |
46 "Code_conf (s, l, r) = (s, Code_tp l, Code_tp r)" |
35 |
47 |
36 fun code_instr :: "instr \<Rightarrow> nat" where |
48 fun code_instr :: "instr \<Rightarrow> nat" where |
151 |
163 |
152 definition Stknum :: "nat \<Rightarrow> nat" |
164 definition Stknum :: "nat \<Rightarrow> nat" |
153 where |
165 where |
154 "Stknum z \<equiv> (\<Sum>i < enclen z. ldec z i) - 1" |
166 "Stknum z \<equiv> (\<Sum>i < enclen z. ldec z i) - 1" |
155 |
167 |
156 lemma Binnum_simulate1: |
168 |
157 "(Binnum z = 0) \<longleftrightarrow> (\<forall>i \<in> {..<enclen z}. ldec z i = 0)" |
169 definition |
158 by(auto simp add: Binnum_def) |
170 "right_std z \<equiv> (\<exists>i \<le> enclen z. (\<forall>j < i. ldec z j = 1) \<and> (\<forall>j < enclen z - i. ldec z (i + j) = 0))" |
159 |
171 |
160 lemma Binnum_simulate2: |
172 definition |
161 "(\<forall>i \<in> {..<enclen (Code_tp tp)}. ldec (Code_tp tp) i = 0) \<longleftrightarrow> (\<exists>k. tp = Bk \<up> k)" |
173 "left_std z \<equiv> (\<forall>j < enclen z. ldec z j = 0)" |
|
174 |
|
175 lemma ww: |
|
176 "(\<exists>k l. tp = Oc \<up> k @ Bk \<up> l) \<longleftrightarrow> |
|
177 (\<exists>i\<le>length tp. (\<forall>j < i. tp ! j = Oc) \<and> (\<forall>j < length tp - i. tp ! (i + j) = Bk))" |
|
178 apply(rule iffI) |
|
179 apply(erule exE)+ |
|
180 apply(simp) |
|
181 apply(rule_tac x="k" in exI) |
|
182 apply(auto)[1] |
|
183 apply(simp add: nth_append) |
|
184 apply(simp add: nth_append) |
|
185 apply(erule exE) |
|
186 apply(rule_tac x="i" in exI) |
|
187 apply(rule_tac x="length tp - i" in exI) |
|
188 apply(auto) |
|
189 apply(rule sym) |
|
190 apply(subst append_eq_conv_conj) |
|
191 apply(simp) |
|
192 apply(rule conjI) |
|
193 apply (smt length_replicate length_take nth_equalityI nth_replicate nth_take) |
|
194 by (smt length_drop length_replicate nth_drop nth_equalityI nth_replicate) |
|
195 |
|
196 lemma right_std: |
|
197 "(\<exists>k l. tp = Oc \<up> k @ Bk \<up> l) \<longleftrightarrow> right_std (Code_tp tp)" |
|
198 apply(simp add: right_std_def) |
|
199 apply(simp only: list_encode_inverse) |
|
200 apply(simp) |
|
201 apply(simp add: ww) |
|
202 apply(auto) |
|
203 apply(rule_tac x="i" in exI) |
|
204 apply(simp) |
|
205 apply(rule conjI) |
|
206 apply (metis Suc_eq_plus1 Suc_neq_Zero cell_num.cases cell_num.simps(1) leD less_trans linorder_neqE_nat) |
|
207 apply(auto) |
|
208 by (metis One_nat_def cell_num.cases cell_num.simps(2) less_diff_conv n_not_Suc_n nat_add_commute) |
|
209 |
|
210 lemma left_std: |
|
211 "(\<exists>k. tp = Bk \<up> k) \<longleftrightarrow> left_std (Code_tp tp)" |
|
212 apply(simp add: left_std_def) |
|
213 apply(simp only: list_encode_inverse) |
|
214 apply(simp) |
|
215 apply(auto) |
|
216 apply(rule_tac x="length tp" in exI) |
162 apply(induct tp) |
217 apply(induct tp) |
163 apply(simp) |
218 apply(simp) |
164 apply(simp) |
219 apply(simp) |
165 apply(simp add: lessThan_Suc) |
220 apply(auto) |
166 apply(case_tac a) |
221 apply(case_tac a) |
167 apply(simp) |
222 apply(auto) |
168 defer |
223 apply(case_tac a) |
169 apply(simp) |
224 apply(auto) |
170 oops |
225 by (metis Suc_less_eq nth_Cons_Suc) |
171 |
226 |
172 apply(simp add: Binnum_def) |
|
173 |
227 |
174 text {* |
228 text {* |
175 @{text "Std cf"} returns true, if the configuration @{text "cf"} |
229 @{text "Std cf"} returns true, if the configuration @{text "cf"} |
176 is a stardard tape. |
230 is a stardard tape. |
177 *} |
231 *} |
178 |
232 |
179 fun Std :: "nat \<Rightarrow> bool" |
233 fun Std :: "nat \<Rightarrow> bool" |
180 where |
234 where |
181 "Std cf = (Binnum (Left cf) = 0 \<and> |
235 "Std cf = (left_std (Left cf) \<and> right_std (Right cf))" |
182 (\<exists>x\<le>(enclen (Right cf)). Binnum (Right cf) = 2 ^ x))" |
|
183 |
236 |
184 text{* |
237 text{* |
185 @{text "Nostop m cf k"} means that afer @{text k} steps of |
238 @{text "Nostop m cf k"} means that afer @{text k} steps of |
186 execution the TM coded by @{text m} and started in configuration |
239 execution the TM coded by @{text m} and started in configuration |
187 @{text cf} is not at a stardard final configuration. *} |
240 @{text cf} is not at a stardard final configuration. *} |
310 by (case_tac cf) (simp) |
363 by (case_tac cf) (simp) |
311 |
364 |
312 lemma Std_simulate: |
365 lemma Std_simulate: |
313 "Std (Conf (Code_conf cf)) = std_tape (snd cf)" |
366 "Std (Conf (Code_conf cf)) = std_tape (snd cf)" |
314 apply(case_tac cf) |
367 apply(case_tac cf) |
|
368 apply(simp only: ) |
|
369 apply(simp only: std_tape_def) |
|
370 apply(rule trans) |
|
371 defer |
|
372 apply(simp) |
|
373 apply(subst Std.simps) |
|
374 apply(simp only: Left.simps Right.simps) |
|
375 apply(simp only: Code_conf.simps) |
|
376 apply(simp only: Conf.simps) |
|
377 apply(simp only: list_encode_inverse) |
|
378 apply(simp only: misc if_True) |
|
379 apply(simp only: Binnum_simulate) |
315 apply(simp add: std_tape_def del: Std.simps) |
380 apply(simp add: std_tape_def del: Std.simps) |
316 apply(subst Std.simps) |
381 apply(subst Std.simps) |
317 |
382 |
318 (* UNTIL HERE *) |
383 (* UNTIL HERE *) |
319 |
384 |