1 header {* Definition of Recursive Functions *} |
1 header {* Definition of Recursive Functions *} |
2 |
2 |
3 theory Rec_Def |
3 theory Rec_Def |
4 imports Main "~~/src/HOL/Library/Monad_Syntax" |
4 imports Main "~~/src/HOL/Library/Monad_Syntax" |
5 begin |
5 begin |
6 |
|
7 type_synonym heap = "nat \<Rightarrow> nat" |
|
8 type_synonym exception = nat |
|
9 |
|
10 datatype 'a Heap = Heap "heap \<Rightarrow> (('a + exception) * heap)" |
|
11 |
|
12 definition return |
|
13 where "return x = Heap (Pair (Inl x))" |
|
14 |
|
15 fun exec |
|
16 where "exec (Heap f) = f" |
|
17 |
|
18 definition bind ("_ >>= _") |
|
19 where "bind f g = Heap (\<lambda>h. case (exec f h) of |
|
20 (Inl x, h') \<Rightarrow> exec (g x) h' |
|
21 | (Inr exn, h') \<Rightarrow> (Inr exn, h') |
|
22 )" |
|
23 |
6 |
24 datatype recf = |
7 datatype recf = |
25 Zero |
8 Zero |
26 | Succ |
9 | Succ |
27 | Id nat nat --"Projection" |
10 | Id nat nat --"Projection" |
28 | Cn nat recf "recf list" --"Composition" |
11 | Cn nat recf "recf list" --"Composition" |
29 | Pr nat recf recf --"Primitive recursion" |
12 | Pr nat recf recf --"Primitive recursion" |
30 | Mn nat recf --"Minimisation" |
13 | Mn nat recf --"Minimisation" |
31 |
14 |
32 partial_function (tailrec) |
15 partial_function (option) |
33 findzero :: "(nat \<Rightarrow> nat) \<Rightarrow> nat \<Rightarrow> nat" |
16 eval :: "recf \<Rightarrow> nat option \<Rightarrow> (nat list) option => nat list \<Rightarrow> nat option" |
34 where |
17 where |
35 "findzero f n = (if f n = 0 then n else findzero f (Suc n))" |
18 "eval f i gs ns = (case (i, gs, f, ns) of |
|
19 (None, None, Zero, [n]) \<Rightarrow> Some 0 |
|
20 | (None, None, Succ, [n]) \<Rightarrow> Some (n + 1) |
|
21 | (None, None, Id i j, ns) \<Rightarrow> if (j < i) then Some (ns ! j) else None |
|
22 | (None, None, Pr n f g, 0 # ns) \<Rightarrow> eval f None None ns |
|
23 | (None, None, Pr n f g, Suc k # ns) \<Rightarrow> |
|
24 do { r \<leftarrow> eval (Pr n f g) None None (k # ns); eval g None None (r # k # ns) } |
|
25 | (None, None, Mn n f, ns) \<Rightarrow> eval f (Some 0) None ns |
|
26 | (Some n, None, f, ns) \<Rightarrow> |
|
27 do { r \<leftarrow> eval f None None (n # ns); |
|
28 if r = 0 then Some n else eval f (Some (Suc n)) None ns } |
|
29 | (None, None, Cn n f [], ns) \<Rightarrow> eval f None None [] |
|
30 | (None, None, Cn n f (g#gs), ns) \<Rightarrow> |
|
31 do { r \<leftarrow> eval g None None ns; eval (Cn n f gs) None (Some [r]) ns } |
|
32 | (None, Some rs, Cn n f [], ns) \<Rightarrow> eval f None None rs |
|
33 | (None, Some rs, Cn n f (g#gs), ns) \<Rightarrow> |
|
34 do { r \<leftarrow> eval g None None ns; eval (Cn n f gs) None (Some (r#rs)) ns } |
|
35 | (_, _) \<Rightarrow> None)" |
36 |
36 |
37 print_theorems |
37 abbreviation |
|
38 "eval0 f ns \<equiv> eval f None None ns" |
38 |
39 |
39 declare findzero.simps[simp del] |
40 lemma "eval0 Zero [n] = Some 0" |
40 |
41 apply(subst eval.simps) |
41 lemma "findzero (\<lambda>n. if n = 3 then 0 else 1) 0 = 3" |
42 apply(simp) |
42 apply(simp add: findzero.simps) |
|
43 done |
43 done |
44 |
44 |
45 lemma "findzero (\<lambda>n. if n = 3 then 0 else 1) 0 \<noteq> 2" |
45 lemma "eval0 Succ [n] = Some (n + 1)" |
46 apply(simp add: findzero.simps) |
46 apply(subst eval.simps) |
|
47 apply(simp) |
|
48 done |
|
49 |
|
50 lemma "eval0 (Id i j) ns = (if (j < i) then Some (ns ! j) else None)" |
|
51 apply(subst eval.simps) |
|
52 apply(simp) |
|
53 done |
|
54 |
|
55 lemma "eval0 (Pr n f g) (0 # ns) = eval0 f ns" |
|
56 apply(subst eval.simps) |
|
57 apply(simp) |
|
58 done |
|
59 |
|
60 lemma "eval0 (Pr n f g) (Suc k # ns) = |
|
61 do { r \<leftarrow> eval0 (Pr n f g) (k # ns); eval0 g (r # k # ns) }" |
|
62 apply(subst eval.simps) |
|
63 apply(simp) |
47 done |
64 done |
48 |
65 |
49 |
66 |
50 fun |
|
51 least :: "(nat \<Rightarrow> bool) \<Rightarrow> nat" |
|
52 where |
|
53 "least P = (SOME n. (P n \<and> (\<forall>m. m < n \<longrightarrow> \<not> P m)))" |
|
54 |
67 |
55 lemma [partial_function_mono]: |
|
56 "mono_option (\<lambda>eval. if \<forall>g\<in>set list. case eval (g, ba) of None \<Rightarrow> False | Some a \<Rightarrow> True |
|
57 then eval (recf, map (\<lambda>g. the (eval (g, ba))) list) else None)" |
|
58 apply(rule monotoneI) |
|
59 unfolding flat_ord_def |
|
60 apply(auto) |
|
61 oops |
|
62 |
68 |
63 partial_function (option) |
|
64 eval :: "recf \<Rightarrow> nat list \<Rightarrow> nat option" |
|
65 where |
|
66 "eval f ns = (case (f, ns) of |
|
67 (Zero, [n]) \<Rightarrow> Some 0 |
|
68 | (Succ, [n]) \<Rightarrow> Some (n + 1) |
|
69 | (Id i j, ns) \<Rightarrow> if (j < i) then Some (ns ! j) else None |
|
70 | (Pr n f g, 0 # ns) \<Rightarrow> eval f ns |
|
71 | (Pr n f g, Suc k # ns) \<Rightarrow> |
|
72 do { r \<leftarrow> eval (Pr n f g) (k # ns); eval g (r # k # ns) } |
|
73 | (Cn n f gs, ns) \<Rightarrow> if (\<forall>g \<in> set gs. case (eval g ns) of None => False | _ => True) |
|
74 then eval f (map (\<lambda>g. the (eval g ns)) gs) else None |
|
75 | (_, _) \<Rightarrow> None)" |
|
76 |
|
77 (* |
|
78 | (Cn n f gs, ns) \<Rightarrow> if (\<forall>g \<in> set gs. case (eval g ns) of None => False | _ => True) |
|
79 then eval f (map (\<lambda>g. the (eval g ns)) gs) else None |
|
80 *) |
|
81 (* |
|
82 | (Mn n f, ns) \<Rightarrow> Some (least (\<lambda>r. eval f (r # ns) = Some 0)) |
|
83 *) |
|
84 end |
69 end |