1 header {* |
|
2 {\em abacus} a kind of register machine |
|
3 *} |
|
4 |
|
5 theory Abacus |
1 theory Abacus |
6 imports Uncomputable |
2 imports Uncomputable |
7 begin |
3 begin |
8 |
4 |
9 (* |
|
10 declare tm_comp.simps [simp add] |
|
11 declare adjust.simps[simp add] |
|
12 declare shift.simps[simp add] |
|
13 declare tm_wf.simps[simp add] |
|
14 declare step.simps[simp add] |
|
15 declare steps.simps[simp add] |
|
16 *) |
|
17 declare replicate_Suc[simp add] |
5 declare replicate_Suc[simp add] |
18 |
6 |
19 text {* |
7 (* Abacus instructions *) |
20 {\em Abacus} instructions: |
|
21 *} |
|
22 |
8 |
23 datatype abc_inst = |
9 datatype abc_inst = |
24 -- {* @{text "Inc n"} increments the memory cell (or register) with address @{text "n"} by one. |
|
25 *} |
|
26 Inc nat |
10 Inc nat |
27 -- {* |
|
28 @{text "Dec n label"} decrements the memory cell with address @{text "n"} by one. |
|
29 If cell @{text "n"} is already zero, no decrements happens and the executio jumps to |
|
30 the instruction labeled by @{text "label"}. |
|
31 *} |
|
32 | Dec nat nat |
11 | Dec nat nat |
33 -- {* |
|
34 @{text "Goto label"} unconditionally jumps to the instruction labeled by @{text "label"}. |
|
35 *} |
|
36 | Goto nat |
12 | Goto nat |
37 |
13 |
38 |
|
39 text {* |
|
40 Abacus programs are defined as lists of Abacus instructions. |
|
41 *} |
|
42 type_synonym abc_prog = "abc_inst list" |
14 type_synonym abc_prog = "abc_inst list" |
43 |
15 |
44 section {* |
16 section {* Some Sample Abacus programs *} |
45 Sample Abacus programs |
17 |
46 *} |
18 (* Abacus for addition and clearance *) |
47 |
|
48 text {* |
|
49 Abacus for addition and clearance. |
|
50 *} |
|
51 fun plus_clear :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> abc_prog" |
19 fun plus_clear :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> abc_prog" |
52 where |
20 where |
53 "plus_clear m n e = [Dec m e, Inc n, Goto 0]" |
21 "plus_clear m n e = [Dec m e, Inc n, Goto 0]" |
54 |
22 |
55 text {* |
23 (* Abacus for clearing memory untis *) |
56 Abacus for clearing memory untis. |
|
57 *} |
|
58 fun clear :: "nat \<Rightarrow> nat \<Rightarrow> abc_prog" |
24 fun clear :: "nat \<Rightarrow> nat \<Rightarrow> abc_prog" |
59 where |
25 where |
60 "clear n e = [Dec n e, Goto 0]" |
26 "clear n e = [Dec n e, Goto 0]" |
61 |
27 |
62 fun plus:: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> abc_prog" |
28 fun plus:: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> abc_prog" |
70 |
36 |
71 fun expo :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> abc_prog" |
37 fun expo :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> abc_prog" |
72 where |
38 where |
73 "expo n m1 m2 p e = [Inc n, Dec m1 e] @ mult m2 n n p 2" |
39 "expo n m1 m2 p e = [Inc n, Dec m1 e] @ mult m2 n n p 2" |
74 |
40 |
75 |
|
76 text {* |
|
77 The state of Abacus machine. |
|
78 *} |
|
79 type_synonym abc_state = nat |
41 type_synonym abc_state = nat |
80 |
|
81 (* text {* |
|
82 The memory of Abacus machine is defined as a function from address to contents. |
|
83 *} |
|
84 type_synonym abc_mem = "nat \<Rightarrow> nat" *) |
|
85 |
42 |
86 text {* |
43 text {* |
87 The memory of Abacus machine is defined as a list of contents, with |
44 The memory of Abacus machine is defined as a list of contents, with |
88 every units addressed by index into the list. |
45 every units addressed by index into the list. |
89 *} |
46 *} |
310 @{text "tm_of ap"} returns the final TM machine compiled from Abacus program @{text "ap"}. |
267 @{text "tm_of ap"} returns the final TM machine compiled from Abacus program @{text "ap"}. |
311 *} |
268 *} |
312 fun tm_of :: "abc_prog \<Rightarrow> instr list" |
269 fun tm_of :: "abc_prog \<Rightarrow> instr list" |
313 where "tm_of ap = concat (tms_of ap)" |
270 where "tm_of ap = concat (tms_of ap)" |
314 |
271 |
315 text {* |
|
316 The following two functions specify the well-formedness of complied TM. |
|
317 *} |
|
318 (* |
|
319 fun t_ncorrect :: "tprog \<Rightarrow> bool" |
|
320 where |
|
321 "t_ncorrect tp = (length tp mod 2 = 0)" |
|
322 |
|
323 fun abc2t_correct :: "abc_prog \<Rightarrow> bool" |
|
324 where |
|
325 "abc2t_correct ap = list_all (\<lambda> (n, tm). |
|
326 t_ncorrect (ci (layout_of ap) n tm)) (tpairs_of ap)" |
|
327 *) |
|
328 |
|
329 lemma length_findnth: |
272 lemma length_findnth: |
330 "length (findnth n) = 4 * n" |
273 "length (findnth n) = 4 * n" |
331 apply(induct n, auto) |
274 by (induct n, auto) |
332 done |
|
333 |
275 |
334 lemma ci_length : "length (ci ns n ai) div 2 = length_of ai" |
276 lemma ci_length : "length (ci ns n ai) div 2 = length_of ai" |
335 apply(auto simp: ci.simps tinc_b_def tdec_b_def length_findnth |
277 apply(auto simp: ci.simps tinc_b_def tdec_b_def length_findnth |
336 split: abc_inst.splits) |
278 split: abc_inst.splits) |
337 done |
279 done |
338 |
280 |
339 subsection {* |
281 subsection {* Representation of Abacus memory by TM tapes *} |
340 Representation of Abacus memory by TM tape |
|
341 *} |
|
342 |
282 |
343 text {* |
283 text {* |
344 @{text "crsp acf tcf"} meams the abacus configuration @{text "acf"} |
284 @{text "crsp acf tcf"} meams the abacus configuration @{text "acf"} |
345 is corretly represented by the TM configuration @{text "tcf"}. |
285 is corretly represented by the TM configuration @{text "tcf"}. |
346 *} |
286 *} |
351 (s = start_of ly as \<and> (\<exists> x. r = <lm> @ Bk\<up>x) \<and> |
291 (s = start_of ly as \<and> (\<exists> x. r = <lm> @ Bk\<up>x) \<and> |
352 l = Bk # Bk # inres)" |
292 l = Bk # Bk # inres)" |
353 |
293 |
354 declare crsp.simps[simp del] |
294 declare crsp.simps[simp del] |
355 |
295 |
356 subsection {* |
|
357 A more general definition of TM execution. |
|
358 *} |
|
359 |
|
360 (* |
|
361 fun nnth_of :: "(taction \<times> nat) list \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> (taction \<times> nat)" |
|
362 where |
|
363 "nnth_of p s b = (if 2*s < length p |
|
364 then (p ! (2*s + b)) else (Nop, 0))" |
|
365 |
|
366 thm nth_of.simps |
|
367 |
|
368 fun nfetch :: "tprog \<Rightarrow> nat \<Rightarrow> block \<Rightarrow> taction \<times> nat" |
|
369 where |
|
370 "nfetch p 0 b = (Nop, 0)" | |
|
371 "nfetch p (Suc s) b = |
|
372 (case b of |
|
373 Bk \<Rightarrow> nnth_of p s 0 | |
|
374 Oc \<Rightarrow> nnth_of p s 1)" |
|
375 *) |
|
376 |
|
377 |
|
378 text {* |
296 text {* |
379 The type of invarints expressing correspondence between |
297 The type of invarints expressing correspondence between |
380 Abacus configuration and TM configuration. |
298 Abacus configuration and TM configuration. |
381 *} |
299 *} |
382 |
300 |
385 declare tms_of.simps[simp del] tm_of.simps[simp del] |
303 declare tms_of.simps[simp del] tm_of.simps[simp del] |
386 layout_of.simps[simp del] abc_fetch.simps [simp del] |
304 layout_of.simps[simp del] abc_fetch.simps [simp del] |
387 tpairs_of.simps[simp del] start_of.simps[simp del] |
305 tpairs_of.simps[simp del] start_of.simps[simp del] |
388 ci.simps [simp del] length_of.simps[simp del] |
306 ci.simps [simp del] length_of.simps[simp del] |
389 layout_of.simps[simp del] |
307 layout_of.simps[simp del] |
390 |
|
391 (* |
|
392 subsection {* The compilation of @{text "Inc n"} *} |
|
393 *) |
|
394 |
308 |
395 text {* |
309 text {* |
396 The lemmas in this section lead to the correctness of |
310 The lemmas in this section lead to the correctness of |
397 the compilation of @{text "Inc n"} instruction. |
311 the compilation of @{text "Inc n"} instruction. |
398 *} |
312 *} |
2325 ml = 1 \<and> tn = s + 1 - length lm \<and> |
2239 ml = 1 \<and> tn = s + 1 - length lm \<and> |
2326 (if lm1 = [] then l = Oc\<up>ml @ Bk # Bk # ires |
2240 (if lm1 = [] then l = Oc\<up>ml @ Bk # Bk # ires |
2327 else l = Oc\<up>ml @ Bk # <rev lm1> @ Bk # Bk # ires) \<and> |
2241 else l = Oc\<up>ml @ Bk # <rev lm1> @ Bk # Bk # ires) \<and> |
2328 (r = Oc\<up>mr @ [Bk] @ <lm2>@ Bk\<up>rn \<or> (lm2 = [] \<and> r = Oc\<up>mr)) |
2242 (r = Oc\<up>mr @ [Bk] @ <lm2>@ Bk\<up>rn \<or> (lm2 = [] \<and> r = Oc\<up>mr)) |
2329 )" |
2243 )" |
2330 (* |
|
2331 fun dec_inv_1 :: "layout \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> dec_inv_t" |
|
2332 where |
|
2333 "dec_inv_1 ly n e (as, am) (s, l, r) ires = |
|
2334 (let ss = start_of ly as in |
|
2335 let am' = abc_lm_s am n (abc_lm_v am n - Suc 0) in |
|
2336 let am'' = abc_lm_s am n (abc_lm_v am n) in |
|
2337 if s = start_of ly e then inv_stop (as, am'') (s, l, r) ires |
|
2338 else if s = ss then False |
|
2339 else if s = ss + 2 * n then |
|
2340 inv_locate_a (as, am) (n, l, r) ires |
|
2341 \<or> inv_locate_a (as, am'') (n, l, r) ires |
|
2342 else if s = ss + 2 * n + 1 then |
|
2343 inv_locate_b (as, am) (n, l, r) ires |
|
2344 else if s = ss + 2 * n + 13 then |
|
2345 inv_on_left_moving (as, am'') (s, l, r) ires |
|
2346 else if s = ss + 2 * n + 14 then |
|
2347 inv_check_left_moving (as, am'') (s, l, r) ires |
|
2348 else if s = ss + 2 * n + 15 then |
|
2349 inv_after_left_moving (as, am'') (s, l, r) ires |
|
2350 else False)" |
|
2351 *) |
|
2352 |
|
2353 |
2244 |
2354 fun dec_inv_1 :: "layout \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> dec_inv_t" |
2245 fun dec_inv_1 :: "layout \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> dec_inv_t" |
2355 where |
2246 where |
2356 "dec_inv_1 ly n e (as, am) (s, l, r) ires = |
2247 "dec_inv_1 ly n e (as, am) (s, l, r) ires = |
2357 (let ss = start_of ly as in |
2248 (let ss = start_of ly as in |
2830 |
2721 |
2831 lemma [simp]: "inv_locate_b (as, lm) (n, [], Bk # list) ires = False" |
2722 lemma [simp]: "inv_locate_b (as, lm) (n, [], Bk # list) ires = False" |
2832 apply(auto simp: inv_locate_b.simps in_middle.simps split: if_splits) |
2723 apply(auto simp: inv_locate_b.simps in_middle.simps split: if_splits) |
2833 done |
2724 done |
2834 |
2725 |
2835 (* |
|
2836 |
|
2837 lemma inv_locate_b_2_on_left_moving_b[simp]: |
|
2838 "inv_locate_b (as, am) (n, l, []) ires |
|
2839 \<Longrightarrow> inv_on_left_moving (as, |
|
2840 abc_lm_s am n (abc_lm_v am n)) (s, [], [Bk]) ires" |
|
2841 apply(auto simp: inv_locate_b.simps inv_on_left_moving.simps inv_on_left_moving_in_middle_B.simps |
|
2842 in_middle.simps split: if_splits) |
|
2843 apply(drule_tac length_equal, simp) |
|
2844 |
|
2845 apply(insert inv_locate_b_2_on_left_moving[of as am n l "[]" ires s]) |
|
2846 apply(simp only: inv_on_left_moving.simps, simp) |
|
2847 apply(subgoal_tac "\<not> inv_on_left_moving_in_middle_B |
|
2848 (as, abc_lm_s am n (abc_lm_v am n)) (s, tl l, [hd l]) ires", simp) |
|
2849 *) |
|
2850 |
|
2851 (* |
|
2852 lemma [simp]: |
|
2853 "inv_locate_b (as, am) (n, l, []) ires; l \<noteq> []\<rbrakk> |
|
2854 \<Longrightarrow> inv_on_left_moving (as, abc_lm_s am n |
|
2855 (abc_lm_v am n)) (s, tl l, [hd l]) ires" |
|
2856 apply(auto simp: inv_locate_b.simps inv_on_left_moving.simps inv_on_left_moving_in_middle_B.simps |
|
2857 in_middle.simps split: if_splits) |
|
2858 apply(drule_tac length_equal, simp) |
|
2859 |
|
2860 apply(insert inv_locate_b_2_on_left_moving[of as am n l "[]" ires s]) |
|
2861 apply(simp only: inv_on_left_moving.simps, simp) |
|
2862 apply(subgoal_tac "\<not> inv_on_left_moving_in_middle_B |
|
2863 (as, abc_lm_s am n (abc_lm_v am n)) (s, tl l, [hd l]) ires", simp) |
|
2864 |
|
2865 apply(insert inv_locate_b_2_on_left_moving[of as am n l "[]" ires s]) |
|
2866 apply(simp only: inv_on_left_moving.simps, simp) |
|
2867 apply(subgoal_tac "\<not> inv_on_left_moving_in_middle_B |
|
2868 (as, abc_lm_s am n (abc_lm_v am n)) (s, tl l, [hd l]) ires", simp) |
|
2869 apply(simp only: inv_on_left_moving_norm.simps) |
|
2870 apply(erule_tac exE)+ |
|
2871 apply(erule_tac conjE)+ |
|
2872 apply(rule_tac x = lm1 in exI, rule_tac x = lm2 in exI, |
|
2873 rule_tac x = m in exI, rule_tac x = ml in exI, |
|
2874 rule_tac x = mr in exI, simp) |
|
2875 apply(case_tac mr, simp, simp, case_tac nat, auto intro: nil_2_nil) |
|
2876 done |
|
2877 *) |
|
2878 |
|
2879 lemma [simp]: |
2726 lemma [simp]: |
2880 "\<lbrakk>dec_first_on_right_moving n (as, am) (s, aaa, Oc # xs) ires\<rbrakk> |
2727 "\<lbrakk>dec_first_on_right_moving n (as, am) (s, aaa, Oc # xs) ires\<rbrakk> |
2881 \<Longrightarrow> dec_first_on_right_moving n (as, am) (s', Oc # aaa, xs) ires" |
2728 \<Longrightarrow> dec_first_on_right_moving n (as, am) (s', Oc # aaa, xs) ires" |
2882 apply(simp only: dec_first_on_right_moving.simps) |
2729 apply(simp only: dec_first_on_right_moving.simps) |
2883 apply(erule exE)+ |
2730 apply(erule exE)+ |
3048 |
2895 |
3049 lemma [simp]: "dec_left_move (as, am) (s, l, Bk # r) ires |
2896 lemma [simp]: "dec_left_move (as, am) (s, l, Bk # r) ires |
3050 \<Longrightarrow> inv_on_left_moving (as, am) (s', tl l, hd l # Bk # r) ires" |
2897 \<Longrightarrow> inv_on_left_moving (as, am) (s', tl l, hd l # Bk # r) ires" |
3051 apply(auto simp: dec_left_move.simps inv_on_left_moving.simps split: if_splits) |
2898 apply(auto simp: dec_left_move.simps inv_on_left_moving.simps split: if_splits) |
3052 done |
2899 done |
3053 |
|
3054 (* |
|
3055 lemma [simp]: "inv_on_left_moving_in_middle_B (as, lm1 @ [m]) |
|
3056 (s', Oc # Oc\<^bsup>m\<^esup> @ Bk # <rev lm1> @ Bk\<^bsup>ln\<^esup>, [Bk]) ires" |
|
3057 apply(auto simp: inv_on_left_moving_in_middle_B.simps) |
|
3058 apply(rule_tac x = "lm1 @ [m]" in exI, rule_tac x = "[]" in exI, auto) |
|
3059 done |
|
3060 *) |
|
3061 |
2900 |
3062 lemma [simp]: "dec_left_move (as, am) (s, l, []) ires |
2901 lemma [simp]: "dec_left_move (as, am) (s, l, []) ires |
3063 \<Longrightarrow> inv_on_left_moving (as, am) (s', tl l, [hd l]) ires" |
2902 \<Longrightarrow> inv_on_left_moving (as, am) (s', tl l, [hd l]) ires" |
3064 apply(auto simp: dec_left_move.simps inv_on_left_moving.simps split: if_splits) |
2903 apply(auto simp: dec_left_move.simps inv_on_left_moving.simps split: if_splits) |
3065 done |
2904 done |
3846 assumes layout: "ly = layout_of ap" |
3685 assumes layout: "ly = layout_of ap" |
3847 and compile: "tp = tm_of ap" |
3686 and compile: "tp = tm_of ap" |
3848 and crsp: "crsp ly (as, lm) (s, l, r) ires" |
3687 and crsp: "crsp ly (as, lm) (s, l, r) ires" |
3849 shows "\<exists> stp. crsp ly (abc_steps_l (as, lm) ap n) |
3688 shows "\<exists> stp. crsp ly (abc_steps_l (as, lm) ap n) |
3850 (steps (s, l, r) (tp, 0) stp) ires" |
3689 (steps (s, l, r) (tp, 0) stp) ires" |
3851 (* |
|
3852 proof(induct n) |
|
3853 case 0 |
|
3854 have "crsp ly (abc_steps_l (as, lm) ap 0) (steps (s, l, r) (tp, 0) 0) ires" |
|
3855 using crsp by(simp add: steps.simps abc_steps_l.simps) |
|
3856 thus "?case" |
|
3857 by(rule_tac x = 0 in exI, simp) |
|
3858 next |
|
3859 case (Suc n) |
|
3860 obtain as' lm' where a: "abc_steps_l (as, lm) ap n = (as', lm')" |
|
3861 by(case_tac "abc_steps_l (as, lm) ap n", auto) |
|
3862 have "\<exists>stp\<ge>n. crsp ly (abc_steps_l (as, lm) ap n) (steps (s, l, r) (tp, 0) stp) ires" |
|
3863 by fact |
|
3864 from this a obtain stpa where b: |
|
3865 "stpa\<ge>n \<and> crsp ly (as', lm') (steps (s, l, r) (tp, 0) stpa) ires" by auto |
|
3866 obtain s' l' r' where "steps (s, l, r) (tp, 0) stpa = (s', l', r')" |
|
3867 by(case_tac "steps (s, l, r) (tp, 0) stpa") |
|
3868 then have "stpa\<ge>n \<and> crsp ly (as', lm') (s', l', r') ires" using b by simp |
|
3869 from a and this show "?case" |
|
3870 proof(cases "abc_fetch as' ap") |
|
3871 case None |
|
3872 |
|
3873 |
|
3874 |
|
3875 have "crsp ly (abc_steps_l (as, lm) ap 0) (steps (s, l, r) (tp, 0) stp) ires" |
|
3876 apply(simp add: steps.simps abc_steps_l.simps) |
|
3877 *) |
|
3878 using crsp |
3690 using crsp |
3879 apply(induct n) |
3691 apply(induct n) |
3880 apply(rule_tac x = 0 in exI) |
3692 apply(rule_tac x = 0 in exI) |
3881 apply(simp add: steps.simps abc_steps_l.simps, simp) |
3693 apply(simp add: steps.simps abc_steps_l.simps, simp) |
3882 apply(case_tac "(abc_steps_l (as, lm) ap n)", auto) |
3694 apply(case_tac "(abc_steps_l (as, lm) ap n)", auto) |
3968 fetch (tp @ [(Nop, 0), (Nop, 0)]) (start_of ly (length ap)) b = |
3780 fetch (tp @ [(Nop, 0), (Nop, 0)]) (start_of ly (length ap)) b = |
3969 (Nop, 0)" |
3781 (Nop, 0)" |
3970 apply(case_tac b) |
3782 apply(case_tac b) |
3971 apply(simp_all add: start_of.simps fetch.simps nth_append) |
3783 apply(simp_all add: start_of.simps fetch.simps nth_append) |
3972 done |
3784 done |
3973 (* |
3785 |
3974 lemma tp_correct: |
|
3975 assumes layout: "ly = layout_of ap" |
|
3976 and compile: "tp = tm_of ap" |
|
3977 and crsp: "crsp ly (0, lm) (Suc 0, l, r) ires" |
|
3978 and abc_halt: "abc_steps_l (0, lm) ap stp = (length ap, am)" |
|
3979 shows "\<exists> stp k. steps (Suc 0, l, r) (tp @ [(Nop, 0), (Nop, 0)], 0) stp = (0, Bk # Bk # ires, <am> @ Bk\<up>k)" |
|
3980 using assms |
|
3981 proof - |
|
3982 have "\<exists> stp k. steps (Suc 0, l, r) (tp @ [(Nop, 0), (Nop, 0)], 0) stp = |
|
3983 (start_of ly (length ap), Bk # Bk # ires, <am> @ Bk\<up>k)" |
|
3984 proof - |
|
3985 have "\<exists> stp k. steps (Suc 0, l, r) (tp, 0) stp = |
|
3986 (start_of ly (length ap), Bk # Bk # ires, <am> @ Bk\<up>k)" |
|
3987 using assms |
|
3988 apply(rule_tac tp_correct', simp_all) |
|
3989 done |
|
3990 from this obtain stp k where "steps (Suc 0, l, r) (tp, 0) stp = |
|
3991 (start_of ly (length ap), Bk # Bk # ires, <am> @ Bk\<up>k)" by blast |
|
3992 thus "?thesis" |
|
3993 apply(rule_tac x = stp in exI, rule_tac x = k in exI) |
|
3994 apply(drule_tac tm_append_first_steps_eq, simp_all) |
|
3995 done |
|
3996 qed |
|
3997 from this obtain stp k where |
|
3998 "steps (Suc 0, l, r) (tp @ [(Nop, 0), (Nop, 0)], 0) stp = |
|
3999 (start_of ly (length ap), Bk # Bk # ires, <am> @ Bk\<up>k)" |
|
4000 by blast |
|
4001 thus "\<exists>stp k. steps (Suc 0, l, r) (tp @ [(Nop, 0), (Nop, 0)], 0) stp |
|
4002 = (0, Bk # Bk # ires, <am> @ Bk \<up> k)" |
|
4003 using assms |
|
4004 apply(rule_tac x = "stp + Suc 0" in exI) |
|
4005 apply(simp add: steps_add) |
|
4006 apply(auto simp: step.simps) |
|
4007 done |
|
4008 qed |
|
4009 *) |
|
4010 (********for mopup***********) |
3786 (********for mopup***********) |
4011 fun mopup_a :: "nat \<Rightarrow> instr list" |
3787 fun mopup_a :: "nat \<Rightarrow> instr list" |
4012 where |
3788 where |
4013 "mopup_a 0 = []" | |
3789 "mopup_a 0 = []" | |
4014 "mopup_a (Suc n) = mopup_a n @ |
3790 "mopup_a (Suc n) = mopup_a n @ |