|
1 theory UF_Rec |
|
2 imports Recs Hoare_tm |
|
3 begin |
|
4 |
|
5 section {* Coding of Turing Machines and Tapes*} |
|
6 |
|
7 |
|
8 fun actnum :: "taction \<Rightarrow> nat" |
|
9 where |
|
10 "actnum W0 = 0" |
|
11 | "actnum W1 = 1" |
|
12 | "actnum L = 2" |
|
13 | "actnum R = 3" |
|
14 |
|
15 |
|
16 fun cellnum :: "Block \<Rightarrow> nat" where |
|
17 "cellnum Bk = 0" |
|
18 | "cellnum Oc = 1" |
|
19 |
|
20 |
|
21 (* NEED TO CODE TAPES *) |
|
22 |
|
23 text {* Coding tapes *} |
|
24 |
|
25 fun code_tp :: "cell list \<Rightarrow> nat list" |
|
26 where |
|
27 "code_tp [] = []" |
|
28 | "code_tp (c # tp) = (cellnum c) # code_tp tp" |
|
29 |
|
30 fun Code_tp where |
|
31 "Code_tp tp = lenc (code_tp tp)" |
|
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 |
|
37 lemma code_tp_length [simp]: |
|
38 "length (code_tp tp) = length tp" |
|
39 by (induct tp) (simp_all) |
|
40 |
|
41 lemma code_tp_nth [simp]: |
|
42 "n < length tp \<Longrightarrow> (code_tp tp) ! n = cellnum (tp ! n)" |
|
43 apply(induct n arbitrary: tp) |
|
44 apply(simp_all) |
|
45 apply(case_tac [!] tp) |
|
46 apply(simp_all) |
|
47 done |
|
48 |
|
49 lemma code_tp_replicate [simp]: |
|
50 "code_tp (c \<up> n) = (cellnum c) \<up> n" |
|
51 by(induct n) (simp_all) |
|
52 |
|
53 text {* Coding Configurations and TMs *} |
|
54 |
|
55 fun Code_conf where |
|
56 "Code_conf (s, l, r) = (s, Code_tp l, Code_tp r)" |
|
57 |
|
58 fun code_instr :: "instr \<Rightarrow> nat" where |
|
59 "code_instr i = penc (actnum (fst i)) (snd i)" |
|
60 |
|
61 fun Code_instr :: "instr \<times> instr \<Rightarrow> nat" where |
|
62 "Code_instr i = penc (code_instr (fst i)) (code_instr (snd i))" |
|
63 |
|
64 fun code_tprog :: "tprog \<Rightarrow> nat list" |
|
65 where |
|
66 "code_tprog [] = []" |
|
67 | "code_tprog (i # tm) = Code_instr i # code_tprog tm" |
|
68 |
|
69 lemma code_tprog_length [simp]: |
|
70 "length (code_tprog tp) = length tp" |
|
71 by (induct tp) (simp_all) |
|
72 |
|
73 lemma code_tprog_nth [simp]: |
|
74 "n < length tp \<Longrightarrow> (code_tprog tp) ! n = Code_instr (tp ! n)" |
|
75 by (induct tp arbitrary: n) (simp_all add: nth_Cons') |
|
76 |
|
77 fun Code_tprog :: "tprog \<Rightarrow> nat" |
|
78 where |
|
79 "Code_tprog tm = lenc (code_tprog tm)" |
|
80 |
|
81 |
|
82 section {* An Universal Function in HOL *} |
|
83 |
|
84 text {* Reading and writing the encoded tape *} |
|
85 |
|
86 fun Read where |
|
87 "Read tp = ldec tp 0" |
|
88 |
|
89 fun Write where |
|
90 "Write n tp = penc (Suc n) (pdec2 tp)" |
|
91 |
|
92 text {* |
|
93 The @{text Newleft} and @{text Newright} functions on page 91 of B book. |
|
94 They calculate the new left and right tape (@{text p} and @{text r}) |
|
95 according to an action @{text a}. Adapted to our encoding functions. |
|
96 *} |
|
97 |
|
98 fun Newleft :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat" |
|
99 where |
|
100 "Newleft l r a = (if a = 0 then l else |
|
101 if a = 1 then l else |
|
102 if a = 2 then pdec2 l else |
|
103 if a = 3 then penc (Suc (Read r)) l |
|
104 else l)" |
|
105 |
|
106 fun Newright :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat" |
|
107 where |
|
108 "Newright l r a = (if a = 0 then Write 0 r |
|
109 else if a = 1 then Write 1 r |
|
110 else if a = 2 then penc (Suc (Read l)) r |
|
111 else if a = 3 then pdec2 r |
|
112 else r)" |
|
113 |
|
114 text {* |
|
115 The @{text "Action"} function given on page 92 of B book, which is used to |
|
116 fetch Turing Machine intructions. In @{text "Action m q r"}, @{text "m"} is |
|
117 the code of the Turing Machine, @{text "q"} is the current state of |
|
118 Turing Machine, and @{text "r"} is the scanned cell of is the right tape. |
|
119 *} |
|
120 |
|
121 fun Actn :: "nat \<Rightarrow> nat \<Rightarrow> nat" where |
|
122 "Actn n 0 = pdec1 (pdec1 n)" |
|
123 | "Actn n _ = pdec1 (pdec2 n)" |
|
124 |
|
125 fun Action :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat" |
|
126 where |
|
127 "Action m q c = (if q \<noteq> 0 \<and> within m (q - 1) then Actn (ldec m (q - 1)) c else 4)" |
|
128 |
|
129 fun Newstat :: "nat \<Rightarrow> nat \<Rightarrow> nat" where |
|
130 "Newstat n 0 = pdec2 (pdec1 n)" |
|
131 | "Newstat n _ = pdec2 (pdec2 n)" |
|
132 |
|
133 fun Newstate :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat" |
|
134 where |
|
135 "Newstate m q r = (if q \<noteq> 0 then Newstat (ldec m (q - 1)) r else 0)" |
|
136 |
|
137 fun Conf :: "nat \<times> (nat \<times> nat) \<Rightarrow> nat" |
|
138 where |
|
139 "Conf (q, l, r) = lenc [q, l, r]" |
|
140 |
|
141 fun State where |
|
142 "State cf = ldec cf 0" |
|
143 |
|
144 fun Left where |
|
145 "Left cf = ldec cf 1" |
|
146 |
|
147 fun Right where |
|
148 "Right cf = ldec cf 2" |
|
149 |
|
150 text {* |
|
151 @{text "Steps cf m k"} computes the TM configuration after @{text "k"} steps of |
|
152 execution of TM coded as @{text "m"}. @{text Step} is a single step of the TM. |
|
153 *} |
|
154 |
|
155 fun Step :: "nat \<Rightarrow> nat \<Rightarrow> nat" |
|
156 where |
|
157 "Step cf m = Conf (Newstate m (State cf) (Read (Right cf)), |
|
158 Newleft (Left cf) (Right cf) (Action m (State cf) (Read (Right cf))), |
|
159 Newright (Left cf) (Right cf) (Action m (State cf) (Read (Right cf))))" |
|
160 |
|
161 fun Steps :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat" |
|
162 where |
|
163 "Steps cf p 0 = cf" |
|
164 | "Steps cf p (Suc n) = Steps (Step cf p) p n" |
|
165 |
|
166 lemma Step_Steps_comm: |
|
167 "Step (Steps cf p n) p = Steps (Step cf p) p n" |
|
168 by (induct n arbitrary: cf) (simp_all only: Steps.simps) |
|
169 |
|
170 |
|
171 text {* Decoding tapes back into numbers. *} |
|
172 |
|
173 definition Stknum :: "nat \<Rightarrow> nat" |
|
174 where |
|
175 "Stknum z \<equiv> (\<Sum>i < enclen z. ldec z i)" |
|
176 |
|
177 lemma Stknum_append: |
|
178 "Stknum (Code_tp (tp1 @ tp2)) = Stknum (Code_tp tp1) + Stknum (Code_tp tp2)" |
|
179 apply(simp only: Code_tp.simps) |
|
180 apply(simp only: code_tp_append) |
|
181 apply(simp only: Stknum_def) |
|
182 apply(simp only: enclen_length length_append code_tp_length) |
|
183 apply(simp only: list_encode_inverse) |
|
184 apply(simp only: enclen_length length_append code_tp_length) |
|
185 apply(simp) |
|
186 apply(subgoal_tac "{..<length tp1 + length tp2} = {..<length tp1} \<union> {length tp1 ..<length tp1 + length tp2}") |
|
187 prefer 2 |
|
188 apply(auto)[1] |
|
189 apply(simp only:) |
|
190 apply(subst setsum_Un_disjoint) |
|
191 apply(auto)[2] |
|
192 apply (metis ivl_disj_int_one(2)) |
|
193 apply(simp add: nth_append) |
|
194 apply(subgoal_tac "{length tp1..<length tp1 + length tp2} = (\<lambda>x. x + length tp1) ` {0..<length tp2}") |
|
195 prefer 2 |
|
196 apply(simp only: image_add_atLeastLessThan) |
|
197 apply (metis comm_monoid_add_class.add.left_neutral nat_add_commute) |
|
198 apply(simp only:) |
|
199 apply(subst setsum_reindex) |
|
200 prefer 2 |
|
201 apply(simp add: comp_def) |
|
202 apply (metis atLeast0LessThan) |
|
203 apply(simp add: inj_on_def) |
|
204 done |
|
205 |
|
206 lemma Stknum_up: |
|
207 "Stknum (lenc (a \<up> n)) = n * a" |
|
208 apply(induct n) |
|
209 apply(simp_all add: Stknum_def list_encode_inverse del: replicate.simps) |
|
210 done |
|
211 |
|
212 lemma result: |
|
213 "Stknum (Code_tp (<n> @ Bk \<up> l)) - 1 = n" |
|
214 apply(simp only: Stknum_append) |
|
215 apply(simp only: tape_of_nat.simps) |
|
216 apply(simp only: Code_tp.simps) |
|
217 apply(simp only: code_tp_replicate) |
|
218 apply(simp only: cellnum.simps) |
|
219 apply(simp only: Stknum_up) |
|
220 apply(simp) |
|
221 done |
|
222 |
|
223 |
|
224 section {* Standard Tapes *} |
|
225 |
|
226 definition |
|
227 "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))" |
|
228 |
|
229 definition |
|
230 "left_std z \<equiv> (\<forall>j < enclen z. ldec z j = 0)" |
|
231 |
|
232 lemma ww: |
|
233 "(\<exists>k l. 1 \<le> k \<and> tp = Oc \<up> k @ Bk \<up> l) \<longleftrightarrow> |
|
234 (\<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))" |
|
235 apply(rule iffI) |
|
236 apply(erule exE)+ |
|
237 apply(simp) |
|
238 apply(rule_tac x="k" in exI) |
|
239 apply(auto)[1] |
|
240 apply(simp add: nth_append) |
|
241 apply(simp add: nth_append) |
|
242 apply(erule exE) |
|
243 apply(rule_tac x="i" in exI) |
|
244 apply(rule_tac x="length tp - i" in exI) |
|
245 apply(auto) |
|
246 apply(rule sym) |
|
247 apply(subst append_eq_conv_conj) |
|
248 apply(simp) |
|
249 apply(rule conjI) |
|
250 apply (smt length_replicate length_take nth_equalityI nth_replicate nth_take) |
|
251 by (smt length_drop length_replicate nth_drop nth_equalityI nth_replicate) |
|
252 |
|
253 lemma right_std: |
|
254 "(\<exists>k l. 1 \<le> k \<and> tp = Oc \<up> k @ Bk \<up> l) \<longleftrightarrow> right_std (Code_tp tp)" |
|
255 apply(simp only: ww) |
|
256 apply(simp add: right_std_def) |
|
257 apply(simp only: list_encode_inverse) |
|
258 apply(simp) |
|
259 apply(auto) |
|
260 apply(rule_tac x="i" in exI) |
|
261 apply(simp) |
|
262 apply(rule conjI) |
|
263 apply (metis Suc_eq_plus1 Suc_neq_Zero cellnum.cases cellnum.simps(1) leD less_trans linorder_neqE_nat) |
|
264 apply(auto) |
|
265 by (metis One_nat_def cellnum.cases cellnum.simps(2) less_diff_conv n_not_Suc_n nat_add_commute) |
|
266 |
|
267 lemma left_std: |
|
268 "(\<exists>k. tp = Bk \<up> k) \<longleftrightarrow> left_std (Code_tp tp)" |
|
269 apply(simp add: left_std_def) |
|
270 apply(simp only: list_encode_inverse) |
|
271 apply(simp) |
|
272 apply(auto) |
|
273 apply(rule_tac x="length tp" in exI) |
|
274 apply(induct tp) |
|
275 apply(simp) |
|
276 apply(simp) |
|
277 apply(auto) |
|
278 apply(case_tac a) |
|
279 apply(auto) |
|
280 apply(case_tac a) |
|
281 apply(auto) |
|
282 by (metis Suc_less_eq nth_Cons_Suc) |
|
283 |
|
284 |
|
285 section {* Standard- and Final Configurations, the Universal Function *} |
|
286 |
|
287 text {* |
|
288 @{text "Std cf"} returns true, if the configuration @{text "cf"} |
|
289 is a stardard tape. |
|
290 *} |
|
291 |
|
292 fun Std :: "nat \<Rightarrow> bool" |
|
293 where |
|
294 "Std cf = (left_std (Left cf) \<and> right_std (Right cf))" |
|
295 |
|
296 text{* |
|
297 @{text "Stop m cf k"} means that afer @{text k} steps of |
|
298 execution the TM coded by @{text m} and started in configuration |
|
299 @{text cf} is in a stardard final configuration. *} |
|
300 |
|
301 fun Final :: "nat \<Rightarrow> bool" |
|
302 where |
|
303 "Final cf = (State cf = 0)" |
|
304 |
|
305 fun Stop :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool" |
|
306 where |
|
307 "Stop m cf k = (Final (Steps cf m k) \<and> Std (Steps cf m k))" |
|
308 |
|
309 text{* |
|
310 @{text "Halt"} is the function calculating the steps a TM needs to |
|
311 execute before reaching a stardard final configuration. This recursive |
|
312 function is the only one that uses unbounded minimization. So it is the |
|
313 only non-primitive recursive function needs to be used in the construction |
|
314 of the universal function @{text "UF"}. |
|
315 *} |
|
316 |
|
317 fun Halt :: "nat \<Rightarrow> nat \<Rightarrow> nat" |
|
318 where |
|
319 "Halt m cf = (LEAST k. Stop m cf k)" |
|
320 |
|
321 fun UF :: "nat \<Rightarrow> nat \<Rightarrow> nat" |
|
322 where |
|
323 "UF m cf = Stknum (Right (Steps cf m (Halt m cf))) - 1" |
|
324 |
|
325 |
|
326 section {* The UF simulates Turing machines *} |
|
327 |
|
328 lemma Update_left_simulate: |
|
329 shows "Newleft (Code_tp l) (Code_tp r) (actnum a) = Code_tp (fst (update a (l, r)))" |
|
330 apply(induct a) |
|
331 apply(simp_all) |
|
332 apply(case_tac l) |
|
333 apply(simp_all) |
|
334 apply(case_tac r) |
|
335 apply(simp_all) |
|
336 done |
|
337 |
|
338 lemma Update_right_simulate: |
|
339 shows "Newright (Code_tp l) (Code_tp r) (actnum a) = Code_tp (snd (update a (l, r)))" |
|
340 apply(induct a) |
|
341 apply(simp_all) |
|
342 apply(case_tac r) |
|
343 apply(simp_all) |
|
344 apply(case_tac r) |
|
345 apply(simp_all) |
|
346 apply(case_tac l) |
|
347 apply(simp_all) |
|
348 apply(case_tac r) |
|
349 apply(simp_all) |
|
350 done |
|
351 |
|
352 lemma Fetch_state_simulate: |
|
353 "tm_wf tp \<Longrightarrow> Newstate (Code_tprog tp) st (cellnum c) = snd (fetch tp st c)" |
|
354 apply(induct tp st c rule: fetch.induct) |
|
355 apply(simp_all add: list_encode_inverse split: cell.split) |
|
356 done |
|
357 |
|
358 lemma Fetch_action_simulate: |
|
359 "tm_wf tp \<Longrightarrow> Action (Code_tprog tp) st (cellnum c) = actnum (fst (fetch tp st c))" |
|
360 apply(induct tp st c rule: fetch.induct) |
|
361 apply(simp_all add: list_encode_inverse split: cell.split) |
|
362 done |
|
363 |
|
364 lemma Read_simulate: |
|
365 "Read (Code_tp tp) = cellnum (read tp)" |
|
366 apply(case_tac tp) |
|
367 apply(simp_all) |
|
368 done |
|
369 |
|
370 lemma misc: |
|
371 "2 < (3::nat)" |
|
372 "1 < (3::nat)" |
|
373 "0 < (3::nat)" |
|
374 "length [x] = 1" |
|
375 "length [x, y] = 2" |
|
376 "length [x, y , z] = 3" |
|
377 "[x, y, z] ! 0 = x" |
|
378 "[x, y, z] ! 1 = y" |
|
379 "[x, y, z] ! 2 = z" |
|
380 apply(simp_all) |
|
381 done |
|
382 |
|
383 lemma Step_simulate: |
|
384 assumes "tm_wf tp" |
|
385 shows "Step (Conf (Code_conf (st, l, r))) (Code_tprog tp) = Conf (Code_conf (step (st, l, r) tp))" |
|
386 apply(subst step.simps) |
|
387 apply(simp only: Let_def) |
|
388 apply(subst Step.simps) |
|
389 apply(simp only: Conf.simps Code_conf.simps Right.simps Left.simps) |
|
390 apply(simp only: list_encode_inverse) |
|
391 apply(simp only: misc if_True Code_tp.simps) |
|
392 apply(simp only: prod_case_beta) |
|
393 apply(subst Fetch_state_simulate[OF assms, symmetric]) |
|
394 apply(simp only: State.simps) |
|
395 apply(simp only: list_encode_inverse) |
|
396 apply(simp only: misc if_True) |
|
397 apply(simp only: Read_simulate[simplified Code_tp.simps]) |
|
398 apply(simp only: Fetch_action_simulate[OF assms]) |
|
399 apply(simp only: Update_left_simulate[simplified Code_tp.simps]) |
|
400 apply(simp only: Update_right_simulate[simplified Code_tp.simps]) |
|
401 apply(case_tac "update (fst (fetch tp st (read r))) (l, r)") |
|
402 apply(simp only: Code_conf.simps) |
|
403 apply(simp only: Conf.simps) |
|
404 apply(simp) |
|
405 done |
|
406 |
|
407 lemma Steps_simulate: |
|
408 assumes "tm_wf tp" |
|
409 shows "Steps (Conf (Code_conf cf)) (Code_tprog tp) n = Conf (Code_conf (steps cf tp n))" |
|
410 apply(induct n arbitrary: cf) |
|
411 apply(simp) |
|
412 apply(simp only: Steps.simps steps.simps) |
|
413 apply(case_tac cf) |
|
414 apply(simp only: ) |
|
415 apply(subst Step_simulate) |
|
416 apply(rule assms) |
|
417 apply(drule_tac x="step (a, b, c) tp" in meta_spec) |
|
418 apply(simp) |
|
419 done |
|
420 |
|
421 lemma Final_simulate: |
|
422 "Final (Conf (Code_conf cf)) = is_final cf" |
|
423 by (case_tac cf) (simp) |
|
424 |
|
425 lemma Std_simulate: |
|
426 "Std (Conf (Code_conf cf)) = std_tape cf" |
|
427 apply(case_tac cf) |
|
428 apply(simp only: std_tape_def) |
|
429 apply(simp only: Code_conf.simps) |
|
430 apply(simp only: Conf.simps) |
|
431 apply(simp only: Std.simps) |
|
432 apply(simp only: Left.simps Right.simps) |
|
433 apply(simp only: list_encode_inverse) |
|
434 apply(simp only: misc if_True) |
|
435 apply(simp only: left_std[symmetric] right_std[symmetric]) |
|
436 apply(simp) |
|
437 by (metis Suc_le_D Suc_neq_Zero append_Cons nat.exhaust not_less_eq_eq replicate_Suc) |
|
438 |
|
439 |
|
440 lemma UF_simulate: |
|
441 assumes "tm_wf tm" |
|
442 shows "UF (Code_tprog tm) (Conf (Code_conf cf)) = |
|
443 Stknum (Right (Conf |
|
444 (Code_conf (steps cf tm (LEAST n. is_final (steps cf tm n) \<and> std_tape (steps cf tm n)))))) - 1" |
|
445 apply(simp only: UF.simps) |
|
446 apply(subst Steps_simulate[symmetric, OF assms]) |
|
447 apply(subst Final_simulate[symmetric]) |
|
448 apply(subst Std_simulate[symmetric]) |
|
449 apply(simp only: Halt.simps) |
|
450 apply(simp only: Steps_simulate[symmetric, OF assms]) |
|
451 apply(simp only: Stop.simps[symmetric]) |
|
452 done |
|
453 |
|
454 |
|
455 section {* Universal Function as Recursive Functions *} |
|
456 |
|
457 definition |
|
458 "rec_read = CN rec_ldec [Id 1 0, constn 0]" |
|
459 |
|
460 definition |
|
461 "rec_write = CN rec_penc [CN S [Id 2 0], CN rec_pdec2 [Id 2 1]]" |
|
462 |
|
463 definition |
|
464 "rec_newleft = |
|
465 (let cond0 = CN rec_eq [Id 3 2, constn 0] in |
|
466 let cond1 = CN rec_eq [Id 3 2, constn 1] in |
|
467 let cond2 = CN rec_eq [Id 3 2, constn 2] in |
|
468 let cond3 = CN rec_eq [Id 3 2, constn 3] in |
|
469 let case3 = CN rec_penc [CN S [CN rec_read [Id 3 1]], Id 3 0] in |
|
470 CN rec_if [cond0, Id 3 0, |
|
471 CN rec_if [cond1, Id 3 0, |
|
472 CN rec_if [cond2, CN rec_pdec2 [Id 3 0], |
|
473 CN rec_if [cond3, case3, Id 3 0]]]])" |
|
474 |
|
475 definition |
|
476 "rec_newright = |
|
477 (let cond0 = CN rec_eq [Id 3 2, constn 0] in |
|
478 let cond1 = CN rec_eq [Id 3 2, constn 1] in |
|
479 let cond2 = CN rec_eq [Id 3 2, constn 2] in |
|
480 let cond3 = CN rec_eq [Id 3 2, constn 3] in |
|
481 let case2 = CN rec_penc [CN S [CN rec_read [Id 3 0]], Id 3 1] in |
|
482 CN rec_if [cond0, CN rec_write [constn 0, Id 3 1], |
|
483 CN rec_if [cond1, CN rec_write [constn 1, Id 3 1], |
|
484 CN rec_if [cond2, case2, |
|
485 CN rec_if [cond3, CN rec_pdec2 [Id 3 1], Id 3 1]]]])" |
|
486 |
|
487 definition |
|
488 "rec_actn = rec_swap (PR (CN rec_pdec1 [CN rec_pdec1 [Id 1 0]]) |
|
489 (CN rec_pdec1 [CN rec_pdec2 [Id 3 2]]))" |
|
490 |
|
491 definition |
|
492 "rec_action = (let cond1 = CN rec_noteq [Id 3 1, Z] in |
|
493 let cond2 = CN rec_within [Id 3 0, CN rec_pred [Id 3 1]] in |
|
494 let if_branch = CN rec_actn [CN rec_ldec [Id 3 0, CN rec_pred [Id 3 1]], Id 3 2] |
|
495 in CN rec_if [CN rec_conj [cond1, cond2], if_branch, constn 4])" |
|
496 |
|
497 definition |
|
498 "rec_newstat = rec_swap (PR (CN rec_pdec2 [CN rec_pdec1 [Id 1 0]]) |
|
499 (CN rec_pdec2 [CN rec_pdec2 [Id 3 2]]))" |
|
500 |
|
501 definition |
|
502 "rec_newstate = (let cond = CN rec_noteq [Id 3 1, Z] in |
|
503 let if_branch = CN rec_newstat [CN rec_ldec [Id 3 0, CN rec_pred [Id 3 1]], Id 3 2] |
|
504 in CN rec_if [cond, if_branch, Z])" |
|
505 |
|
506 definition |
|
507 "rec_conf = rec_lenc [Id 3 0, Id 3 1, Id 3 2]" |
|
508 |
|
509 definition |
|
510 "rec_state = CN rec_ldec [Id 1 0, Z]" |
|
511 |
|
512 definition |
|
513 "rec_left = CN rec_ldec [Id 1 0, constn 1]" |
|
514 |
|
515 definition |
|
516 "rec_right = CN rec_ldec [Id 1 0, constn 2]" |
|
517 |
|
518 definition |
|
519 "rec_step = (let left = CN rec_left [Id 2 0] in |
|
520 let right = CN rec_right [Id 2 0] in |
|
521 let state = CN rec_state [Id 2 0] in |
|
522 let read = CN rec_read [right] in |
|
523 let action = CN rec_action [Id 2 1, state, read] in |
|
524 let newstate = CN rec_newstate [Id 2 1, state, read] in |
|
525 let newleft = CN rec_newleft [left, right, action] in |
|
526 let newright = CN rec_newright [left, right, action] |
|
527 in CN rec_conf [newstate, newleft, newright])" |
|
528 |
|
529 definition |
|
530 "rec_steps = PR (Id 2 0) (CN rec_step [Id 4 1, Id 4 3])" |
|
531 |
|
532 definition |
|
533 "rec_stknum = CN rec_minus |
|
534 [CN (rec_sigma1 (CN rec_ldec [Id 2 1, Id 2 0])) [CN rec_enclen [Id 1 0], Id 1 0], |
|
535 CN rec_ldec [Id 1 0, CN rec_enclen [Id 1 0]]]" |
|
536 |
|
537 definition |
|
538 "rec_right_std = (let bound = CN rec_enclen [Id 1 0] in |
|
539 let cond1 = CN rec_le [CN (constn 1) [Id 2 0], Id 2 0] in |
|
540 let cond2 = rec_all1_less (CN rec_eq [CN rec_ldec [Id 2 1, Id 2 0], constn 1]) in |
|
541 let bound2 = CN rec_minus [CN rec_enclen [Id 2 1], Id 2 0] in |
|
542 let cond3 = CN (rec_all2_less |
|
543 (CN rec_eq [CN rec_ldec [Id 3 2, CN rec_add [Id 3 1, Id 3 0]], Z])) |
|
544 [bound2, Id 2 0, Id 2 1] in |
|
545 CN (rec_ex1 (CN rec_conj [CN rec_conj [cond1, cond2], cond3])) [bound, Id 1 0])" |
|
546 |
|
547 definition |
|
548 "rec_left_std = (let cond = CN rec_eq [CN rec_ldec [Id 2 1, Id 2 0], Z] |
|
549 in CN (rec_all1_less cond) [CN rec_enclen [Id 1 0], Id 1 0])" |
|
550 |
|
551 definition |
|
552 "rec_std = CN rec_conj [CN rec_left_std [CN rec_left [Id 1 0]], |
|
553 CN rec_right_std [CN rec_right [Id 1 0]]]" |
|
554 |
|
555 definition |
|
556 "rec_final = CN rec_eq [CN rec_state [Id 1 0], Z]" |
|
557 |
|
558 definition |
|
559 "rec_stop = (let steps = CN rec_steps [Id 3 2, Id 3 1, Id 3 0] in |
|
560 CN rec_conj [CN rec_final [steps], CN rec_std [steps]])" |
|
561 |
|
562 definition |
|
563 "rec_halt = MN (CN rec_not [CN rec_stop [Id 3 1, Id 3 2, Id 3 0]])" |
|
564 |
|
565 definition |
|
566 "rec_uf = CN rec_pred |
|
567 [CN rec_stknum |
|
568 [CN rec_right |
|
569 [CN rec_steps [CN rec_halt [Id 2 0, Id 2 1], Id 2 1, Id 2 0]]]]" |
|
570 |
|
571 lemma read_lemma [simp]: |
|
572 "rec_eval rec_read [x] = Read x" |
|
573 by (simp add: rec_read_def) |
|
574 |
|
575 lemma write_lemma [simp]: |
|
576 "rec_eval rec_write [x, y] = Write x y" |
|
577 by (simp add: rec_write_def) |
|
578 |
|
579 lemma newleft_lemma [simp]: |
|
580 "rec_eval rec_newleft [p, r, a] = Newleft p r a" |
|
581 by (simp add: rec_newleft_def Let_def) |
|
582 |
|
583 lemma newright_lemma [simp]: |
|
584 "rec_eval rec_newright [p, r, a] = Newright p r a" |
|
585 by (simp add: rec_newright_def Let_def) |
|
586 |
|
587 lemma act_lemma [simp]: |
|
588 "rec_eval rec_actn [n, c] = Actn n c" |
|
589 apply(simp add: rec_actn_def) |
|
590 apply(case_tac c) |
|
591 apply(simp_all) |
|
592 done |
|
593 |
|
594 lemma action_lemma [simp]: |
|
595 "rec_eval rec_action [m, q, c] = Action m q c" |
|
596 by (simp add: rec_action_def) |
|
597 |
|
598 lemma newstat_lemma [simp]: |
|
599 "rec_eval rec_newstat [n, c] = Newstat n c" |
|
600 apply(simp add: rec_newstat_def) |
|
601 apply(case_tac c) |
|
602 apply(simp_all) |
|
603 done |
|
604 |
|
605 lemma newstate_lemma [simp]: |
|
606 "rec_eval rec_newstate [m, q, r] = Newstate m q r" |
|
607 by (simp add: rec_newstate_def) |
|
608 |
|
609 lemma conf_lemma [simp]: |
|
610 "rec_eval rec_conf [q, l, r] = Conf (q, l, r)" |
|
611 by(simp add: rec_conf_def) |
|
612 |
|
613 lemma state_lemma [simp]: |
|
614 "rec_eval rec_state [cf] = State cf" |
|
615 by (simp add: rec_state_def) |
|
616 |
|
617 lemma left_lemma [simp]: |
|
618 "rec_eval rec_left [cf] = Left cf" |
|
619 by (simp add: rec_left_def) |
|
620 |
|
621 lemma right_lemma [simp]: |
|
622 "rec_eval rec_right [cf] = Right cf" |
|
623 by (simp add: rec_right_def) |
|
624 |
|
625 lemma step_lemma [simp]: |
|
626 "rec_eval rec_step [cf, m] = Step cf m" |
|
627 by (simp add: Let_def rec_step_def) |
|
628 |
|
629 lemma steps_lemma [simp]: |
|
630 "rec_eval rec_steps [n, cf, p] = Steps cf p n" |
|
631 by (induct n) (simp_all add: rec_steps_def Step_Steps_comm del: Step.simps) |
|
632 |
|
633 lemma stknum_lemma [simp]: |
|
634 "rec_eval rec_stknum [z] = Stknum z" |
|
635 by (simp add: rec_stknum_def Stknum_def lessThan_Suc_atMost[symmetric]) |
|
636 |
|
637 lemma left_std_lemma [simp]: |
|
638 "rec_eval rec_left_std [z] = (if left_std z then 1 else 0)" |
|
639 by (simp add: Let_def rec_left_std_def left_std_def) |
|
640 |
|
641 lemma right_std_lemma [simp]: |
|
642 "rec_eval rec_right_std [z] = (if right_std z then 1 else 0)" |
|
643 by (simp add: Let_def rec_right_std_def right_std_def) |
|
644 |
|
645 lemma std_lemma [simp]: |
|
646 "rec_eval rec_std [cf] = (if Std cf then 1 else 0)" |
|
647 by (simp add: rec_std_def) |
|
648 |
|
649 lemma final_lemma [simp]: |
|
650 "rec_eval rec_final [cf] = (if Final cf then 1 else 0)" |
|
651 by (simp add: rec_final_def) |
|
652 |
|
653 lemma stop_lemma [simp]: |
|
654 "rec_eval rec_stop [m, cf, k] = (if Stop m cf k then 1 else 0)" |
|
655 by (simp add: Let_def rec_stop_def) |
|
656 |
|
657 lemma halt_lemma [simp]: |
|
658 "rec_eval rec_halt [m, cf] = Halt m cf" |
|
659 by (simp add: rec_halt_def del: Stop.simps) |
|
660 |
|
661 lemma uf_lemma [simp]: |
|
662 "rec_eval rec_uf [m, cf] = UF m cf" |
|
663 by (simp add: rec_uf_def) |
|
664 |
|
665 (* value "size rec_uf" *) |
|
666 end |
|
667 |