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