1 theory Rec_Def |
1 theory Rec_Def |
2 imports Main |
2 imports Main |
3 begin |
3 begin |
4 |
4 |
5 section {* |
5 section {* Recursive functions *} |
6 Recursive functions |
|
7 *} |
|
8 |
|
9 text {* |
|
10 Datatype of recursive operators. |
|
11 *} |
|
12 |
6 |
13 datatype recf = |
7 datatype recf = |
14 -- {* The zero function, which always resturns @{text "0"} as result. *} |
8 z | s | |
15 z | |
9 -- {* The projection function, where @{text "id i j"} returns the @{text "j"}-th |
16 -- {* The successor function, which increments its arguments. *} |
10 argment out of the @{text "i"} arguments. *} |
17 s | |
|
18 -- {* |
|
19 The projection function, where @{text "id i j"} returns the @{text "j"}-th |
|
20 argment out of the @{text "i"} arguments. |
|
21 *} |
|
22 id nat nat | |
11 id nat nat | |
23 -- {* |
12 -- {* The compostion operator, where "@{text "Cn n f [g1; g2; \<dots> ;gm]"} |
24 The compostion operator, where "@{text "Cn n f [g1; g2; \<dots> ;gm]"} |
|
25 computes @{text "f (g1(x1, x2, \<dots>, xn), g2(x1, x2, \<dots>, xn), \<dots> , |
13 computes @{text "f (g1(x1, x2, \<dots>, xn), g2(x1, x2, \<dots>, xn), \<dots> , |
26 gm(x1, x2, \<dots> , xn))"} for input argments @{text "x1, \<dots>, xn"}. |
14 gm(x1, x2, \<dots> , xn))"} for input argments @{text "x1, \<dots>, xn"}. *} |
27 *} |
|
28 Cn nat recf "recf list" | |
15 Cn nat recf "recf list" | |
29 -- {* |
16 -- {* The primitive resursive operator, where @{text "Pr n f g"} computes: |
30 The primitive resursive operator, where @{text "Pr n f g"} computes: |
|
31 @{text "Pr n f g (x1, x2, \<dots>, xn-1, 0) = f(x1, \<dots>, xn-1)"} |
17 @{text "Pr n f g (x1, x2, \<dots>, xn-1, 0) = f(x1, \<dots>, xn-1)"} |
32 and @{text "Pr n f g (x1, x2, \<dots>, xn-1, k') = g(x1, x2, \<dots>, xn-1, k, |
18 and @{text "Pr n f g (x1, x2, \<dots>, xn-1, k') = g(x1, x2, \<dots>, xn-1, k, |
33 Pr n f g (x1, \<dots>, xn-1, k))"}. |
19 Pr n f g (x1, \<dots>, xn-1, k))"}. |
34 *} |
20 *} |
35 Pr nat recf recf | |
21 Pr nat recf recf | |
36 -- {* |
22 -- {* The minimization operator, where @{text "Mn n f (x1, x2, \<dots> , xn)"} |
37 The minimization operator, where @{text "Mn n f (x1, x2, \<dots> , xn)"} |
|
38 computes the first i such that @{text "f (x1, \<dots>, xn, i) = 0"} and for all |
23 computes the first i such that @{text "f (x1, \<dots>, xn, i) = 0"} and for all |
39 @{text "j"}, @{text "f (x1, x2, \<dots>, xn, j) > 0"}. |
24 @{text "j"}, @{text "f (x1, x2, \<dots>, xn, j) > 0"}. *} |
40 *} |
|
41 Mn nat recf |
25 Mn nat recf |
42 |
26 |
43 text {* |
27 text {* |
44 The semantis of recursive operators is given by an inductively defined |
28 The semantis of recursive operators is given by an inductively defined |
45 relation as follows, where |
29 relation as follows, where |
70 calc_mn: "\<lbrakk>length args = n; |
54 calc_mn: "\<lbrakk>length args = n; |
71 rec_calc_rel f (args@[r]) 0; |
55 rec_calc_rel f (args@[r]) 0; |
72 \<forall> i < r. (\<exists> ri. rec_calc_rel f (args@[i]) ri \<and> ri \<noteq> 0)\<rbrakk> |
56 \<forall> i < r. (\<exists> ri. rec_calc_rel f (args@[i]) ri \<and> ri \<noteq> 0)\<rbrakk> |
73 \<Longrightarrow> rec_calc_rel (Mn n f) args r" |
57 \<Longrightarrow> rec_calc_rel (Mn n f) args r" |
74 |
58 |
75 inductive_cases calc_pr_reverse: |
59 inductive_cases calc_pr_reverse: "rec_calc_rel (Pr n f g) (lm) rSucy" |
76 "rec_calc_rel (Pr n f g) (lm) rSucy" |
|
77 |
60 |
78 inductive_cases calc_z_reverse: "rec_calc_rel z lm x" |
61 inductive_cases calc_z_reverse: "rec_calc_rel z lm x" |
79 |
62 |
80 inductive_cases calc_s_reverse: "rec_calc_rel s lm x" |
63 inductive_cases calc_s_reverse: "rec_calc_rel s lm x" |
81 |
64 |