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