7 | id nat nat |
7 | id nat nat |
8 | Cn nat recf "recf list" |
8 | Cn nat recf "recf list" |
9 | Pr nat recf recf |
9 | Pr nat recf recf |
10 | Mn nat recf |
10 | Mn nat recf |
11 |
11 |
12 definition pred_of_nl :: "nat list \<Rightarrow> nat list" |
|
13 where |
|
14 "pred_of_nl xs = butlast xs @ [last xs - 1]" |
|
15 |
|
16 function rec_exec :: "recf \<Rightarrow> nat list \<Rightarrow> nat" |
12 function rec_exec :: "recf \<Rightarrow> nat list \<Rightarrow> nat" |
17 where |
13 where |
18 "rec_exec z xs = 0" | |
14 "rec_exec z xs = 0" | |
19 "rec_exec s xs = (Suc (xs ! 0))" | |
15 "rec_exec s xs = Suc (xs ! 0)" | |
20 "rec_exec (id m n) xs = (xs ! n)" | |
16 "rec_exec (id m n) xs = (xs ! n)" | |
21 "rec_exec (Cn n f gs) xs = |
17 "rec_exec (Cn n f gs) xs = |
22 rec_exec f (map (\<lambda> a. rec_exec a xs) gs)" | |
18 rec_exec f (map (\<lambda> a. rec_exec a xs) gs)" | |
23 "rec_exec (Pr n f g) xs = |
19 "rec_exec (Pr n f g) xs = |
24 (if last xs = 0 then rec_exec f (butlast xs) |
20 (if last xs = 0 then rec_exec f (butlast xs) |
29 termination |
25 termination |
30 apply(relation "measures [\<lambda> (r, xs). size r, (\<lambda> (r, xs). last xs)]") |
26 apply(relation "measures [\<lambda> (r, xs). size r, (\<lambda> (r, xs). last xs)]") |
31 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') |
32 done |
28 done |
33 |
29 |
34 inductive terminate :: "recf \<Rightarrow> nat list \<Rightarrow> bool" |
30 inductive |
35 where |
31 terminates :: "recf \<Rightarrow> nat list \<Rightarrow> bool" |
36 termi_z: "terminate z [n]" |
32 where |
37 | termi_s: "terminate s [n]" |
33 termi_z: "terminates z [n]" |
38 | termi_id: "\<lbrakk>n < m; length xs = m\<rbrakk> \<Longrightarrow> terminate (id m n) xs" |
34 | termi_s: "terminates s [n]" |
39 | termi_cn: "\<lbrakk>terminate f (map (\<lambda>g. rec_exec g xs) gs); |
35 | termi_id: "\<lbrakk>n < m; length xs = m\<rbrakk> \<Longrightarrow> terminates (id m n) xs" |
40 \<forall>g \<in> set gs. terminate g xs; length xs = n\<rbrakk> \<Longrightarrow> terminate (Cn n f gs) xs" |
36 | termi_cn: "\<lbrakk>terminates f (map (\<lambda>g. rec_exec g xs) gs); |
41 | termi_pr: "\<lbrakk>\<forall> y < x. terminate g (xs @ y # [rec_exec (Pr n f g) (xs @ [y])]); |
37 \<forall>g \<in> set gs. terminates g xs; length xs = n\<rbrakk> \<Longrightarrow> terminates (Cn n f gs) xs" |
42 terminate f xs; |
38 | termi_pr: "\<lbrakk>\<forall> y < x. terminates g (xs @ y # [rec_exec (Pr n f g) (xs @ [y])]); |
|
39 terminates f xs; |
43 length xs = n\<rbrakk> |
40 length xs = n\<rbrakk> |
44 \<Longrightarrow> terminate (Pr n f g) (xs @ [x])" |
41 \<Longrightarrow> terminates (Pr n f g) (xs @ [x])" |
45 | termi_mn: "\<lbrakk>length xs = n; terminate f (xs @ [r]); |
42 | termi_mn: "\<lbrakk>length xs = n; terminates f (xs @ [r]); |
46 rec_exec f (xs @ [r]) = 0; |
43 rec_exec f (xs @ [r]) = 0; |
47 \<forall> i < r. terminate f (xs @ [i]) \<and> rec_exec f (xs @ [i]) > 0\<rbrakk> \<Longrightarrow> terminate (Mn n f) xs" |
44 \<forall> i < r. terminates f (xs @ [i]) \<and> rec_exec f (xs @ [i]) > 0\<rbrakk> \<Longrightarrow> terminates (Mn n f) xs" |
48 |
45 |
49 |
46 |
50 inductive_cases terminate_pr_reverse: "terminate (Pr n f g) xs" |
47 inductive_cases terminates_pr_reverse: "terminates (Pr n f g) xs" |
51 |
48 |
52 inductive_cases terminate_z_reverse[elim!]: "terminate z xs" |
49 inductive_cases terminates_z_reverse[elim!]: "terminates z xs" |
53 |
50 |
54 inductive_cases terminate_s_reverse[elim!]: "terminate s xs" |
51 inductive_cases terminates_s_reverse[elim!]: "terminates s xs" |
55 |
52 |
56 inductive_cases terminate_id_reverse[elim!]: "terminate (id m n) xs" |
53 inductive_cases terminates_id_reverse[elim!]: "terminates (id m n) xs" |
57 |
54 |
58 inductive_cases terminate_cn_reverse[elim!]: "terminate (Cn n f gs) xs" |
55 inductive_cases terminates_cn_reverse[elim!]: "terminates (Cn n f gs) xs" |
59 |
56 |
60 inductive_cases terminate_mn_reverse[elim!]:"terminate (Mn n f) xs" |
57 inductive_cases terminates_mn_reverse[elim!]:"terminates (Mn n f) xs" |
61 |
58 |
62 end |
59 end |