90 arity of the recursive function @{text "recf"}, |
90 arity of the recursive function @{text "recf"}, |
91 @{text "fp"} is the amount of memory which is going to be |
91 @{text "fp"} is the amount of memory which is going to be |
92 used by @{text "ap"} for its execution. |
92 used by @{text "ap"} for its execution. |
93 *} |
93 *} |
94 |
94 |
95 function rec_ci :: "recf \<Rightarrow> abc_inst list \<times> nat \<times> nat" |
95 fun rec_ci :: "recf \<Rightarrow> abc_inst list \<times> nat \<times> nat" |
96 where |
96 where |
97 "rec_ci z = (rec_ci_z, 1, 2)" | |
97 "rec_ci z = (rec_ci_z, 1, 2)" | |
98 "rec_ci s = (rec_ci_s, 1, 3)" | |
98 "rec_ci s = (rec_ci_s, 1, 3)" | |
99 "rec_ci (id m n) = (rec_ci_id m n, m, m + 2)" | |
99 "rec_ci (id m n) = (rec_ci_id m n, m, m + 2)" | |
100 "rec_ci (Cn n f gs) = |
100 "rec_ci (Cn n f gs) = |
101 (let cied_gs = map (\<lambda> g. rec_ci g) (f # gs) in |
101 (let cied_gs = map (\<lambda> g. rec_ci g) gs in |
102 let (fprog, fpara, fn) = hd cied_gs in |
102 let (fprog, fpara, fn) = rec_ci f in |
103 let pstr = |
103 let pstr = Max (set (Suc n # fn # (map (\<lambda> (aprog, p, n). n) cied_gs))) in |
104 Max (set (Suc n # fn # (map (\<lambda> (aprog, p, n). n) cied_gs))) in |
|
105 let qstr = pstr + Suc (length gs) in |
104 let qstr = pstr + Suc (length gs) in |
106 (cn_merge_gs (tl cied_gs) pstr [+] mv_boxes 0 qstr n [+] |
105 (cn_merge_gs cied_gs pstr [+] mv_boxes 0 qstr n [+] |
107 mv_boxes pstr 0 (length gs) [+] fprog [+] |
106 mv_boxes pstr 0 (length gs) [+] fprog [+] |
108 mv_box fpara pstr [+] empty_boxes (length gs) [+] |
107 mv_box fpara pstr [+] empty_boxes (length gs) [+] |
109 mv_box pstr n [+] mv_boxes qstr 0 n, n, qstr + n))" | |
108 mv_box pstr n [+] mv_boxes qstr 0 n, n, qstr + n))" | |
110 "rec_ci (Pr n f g) = |
109 "rec_ci (Pr n f g) = |
111 (let (fprog, fpara, fn) = rec_ci f in |
110 (let (fprog, fpara, fn) = rec_ci f in |
120 "rec_ci (Mn n f) = |
119 "rec_ci (Mn n f) = |
121 (let (fprog, fpara, fn) = rec_ci f in |
120 (let (fprog, fpara, fn) = rec_ci f in |
122 let len = length (fprog) in |
121 let len = length (fprog) in |
123 (fprog @ [Dec (Suc n) (len + 5), Dec (Suc n) (len + 3), |
122 (fprog @ [Dec (Suc n) (len + 5), Dec (Suc n) (len + 3), |
124 Goto (len + 1), Inc n, Goto 0], n, max (Suc n) fn))" |
123 Goto (len + 1), Inc n, Goto 0], n, max (Suc n) fn))" |
125 by pat_completeness auto |
|
126 termination |
|
127 proof |
|
128 show "wf (measure size)" by auto |
|
129 next |
|
130 fix n f gs x |
|
131 assume "(x::recf) \<in> set (f # gs)" |
|
132 thus "(x, Cn n f gs) \<in> measure size" |
|
133 by(induct gs, auto) |
|
134 next |
|
135 fix n f g |
|
136 show "(f, Pr n f g) \<in> measure size" by auto |
|
137 next |
|
138 fix n f g x xa y xb ya |
|
139 show "(g, Pr n f g) \<in> measure size" by auto |
|
140 next |
|
141 fix n f |
|
142 show "(f, Mn n f) \<in> measure size" by auto |
|
143 qed |
|
144 |
124 |
145 declare rec_ci.simps [simp del] rec_ci_s_def[simp del] |
125 declare rec_ci.simps [simp del] rec_ci_s_def[simp del] |
146 rec_ci_z_def[simp del] rec_ci_id.simps[simp del] |
126 rec_ci_z_def[simp del] rec_ci_id.simps[simp del] |
147 mv_boxes.simps[simp del] abc_append.simps[simp del] |
127 mv_boxes.simps[simp del] abc_append.simps[simp del] |
148 mv_box.simps[simp del] addition.simps[simp del] |
128 mv_box.simps[simp del] addition.simps[simp del] |
321 "\<lbrakk>rec_calc_rel f l x; |
301 "\<lbrakk>rec_calc_rel f l x; |
322 rec_calc_rel f l y\<rbrakk> \<Longrightarrow> x = y" |
302 rec_calc_rel f l y\<rbrakk> \<Longrightarrow> x = y" |
323 apply(induct f arbitrary: l x y rule: rec_ci.induct) |
303 apply(induct f arbitrary: l x y rule: rec_ci.induct) |
324 apply(simp add: rec_calc_inj_case_z) |
304 apply(simp add: rec_calc_inj_case_z) |
325 apply(simp add: rec_calc_inj_case_s) |
305 apply(simp add: rec_calc_inj_case_s) |
326 apply(simp add: rec_calc_inj_case_id, simp) |
306 apply(simp add: rec_calc_inj_case_id) |
327 apply(erule rec_calc_inj_case_cn,simp, simp) |
307 apply (metis rec_calc_inj_case_cn) |
328 apply(erule rec_calc_inj_case_pr, auto) |
308 apply(erule rec_calc_inj_case_pr, auto) |
329 apply(erule rec_calc_inj_case_mn, auto) |
309 apply(erule rec_calc_inj_case_mn, auto) |
330 done |
310 done |
331 |
311 |
332 |
312 |