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 |
32 |
|
33 lemma code_tp_append [simp]: |
|
34 "code_tp (tp1 @ tp2) = code_tp tp1 @ code_tp tp2" |
|
35 by(induct tp1) (simp_all) |
|
36 |
33 lemma code_tp_length [simp]: |
37 lemma code_tp_length [simp]: |
34 "length (code_tp tp) = length tp" |
38 "length (code_tp tp) = length tp" |
35 by (induct tp) (simp_all) |
39 by (induct tp) (simp_all) |
36 |
40 |
37 lemma code_tp_nth [simp]: |
41 lemma code_tp_nth [simp]: |
39 apply(induct n arbitrary: tp) |
43 apply(induct n arbitrary: tp) |
40 apply(simp_all) |
44 apply(simp_all) |
41 apply(case_tac [!] tp) |
45 apply(case_tac [!] tp) |
42 apply(simp_all) |
46 apply(simp_all) |
43 done |
47 done |
|
48 |
|
49 lemma code_tp_replicate [simp]: |
|
50 "code_tp (c \<up> n) = (cell_num c) \<up> n" |
|
51 by(induct n) (simp_all) |
|
52 |
44 |
53 |
45 fun Code_conf where |
54 fun Code_conf where |
46 "Code_conf (s, l, r) = (s, Code_tp l, Code_tp r)" |
55 "Code_conf (s, l, r) = (s, Code_tp l, Code_tp r)" |
47 |
56 |
48 fun code_instr :: "instr \<Rightarrow> nat" where |
57 fun code_instr :: "instr \<Rightarrow> nat" where |
124 where |
133 where |
125 "Newstate m q r = (if q \<noteq> 0 then (newstate (ldec m (q - 1)) r) else 0)" |
134 "Newstate m q r = (if q \<noteq> 0 then (newstate (ldec m (q - 1)) r) else 0)" |
126 |
135 |
127 fun Conf :: "nat \<times> (nat \<times> nat) \<Rightarrow> nat" |
136 fun Conf :: "nat \<times> (nat \<times> nat) \<Rightarrow> nat" |
128 where |
137 where |
129 "Conf (q, (l, r)) = lenc [q, l, r]" |
138 "Conf (q, l, r) = lenc [q, l, r]" |
130 |
139 |
131 fun State where |
140 fun State where |
132 "State cf = ldec cf 0" |
141 "State cf = ldec cf 0" |
133 |
142 |
134 fun Left where |
143 fun Left where |
138 "Right cf = ldec cf 2" |
147 "Right cf = ldec cf 2" |
139 |
148 |
140 fun Step :: "nat \<Rightarrow> nat \<Rightarrow> nat" |
149 fun Step :: "nat \<Rightarrow> nat \<Rightarrow> nat" |
141 where |
150 where |
142 "Step cf m = Conf (Newstate m (State cf) (Read (Right cf)), |
151 "Step cf m = Conf (Newstate m (State cf) (Read (Right cf)), |
143 (Newleft (Left cf) (Right cf) (Actn m (State cf) (Read (Right cf))), |
152 Newleft (Left cf) (Right cf) (Actn m (State cf) (Read (Right cf))), |
144 Newright (Left cf) (Right cf) (Actn m (State cf) (Read (Right cf)))))" |
153 Newright (Left cf) (Right cf) (Actn m (State cf) (Read (Right cf))))" |
145 |
154 |
146 text {* |
155 text {* |
147 @{text "Steps cf m k"} computes the TM configuration after @{text "k"} steps of execution |
156 @{text "Steps cf m k"} computes the TM configuration after @{text "k"} steps of execution |
148 of TM coded as @{text "m"}. |
157 of TM coded as @{text "m"}. |
149 *} |
158 *} |
155 |
164 |
156 text {* |
165 text {* |
157 Decoding tapes into binary or stroke numbers. |
166 Decoding tapes into binary or stroke numbers. |
158 *} |
167 *} |
159 |
168 |
160 definition Binnum :: "nat \<Rightarrow> nat" |
|
161 where |
|
162 "Binnum z \<equiv> (\<Sum>i < enclen z. ldec z i * 2 ^ i)" |
|
163 |
|
164 definition Stknum :: "nat \<Rightarrow> nat" |
169 definition Stknum :: "nat \<Rightarrow> nat" |
165 where |
170 where |
166 "Stknum z \<equiv> (\<Sum>i < enclen z. ldec z i) - 1" |
171 "Stknum z \<equiv> (\<Sum>i < enclen z. ldec z i)" |
167 |
172 |
168 |
173 |
169 definition |
174 definition |
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))" |
175 "right_std z \<equiv> (\<exists>i \<le> enclen z. 1 \<le> i \<and> (\<forall>j < i. ldec z j = 1) \<and> (\<forall>j < enclen z - i. ldec z (i + j) = 0))" |
171 |
176 |
172 definition |
177 definition |
173 "left_std z \<equiv> (\<forall>j < enclen z. ldec z j = 0)" |
178 "left_std z \<equiv> (\<forall>j < enclen z. ldec z j = 0)" |
174 |
179 |
175 lemma ww: |
180 lemma ww: |
176 "(\<exists>k l. tp = Oc \<up> k @ Bk \<up> l) \<longleftrightarrow> |
181 "(\<exists>k l. 1 \<le> k \<and> 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))" |
182 (\<exists>i\<le>length tp. 1 \<le> i \<and> (\<forall>j < i. tp ! j = Oc) \<and> (\<forall>j < length tp - i. tp ! (i + j) = Bk))" |
178 apply(rule iffI) |
183 apply(rule iffI) |
179 apply(erule exE)+ |
184 apply(erule exE)+ |
180 apply(simp) |
185 apply(simp) |
181 apply(rule_tac x="k" in exI) |
186 apply(rule_tac x="k" in exI) |
182 apply(auto)[1] |
187 apply(auto)[1] |
192 apply(rule conjI) |
197 apply(rule conjI) |
193 apply (smt length_replicate length_take nth_equalityI nth_replicate nth_take) |
198 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) |
199 by (smt length_drop length_replicate nth_drop nth_equalityI nth_replicate) |
195 |
200 |
196 lemma right_std: |
201 lemma right_std: |
197 "(\<exists>k l. tp = Oc \<up> k @ Bk \<up> l) \<longleftrightarrow> right_std (Code_tp tp)" |
202 "(\<exists>k l. 1 \<le> k \<and> tp = Oc \<up> k @ Bk \<up> l) \<longleftrightarrow> right_std (Code_tp tp)" |
|
203 apply(simp only: ww) |
198 apply(simp add: right_std_def) |
204 apply(simp add: right_std_def) |
199 apply(simp only: list_encode_inverse) |
205 apply(simp only: list_encode_inverse) |
200 apply(simp) |
206 apply(simp) |
201 apply(simp add: ww) |
|
202 apply(auto) |
207 apply(auto) |
203 apply(rule_tac x="i" in exI) |
208 apply(rule_tac x="i" in exI) |
204 apply(simp) |
209 apply(simp) |
205 apply(rule conjI) |
210 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) |
211 apply (metis Suc_eq_plus1 Suc_neq_Zero cell_num.cases cell_num.simps(1) leD less_trans linorder_neqE_nat) |
223 apply(case_tac a) |
228 apply(case_tac a) |
224 apply(auto) |
229 apply(auto) |
225 by (metis Suc_less_eq nth_Cons_Suc) |
230 by (metis Suc_less_eq nth_Cons_Suc) |
226 |
231 |
227 |
232 |
|
233 lemma Stknum_append: |
|
234 "Stknum (Code_tp (tp1 @ tp2)) = Stknum (Code_tp tp1) + Stknum (Code_tp tp2)" |
|
235 apply(simp only: Code_tp.simps) |
|
236 apply(simp only: code_tp_append) |
|
237 apply(simp only: Stknum_def) |
|
238 apply(simp only: enclen_length length_append code_tp_length) |
|
239 apply(simp only: list_encode_inverse) |
|
240 apply(simp only: enclen_length length_append code_tp_length) |
|
241 apply(simp) |
|
242 apply(subgoal_tac "{..<length tp1 + length tp2} = {..<length tp1} \<union> {length tp1 ..<length tp1 + length tp2}") |
|
243 prefer 2 |
|
244 apply(auto)[1] |
|
245 apply(simp only:) |
|
246 apply(subst setsum_Un_disjoint) |
|
247 apply(auto)[2] |
|
248 apply (metis ivl_disj_int_one(2)) |
|
249 apply(simp add: nth_append) |
|
250 apply(subgoal_tac "{length tp1..<length tp1 + length tp2} = (\<lambda>x. x + length tp1) ` {0..<length tp2}") |
|
251 prefer 2 |
|
252 apply(simp only: image_add_atLeastLessThan) |
|
253 apply (metis comm_monoid_add_class.add.left_neutral nat_add_commute) |
|
254 apply(simp only:) |
|
255 apply(subst setsum_reindex) |
|
256 prefer 2 |
|
257 apply(simp add: comp_def) |
|
258 apply (metis atLeast0LessThan) |
|
259 apply(simp add: inj_on_def) |
|
260 done |
|
261 |
|
262 lemma Stknum_up: |
|
263 "Stknum (lenc (a \<up> n)) = n * a" |
|
264 apply(induct n) |
|
265 apply(simp_all add: Stknum_def list_encode_inverse del: replicate.simps) |
|
266 done |
|
267 |
|
268 lemma result: |
|
269 "Stknum (Code_tp (<n> @ Bk \<up> l)) - 1 = n" |
|
270 apply(simp only: Stknum_append) |
|
271 apply(simp only: tape_of_nat.simps) |
|
272 apply(simp only: Code_tp.simps) |
|
273 apply(simp only: code_tp_replicate) |
|
274 apply(simp only: cell_num.simps) |
|
275 apply(simp only: Stknum_up) |
|
276 apply(simp) |
|
277 done |
|
278 |
228 text {* |
279 text {* |
229 @{text "Std cf"} returns true, if the configuration @{text "cf"} |
280 @{text "Std cf"} returns true, if the configuration @{text "cf"} |
230 is a stardard tape. |
281 is a stardard tape. |
231 *} |
282 *} |
232 |
283 |
241 |
292 |
242 fun Final :: "nat \<Rightarrow> bool" |
293 fun Final :: "nat \<Rightarrow> bool" |
243 where |
294 where |
244 "Final cf = (State cf = 0)" |
295 "Final cf = (State cf = 0)" |
245 |
296 |
246 fun Nostop :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool" |
297 fun Stop :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool" |
247 where |
298 where |
248 "Nostop m cf k = (Final (Steps cf m k) \<and> \<not> Std (Steps cf m k))" |
299 "Stop m cf k = (Final (Steps cf m k) \<and> Std (Steps cf m k))" |
249 |
300 |
250 text{* |
301 text{* |
251 @{text "Halt"} is the function calculating the steps a TM needs to |
302 @{text "Halt"} is the function calculating the steps a TM needs to |
252 execute before reaching a stardard final configuration. This recursive |
303 execute before reaching a stardard final configuration. This recursive |
253 function is the only one that uses unbounded minimization. So it is the |
304 function is the only one that uses unbounded minimization. So it is the |
255 of the universal function @{text "UF"}. |
306 of the universal function @{text "UF"}. |
256 *} |
307 *} |
257 |
308 |
258 fun Halt :: "nat \<Rightarrow> nat \<Rightarrow> nat" |
309 fun Halt :: "nat \<Rightarrow> nat \<Rightarrow> nat" |
259 where |
310 where |
260 "Halt m cf = (LEAST k. \<not> Nostop m cf k)" |
311 "Halt m cf = (LEAST k. Stop m cf k)" |
261 |
312 |
262 fun UF :: "nat \<Rightarrow> nat \<Rightarrow> nat" |
313 fun UF :: "nat \<Rightarrow> nat \<Rightarrow> nat" |
263 where |
314 where |
264 "UF m cf = Stknum (Right (Steps m cf (Halt m cf)))" |
315 "UF m cf = Stknum (Right (Steps cf m (Halt m cf))) - 1" |
265 |
316 |
266 section {* The UF can simulate Turing machines *} |
317 section {* The UF can simulate Turing machines *} |
267 |
318 |
268 lemma Update_left_simulate: |
319 lemma Update_left_simulate: |
269 shows "Newleft (Code_tp l) (Code_tp r) (action_num a) = Code_tp (fst (update a (l, r)))" |
320 shows "Newleft (Code_tp l) (Code_tp r) (action_num a) = Code_tp (fst (update a (l, r)))" |
361 lemma Final_simulate: |
412 lemma Final_simulate: |
362 "Final (Conf (Code_conf cf)) = is_final cf" |
413 "Final (Conf (Code_conf cf)) = is_final cf" |
363 by (case_tac cf) (simp) |
414 by (case_tac cf) (simp) |
364 |
415 |
365 lemma Std_simulate: |
416 lemma Std_simulate: |
366 "Std (Conf (Code_conf cf)) = std_tape (snd cf)" |
417 "Std (Conf (Code_conf cf)) = std_tape cf" |
367 apply(case_tac cf) |
418 apply(case_tac cf) |
368 apply(simp only: ) |
|
369 apply(simp only: std_tape_def) |
419 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) |
420 apply(simp only: Code_conf.simps) |
376 apply(simp only: Conf.simps) |
421 apply(simp only: Conf.simps) |
|
422 apply(simp only: Std.simps) |
|
423 apply(simp only: Left.simps Right.simps) |
377 apply(simp only: list_encode_inverse) |
424 apply(simp only: list_encode_inverse) |
378 apply(simp only: misc if_True) |
425 apply(simp only: misc if_True) |
379 apply(simp only: Binnum_simulate) |
426 apply(simp only: left_std[symmetric] right_std[symmetric]) |
380 apply(simp add: std_tape_def del: Std.simps) |
427 apply(simp) |
381 apply(subst Std.simps) |
428 apply(auto) |
382 |
429 apply(rule_tac x="ka - 1" in exI) |
383 (* UNTIL HERE *) |
430 apply(rule_tac x="l" in exI) |
384 |
431 apply(simp) |
|
432 apply (metis Suc_diff_le diff_Suc_Suc diff_zero replicate_Suc) |
|
433 apply(rule_tac x="n + 1" in exI) |
|
434 apply(simp) |
|
435 done |
|
436 |
|
437 lemma UF_simulate: |
|
438 assumes "tm_wf tm" |
|
439 shows "UF (Code_tprog tm) (Conf (Code_conf cf)) = |
|
440 Stknum (Right (Conf |
|
441 (Code_conf (steps cf tm (LEAST n. is_final (steps cf tm n) \<and> std_tape (steps cf tm n)))))) - 1" |
|
442 apply(simp only: UF.simps) |
|
443 apply(subst Steps_simulate[symmetric, OF assms]) |
|
444 apply(subst Final_simulate[symmetric]) |
|
445 apply(subst Std_simulate[symmetric]) |
|
446 apply(simp only: Halt.simps) |
|
447 apply(simp only: Steps_simulate[symmetric, OF assms]) |
|
448 apply(simp only: Stop.simps[symmetric]) |
|
449 done |
|
450 |
|
451 text {* UNTIL HERE *} |
385 |
452 |
386 section {* Universal Function as Recursive Functions *} |
453 section {* Universal Function as Recursive Functions *} |
387 |
454 |
388 definition |
455 definition |
389 "rec_entry = CN rec_lo [Id 2 0, CN rec_pi [CN S [Id 2 1]]]" |
456 "rec_entry = CN rec_lo [Id 2 0, CN rec_pi [CN S [Id 2 1]]]" |