28 Pr nat recf recf | |
28 Pr nat recf recf | |
29 -- {* The minimization operator, where @{text "Mn n f (x1, x2, \<dots> , xn)"} |
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 |
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"}. *} |
31 @{text "j"}, @{text "f (x1, x2, \<dots>, xn, j) > 0"}. *} |
32 Mn nat recf |
32 Mn nat recf |
|
33 |
|
34 (* |
|
35 partial_function (tailrec) |
|
36 rec_exec :: "recf \<Rightarrow> nat list \<Rightarrow> nat" |
|
37 where |
|
38 "rec_exec f ns = (case (f, ns) of |
|
39 (z, xs) => 0 |
|
40 | (s, xs) => Suc (xs ! 0) |
|
41 | (id m n, xs) => (xs ! n) |
|
42 | (Cn n f gs, xs) => |
|
43 (let ys = (map (\<lambda> a. rec_exec a xs) gs) in |
|
44 rec_exec f ys) |
|
45 | (Pr n f g, xs) => |
|
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 *) |
33 |
51 |
34 text {* |
52 text {* |
35 The semantis of recursive operators is given by an inductively defined |
53 The semantis of recursive operators is given by an inductively defined |
36 relation as follows, where |
54 relation as follows, where |
37 @{text "rec_calc_rel R [x1, x2, \<dots>, xn] r"} means the computation of |
55 @{text "rec_calc_rel R [x1, x2, \<dots>, xn] r"} means the computation of |