1 (* Title: thys/Rec_Def.thy |
|
2 Author: Jian Xu, Xingyuan Zhang, and Christian Urban |
|
3 *) |
|
4 |
|
5 header {* Definition of Recursive Functions *} |
|
6 |
|
7 |
|
8 theory Rec_Def |
1 theory Rec_Def |
9 imports Main |
2 imports Main |
10 begin |
3 begin |
11 |
4 |
12 section {* Recursive functions *} |
5 datatype recf = z |
|
6 | s |
|
7 | id nat nat |
|
8 | Cn nat recf "recf list" |
|
9 | Pr nat recf recf |
|
10 | Mn nat recf |
13 |
11 |
14 datatype recf = |
12 definition pred_of_nl :: "nat list \<Rightarrow> nat list" |
15 z | s | |
13 where |
16 -- {* The projection function, where @{text "id i j"} returns the @{text "j"}-th |
14 "pred_of_nl xs = butlast xs @ [last xs - 1]" |
17 argment out of the @{text "i"} arguments. *} |
|
18 id nat nat | |
|
19 -- {* The compostion operator, where "@{text "Cn n f [g1; g2; \<dots> ;gm]"} |
|
20 computes @{text "f (g1(x1, x2, \<dots>, xn), g2(x1, x2, \<dots>, xn), \<dots> , |
|
21 gm(x1, x2, \<dots> , xn))"} for input argments @{text "x1, \<dots>, xn"}. *} |
|
22 Cn nat recf "recf list" | |
|
23 -- {* The primitive resursive operator, where @{text "Pr n f g"} computes: |
|
24 @{text "Pr n f g (x1, x2, \<dots>, xn-1, 0) = f(x1, \<dots>, xn-1)"} |
|
25 and @{text "Pr n f g (x1, x2, \<dots>, xn-1, k') = g(x1, x2, \<dots>, xn-1, k, |
|
26 Pr n f g (x1, \<dots>, xn-1, k))"}. |
|
27 *} |
|
28 Pr nat recf recf | |
|
29 -- {* The minimization operator, where @{text "Mn n f (x1, x2, \<dots> , xn)"} |
|
30 computes the first i such that @{text "f (x1, \<dots>, xn, i) = 0"} and for all |
|
31 @{text "j"}, @{text "f (x1, x2, \<dots>, xn, j) > 0"}. *} |
|
32 Mn nat recf |
|
33 |
15 |
34 (* |
16 function rec_exec :: "recf \<Rightarrow> nat list \<Rightarrow> nat" |
35 partial_function (tailrec) |
17 where |
36 rec_exec :: "recf \<Rightarrow> nat list \<Rightarrow> nat" |
18 "rec_exec z xs = 0" | |
37 where |
19 "rec_exec s xs = (Suc (xs ! 0))" | |
38 "rec_exec f ns = (case (f, ns) of |
20 "rec_exec (id m n) xs = (xs ! n)" | |
39 (z, xs) => 0 |
21 "rec_exec (Cn n f gs) xs = |
40 | (s, xs) => Suc (xs ! 0) |
22 rec_exec f (map (\<lambda> a. rec_exec a xs) gs)" | |
41 | (id m n, xs) => (xs ! n) |
23 "rec_exec (Pr n f g) xs = |
42 | (Cn n f gs, xs) => |
24 (if last xs = 0 then rec_exec f (butlast xs) |
43 (let ys = (map (\<lambda> a. rec_exec a xs) gs) in |
25 else rec_exec g (butlast xs @ (last xs - 1) # [rec_exec (Pr n f g) (butlast xs @ [last xs - 1])]))" | |
44 rec_exec f ys) |
26 "rec_exec (Mn n f) xs = (LEAST x. rec_exec f (xs @ [x]) = 0)" |
45 | (Pr n f g, xs) => |
27 by pat_completeness auto |
46 (if last xs = 0 then rec_exec f (butlast xs) |
|
47 else rec_exec g (butlast xs @ [last xs - 1] @ |
|
48 [rec_exec (Pr n f g) (butlast xs @ [last xs - 1])])) |
|
49 | (Mn n f, xs) => (LEAST x. rec_exec f (xs @ [x]) = 0))" |
|
50 *) |
|
51 |
28 |
52 text {* |
29 termination |
53 The semantis of recursive operators is given by an inductively defined |
30 apply(relation "measures [\<lambda> (r, xs). size r, (\<lambda> (r, xs). last xs)]") |
54 relation as follows, where |
31 apply(auto simp add: less_Suc_eq_le intro: trans_le_add2 list_size_estimation') |
55 @{text "rec_calc_rel R [x1, x2, \<dots>, xn] r"} means the computation of |
32 done |
56 @{text "R"} over input arguments @{text "[x1, x2, \<dots>, xn"} terminates |
|
57 and gives rise to a result @{text "r"} |
|
58 *} |
|
59 |
33 |
60 inductive rec_calc_rel :: "recf \<Rightarrow> nat list \<Rightarrow> nat \<Rightarrow> bool" |
34 inductive terminate :: "recf \<Rightarrow> nat list \<Rightarrow> bool" |
61 where |
35 where |
62 calc_z: "rec_calc_rel z [n] 0" | |
36 termi_z: "terminate z [n]" |
63 calc_s: "rec_calc_rel s [n] (Suc n)" | |
37 | termi_s: "terminate s [n]" |
64 calc_id: "\<lbrakk>length args = i; j < i; args!j = r\<rbrakk> \<Longrightarrow> rec_calc_rel (id i j) args r" | |
38 | termi_id: "\<lbrakk>n < m; length xs = m\<rbrakk> \<Longrightarrow> terminate (id m n) xs" |
65 calc_cn: "\<lbrakk>length args = n; |
39 | termi_cn: "\<lbrakk>terminate f (map (\<lambda>g. rec_exec g xs) gs); |
66 \<forall> k < length gs. rec_calc_rel (gs ! k) args (rs ! k); |
40 \<forall>g \<in> set gs. terminate g xs; length xs = n\<rbrakk> \<Longrightarrow> terminate (Cn n f gs) xs" |
67 length rs = length gs; |
41 | termi_pr: "\<lbrakk>\<forall> y < x. terminate g (xs @ y # [rec_exec (Pr n f g) (xs @ [y])]); |
68 rec_calc_rel f rs r\<rbrakk> |
42 terminate f xs; |
69 \<Longrightarrow> rec_calc_rel (Cn n f gs) args r" | |
43 length xs = n\<rbrakk> |
70 calc_pr_zero: |
44 \<Longrightarrow> terminate (Pr n f g) (xs @ [x])" |
71 "\<lbrakk>length args = n; |
45 | termi_mn: "\<lbrakk>length xs = n; terminate f (xs @ [r]); |
72 rec_calc_rel f args r0 \<rbrakk> |
46 rec_exec f (xs @ [r]) = 0; |
73 \<Longrightarrow> rec_calc_rel (Pr n f g) (args @ [0]) r0" | |
47 \<forall> i < r. terminate f (xs @ [i]) \<and> rec_exec f (xs @ [i]) > 0\<rbrakk> \<Longrightarrow> terminate (Mn n f) xs" |
74 calc_pr_ind: " |
|
75 \<lbrakk> length args = n; |
|
76 rec_calc_rel (Pr n f g) (args @ [k]) rk; |
|
77 rec_calc_rel g (args @ [k] @ [rk]) rk'\<rbrakk> |
|
78 \<Longrightarrow> rec_calc_rel (Pr n f g) (args @ [Suc k]) rk'" | |
|
79 calc_mn: "\<lbrakk>length args = n; |
|
80 rec_calc_rel f (args@[r]) 0; |
|
81 \<forall> i < r. (\<exists> ri. rec_calc_rel f (args@[i]) ri \<and> ri \<noteq> 0)\<rbrakk> |
|
82 \<Longrightarrow> rec_calc_rel (Mn n f) args r" |
|
83 |
48 |
84 inductive_cases calc_pr_reverse: "rec_calc_rel (Pr n f g) (lm) rSucy" |
|
85 |
49 |
86 inductive_cases calc_z_reverse: "rec_calc_rel z lm x" |
|
87 |
|
88 inductive_cases calc_s_reverse: "rec_calc_rel s lm x" |
|
89 |
|
90 inductive_cases calc_id_reverse: "rec_calc_rel (id m n) lm x" |
|
91 |
|
92 inductive_cases calc_cn_reverse: "rec_calc_rel (Cn n f gs) lm x" |
|
93 |
|
94 inductive_cases calc_mn_reverse:"rec_calc_rel (Mn n f) lm x" |
|
95 end |
50 end |