212
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
1 |
header {* Definition of Recursive Functions *}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
2 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
3 |
theory Rec_Def
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
4 |
imports Main "~~/src/HOL/Library/Monad_Syntax"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
5 |
begin
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
6 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
7 |
datatype recf =
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
8 |
Zero
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
9 |
| Succ
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
10 |
| Id nat nat --"Projection"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
11 |
| Cn nat recf "recf list" --"Composition"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
12 |
| Pr nat recf recf --"Primitive recursion"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
13 |
| Mn nat recf --"Minimisation"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
14 |
|
215
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
15 |
primrec hd0 :: "nat list => nat" where
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
16 |
"hd0 [] = 0" |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
17 |
"hd0 (m # ms) = m"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
18 |
|
216
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
19 |
(*
|
215
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
20 |
fun
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
21 |
primerec :: "recf \<Rightarrow> nat \<Rightarrow> bool"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
22 |
where
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
23 |
"primerec Zero m = (m = 1)" |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
24 |
"primerec Succ m = (m = 1)" |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
25 |
"primerec (Id i j) m = (j < i \<and> i = m) " |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
26 |
"primerec (Cn n f gs) m = (primerec f (length gs) \<and> (\<forall>g \<in> set gs. primerec g m))" |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
27 |
"primerec (Pr n f g) m = (0 < m \<and> primerec f (m - 1) \<and> primerec g (m + 2))" |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
28 |
"primerec (Mn n f) m = False"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
29 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
30 |
function (domintros) eval :: "recf \<Rightarrow> nat list \<Rightarrow> nat"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
31 |
where
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
32 |
"eval Zero ns = 0" |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
33 |
"eval Succ ns = (Suc (hd0 ns))" |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
34 |
"eval (Id m n) ns = (ns ! n)" |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
35 |
"eval (Cn n f gs) ns =
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
36 |
(let ys = (map (\<lambda>a. eval a ns) gs) in eval f ys)" |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
37 |
"eval (Pr n f g) [] = eval f []" |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
38 |
"eval (Pr n f g) (0#ns) = eval f ns" |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
39 |
"eval (Pr n f g) (Suc m#ns) = eval g (eval (Pr n f g) (m # ns) # m # ns)" |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
40 |
"eval (Mn n f) ns = (LEAST x. eval f (x # ns) = 0)"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
41 |
by pat_completeness auto
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
42 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
43 |
thm eval.psimps
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
44 |
thm eval.pinduct
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
45 |
thm eval.domintros
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
46 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
47 |
lemma
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
48 |
"primerec f (length ns) \<Longrightarrow> eval_dom (f, (ns::nat list))"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
49 |
apply(induct arbitrary: ns rule: primerec.induct)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
50 |
apply(auto intro: eval.domintros)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
51 |
????
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
52 |
|
216
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
53 |
*)
|
215
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
54 |
|
213
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
55 |
partial_function (option)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
56 |
eval :: "recf \<Rightarrow> nat option \<Rightarrow> (nat list) option => nat list \<Rightarrow> nat option"
|
212
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
57 |
where
|
213
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
58 |
"eval f i gs ns = (case (i, gs, f, ns) of
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
59 |
(None, None, Zero, [n]) \<Rightarrow> Some 0
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
60 |
| (None, None, Succ, [n]) \<Rightarrow> Some (n + 1)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
61 |
| (None, None, Id i j, ns) \<Rightarrow> if (j < i) then Some (ns ! j) else None
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
62 |
| (None, None, Pr n f g, 0 # ns) \<Rightarrow> eval f None None ns
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
63 |
| (None, None, Pr n f g, Suc k # ns) \<Rightarrow>
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
64 |
do { r \<leftarrow> eval (Pr n f g) None None (k # ns); eval g None None (r # k # ns) }
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
65 |
| (None, None, Mn n f, ns) \<Rightarrow> eval f (Some 0) None ns
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
66 |
| (Some n, None, f, ns) \<Rightarrow>
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
67 |
do { r \<leftarrow> eval f None None (n # ns);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
68 |
if r = 0 then Some n else eval f (Some (Suc n)) None ns }
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
69 |
| (None, None, Cn n f [], ns) \<Rightarrow> eval f None None []
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
70 |
| (None, None, Cn n f (g#gs), ns) \<Rightarrow>
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
71 |
do { r \<leftarrow> eval g None None ns; eval (Cn n f gs) None (Some [r]) ns }
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
72 |
| (None, Some rs, Cn n f [], ns) \<Rightarrow> eval f None None rs
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
73 |
| (None, Some rs, Cn n f (g#gs), ns) \<Rightarrow>
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
74 |
do { r \<leftarrow> eval g None None ns; eval (Cn n f gs) None (Some (r#rs)) ns }
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
75 |
| (_, _) \<Rightarrow> None)"
|
212
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
76 |
|
213
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
77 |
abbreviation
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
78 |
"eval0 f ns \<equiv> eval f None None ns"
|
212
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
79 |
|
216
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
80 |
lemma "eval0 Zero [n] = Some 0"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
81 |
apply(subst eval.simps)
|
213
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
82 |
apply(simp)
|
212
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
83 |
done
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
84 |
|
216
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
85 |
lemma "eval0 Succ [n] = Some (n + 1)"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
86 |
apply(subst eval.simps)
|
213
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
87 |
apply(simp)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
88 |
done
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
89 |
|
216
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
90 |
lemma "j < i \<Longrightarrow> eval0 (Id i j) ns = Some (ns ! j)"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
91 |
apply(subst eval.simps)
|
213
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
92 |
apply(simp)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
93 |
done
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
94 |
|
216
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
95 |
lemma "eval0 (Pr n f g) (0 # ns) = eval0 f ns"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
96 |
apply(subst eval.simps)
|
213
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
97 |
apply(simp)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
98 |
done
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
99 |
|
216
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
100 |
lemma "eval0 (Pr n f g) (Suc k # ns) =
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
101 |
do { r \<leftarrow> eval0 (Pr n f g) (k # ns); eval0 g (r # k # ns) }"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
102 |
apply(subst eval.simps)
|
213
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
103 |
apply(simp)
|
212
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
104 |
done
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
105 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
106 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
107 |
|
216
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
108 |
lemma
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
109 |
"eval0 (Mn n f) ns = Some (LEAST r. eval0 f (r # ns) = Some 0)"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
110 |
apply(subst eval.simps)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
111 |
apply(simp)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
112 |
apply(subst eval.simps)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
113 |
apply(simp)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
114 |
done
|
212
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
115 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
116 |
end |