|
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 |