0
|
1 |
(* Title: 92/CCL/eval
|
|
2 |
ID: $Id$
|
|
3 |
Author: Martin Coen, Cambridge University Computer Laboratory
|
|
4 |
Copyright 1992 University of Cambridge
|
|
5 |
|
|
6 |
*)
|
|
7 |
|
|
8 |
|
|
9 |
|
|
10 |
(*** Evaluation ***)
|
|
11 |
|
|
12 |
val EVal_rls = ref [trueV,falseV,pairV,lamV,caseVtrue,caseVfalse,caseVpair,caseVlam];
|
|
13 |
val eval_tac = DEPTH_SOLVE_1 (resolve_tac (!EVal_rls) 1);
|
|
14 |
fun ceval_tac rls = DEPTH_SOLVE_1 (resolve_tac (!EVal_rls@rls) 1);
|
|
15 |
|
|
16 |
val prems = goalw thy [apply_def]
|
|
17 |
"[| f ---> lam x.b(x); b(a) ---> c |] ==> f ` a ---> c";
|
|
18 |
by (ceval_tac prems);
|
|
19 |
val applyV = result();
|
|
20 |
|
|
21 |
EVal_rls := !EVal_rls @ [applyV];
|
|
22 |
|
|
23 |
val major::prems = goalw thy [let_def]
|
|
24 |
"[| t ---> a; f(a) ---> c |] ==> let x be t in f(x) ---> c";
|
|
25 |
br (major RS canonical) 1;
|
|
26 |
by (REPEAT (DEPTH_SOLVE_1 (resolve_tac ([major]@prems@(!EVal_rls)) 1 ORELSE
|
|
27 |
eresolve_tac [substitute] 1)));
|
|
28 |
val letV = result();
|
|
29 |
|
|
30 |
val prems = goalw thy [fix_def]
|
|
31 |
"f(fix(f)) ---> c ==> fix(f) ---> c";
|
|
32 |
br applyV 1;
|
|
33 |
br lamV 1;
|
|
34 |
brs prems 1;
|
|
35 |
val fixV = result();
|
|
36 |
|
|
37 |
val prems = goalw thy [letrec_def]
|
|
38 |
"h(t,%y.letrec g x be h(x,g) in g(y)) ---> c ==> \
|
|
39 |
\ letrec g x be h(x,g) in g(t) ---> c";
|
|
40 |
by (REPEAT (resolve_tac (prems @ [fixV,applyV,lamV]) 1));
|
|
41 |
val letrecV = result();
|
|
42 |
|
|
43 |
EVal_rls := !EVal_rls @ [letV,letrecV,fixV];
|
|
44 |
|
|
45 |
fun mk_V_rl s = prove_goalw thy data_defs s (fn prems => [ceval_tac prems]);
|
|
46 |
|
|
47 |
val V_rls = map mk_V_rl
|
|
48 |
["true ---> true",
|
|
49 |
"false ---> false",
|
|
50 |
"[| b--->true; t--->c |] ==> if b then t else u ---> c",
|
|
51 |
"[| b--->false; u--->c |] ==> if b then t else u ---> c",
|
|
52 |
"<a,b> ---> <a,b>",
|
|
53 |
"[| t ---> <a,b>; h(a,b) ---> c |] ==> split(t,h) ---> c",
|
|
54 |
"zero ---> zero",
|
|
55 |
"succ(n) ---> succ(n)",
|
|
56 |
"[| n ---> zero; t ---> c |] ==> ncase(n,t,u) ---> c",
|
|
57 |
"[| n ---> succ(x); u(x) ---> c |] ==> ncase(n,t,u) ---> c",
|
|
58 |
"[| n ---> zero; t ---> c |] ==> nrec(n,t,u) ---> c",
|
|
59 |
"[| n--->succ(x); u(x,nrec(x,t,u))--->c |] ==> nrec(n,t,u)--->c",
|
|
60 |
"[] ---> []",
|
|
61 |
"h.t ---> h.t",
|
|
62 |
"[| l ---> []; t ---> c |] ==> lcase(l,t,u) ---> c",
|
|
63 |
"[| l ---> x.xs; u(x,xs) ---> c |] ==> lcase(l,t,u) ---> c",
|
|
64 |
"[| l ---> []; t ---> c |] ==> lrec(l,t,u) ---> c",
|
|
65 |
"[| l--->x.xs; u(x,xs,lrec(xs,t,u))--->c |] ==> lrec(l,t,u)--->c"];
|
|
66 |
|
|
67 |
EVal_rls := !EVal_rls @ V_rls;
|
|
68 |
|
|
69 |
(* Factorial *)
|
|
70 |
|
|
71 |
val prems = goal thy
|
|
72 |
"letrec f n be ncase(n,succ(zero),%x.nrec(n,zero,%y g.nrec(f(x),g,%z h.succ(h)))) \
|
|
73 |
\ in f(succ(succ(zero))) ---> ?a";
|
|
74 |
by (ceval_tac []);
|
|
75 |
|
|
76 |
val prems = goal thy
|
|
77 |
"letrec f n be ncase(n,succ(zero),%x.nrec(n,zero,%y g.nrec(f(x),g,%z h.succ(h)))) \
|
|
78 |
\ in f(succ(succ(succ(zero)))) ---> ?a";
|
|
79 |
by (ceval_tac []);
|
|
80 |
|
|
81 |
(* Less Than Or Equal *)
|
|
82 |
|
|
83 |
fun isle x y = prove_goal thy
|
|
84 |
("letrec f p be split(p,%m n.ncase(m,true,%x.ncase(n,false,%y.f(<x,y>)))) \
|
|
85 |
\ in f(<"^x^","^y^">) ---> ?a")
|
|
86 |
(fn prems => [ceval_tac []]);
|
|
87 |
|
|
88 |
isle "succ(zero)" "succ(zero)";
|
|
89 |
isle "succ(zero)" "succ(succ(succ(succ(zero))))";
|
|
90 |
isle "succ(succ(succ(succ(succ(zero)))))" "succ(succ(succ(succ(zero))))";
|
|
91 |
|
|
92 |
|
|
93 |
(* Reverse *)
|
|
94 |
|
|
95 |
val prems = goal thy
|
|
96 |
"letrec id l be lcase(l,[],%x xs.x.id(xs)) \
|
|
97 |
\ in id(zero.succ(zero).[]) ---> ?a";
|
|
98 |
by (ceval_tac []);
|
|
99 |
|
|
100 |
val prems = goal thy
|
|
101 |
"letrec rev l be lcase(l,[],%x xs.lrec(rev(xs),x.[],%y ys g.y.g)) \
|
|
102 |
\ in rev(zero.succ(zero).(succ((lam x.x)`succ(zero))).([])) ---> ?a";
|
|
103 |
by (ceval_tac []);
|
|
104 |
|