13 where |
13 where |
14 "rec_exec z xs = 0" | |
14 "rec_exec z xs = 0" | |
15 "rec_exec s xs = (Suc (xs ! 0))" | |
15 "rec_exec s xs = (Suc (xs ! 0))" | |
16 "rec_exec (id m n) xs = (xs ! n)" | |
16 "rec_exec (id m n) xs = (xs ! n)" | |
17 "rec_exec (Cn n f gs) xs = |
17 "rec_exec (Cn n f gs) xs = |
18 (let ys = (map (\<lambda> a. rec_exec a xs) gs) in |
18 rec_exec f (map (\<lambda> a. rec_exec a xs) gs)" | |
19 rec_exec f ys)" | |
|
20 "rec_exec (Pr n f g) xs = |
19 "rec_exec (Pr n f g) xs = |
21 (if hd xs = 0 then |
20 (if hd xs = 0 then rec_exec f (tl xs) |
22 rec_exec f (tl xs) |
21 else rec_exec g ((hd xs - 1) # (rec_exec (Pr n f g) ((hd xs - 1) # tl xs)) # tl xs))" | |
23 else rec_exec g ((hd xs - 1) # tl xs @ [rec_exec (Pr n f g) ((hd xs - 1) # tl xs)]))" | |
|
24 "rec_exec (Mn n f) xs = (LEAST x. rec_exec f (x # xs) = 0)" |
22 "rec_exec (Mn n f) xs = (LEAST x. rec_exec f (x # xs) = 0)" |
25 by pat_completeness auto |
23 by pat_completeness auto |
26 |
24 |
27 termination |
25 termination |
28 apply(relation "measures [\<lambda> (r, xs). size r, (\<lambda> (r, xs). hd xs)]") |
26 apply(relation "measures [\<lambda> (r, xs). size r, (\<lambda> (r, xs). hd xs)]") |
29 apply(auto simp add: less_Suc_eq_le intro: trans_le_add2 list_size_estimation') |
27 apply(auto simp add: less_Suc_eq_le intro: trans_le_add2 list_size_estimation') |
30 done |
28 done |
31 |
|
32 |
29 |
33 inductive terminate :: "recf \<Rightarrow> nat list \<Rightarrow> bool" |
30 inductive terminate :: "recf \<Rightarrow> nat list \<Rightarrow> bool" |
34 where |
31 where |
35 termi_z: "terminate z [n]" |
32 termi_z: "terminate z [n]" |
36 | termi_s: "terminate s [n]" |
33 | termi_s: "terminate s [n]" |
37 | termi_id: "\<lbrakk>n < m; length xs = m\<rbrakk> \<Longrightarrow> terminate (id m n) xs" |
34 | termi_id: "\<lbrakk>n < m; length xs = m\<rbrakk> \<Longrightarrow> terminate (id m n) xs" |
38 | termi_cn: "\<lbrakk>terminate f (map (\<lambda>g. rec_exec g xs) gs); |
35 | termi_cn: "\<lbrakk>terminate f (map (\<lambda>g. rec_exec g xs) gs); |
39 \<forall>g \<in> set gs. terminate g xs; length xs = n\<rbrakk> \<Longrightarrow> terminate (Cn n f gs) xs" |
36 \<forall>g \<in> set gs. terminate g xs; length xs = n\<rbrakk> \<Longrightarrow> terminate (Cn n f gs) xs" |
40 | termi_pr_0: "\<lbrakk>terminate f xs; length xs = n\<rbrakk> \<Longrightarrow> terminate (Pr n f g) (0 # xs)" |
37 | termi_pr_0: "\<lbrakk>terminate f xs; length xs = n\<rbrakk> \<Longrightarrow> terminate (Pr n f g) (0 # xs)" |
41 | termi_pr_suc: "\<lbrakk>terminate (Pr n f gs) (x # xs); |
38 | termi_pr_suc: "\<lbrakk>terminate g (x # rec_exec (Pr n f gs) (x # xs) # xs)\<rbrakk> |
42 terminate g (x # rec_exec (Pr n f gs) (x # xs) # xs)\<rbrakk> |
|
43 \<Longrightarrow> terminate (Pr n f gs) (Suc x # xs)" |
39 \<Longrightarrow> terminate (Pr n f gs) (Suc x # xs)" |
44 | termi_mn: "\<lbrakk>length xs = n; rec_exec f (r # xs) = 0; |
40 | termi_mn: "\<lbrakk>length xs = n; rec_exec f (r # xs) = 0; |
45 \<forall> i < r. terminate f (i # xs) \<and> rec_exec f (i # xs) > 0\<rbrakk> \<Longrightarrow> terminate (Mn n f) xs" |
41 \<forall> i < r. terminate f (i # xs) \<and> rec_exec f (i # xs) > 0\<rbrakk> \<Longrightarrow> terminate (Mn n f) xs" |
46 |
42 |
47 end |
43 end |