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