src/CCL/eval.ML
changeset 0 a5a9c433f639
child 289 78541329ff35
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/CCL/eval.ML	Thu Sep 16 12:20:38 1993 +0200
     1.3 @@ -0,0 +1,104 @@
     1.4 +(*  Title: 	92/CCL/eval
     1.5 +    ID:         $Id$
     1.6 +    Author: 	Martin Coen, Cambridge University Computer Laboratory
     1.7 +    Copyright   1992  University of Cambridge
     1.8 +
     1.9 +*)
    1.10 +
    1.11 +
    1.12 +
    1.13 +(*** Evaluation ***)
    1.14 +
    1.15 +val EVal_rls = ref [trueV,falseV,pairV,lamV,caseVtrue,caseVfalse,caseVpair,caseVlam];
    1.16 +val eval_tac = DEPTH_SOLVE_1 (resolve_tac (!EVal_rls) 1);
    1.17 +fun ceval_tac rls = DEPTH_SOLVE_1 (resolve_tac (!EVal_rls@rls) 1);
    1.18 +
    1.19 +val prems = goalw thy [apply_def]
    1.20 +   "[| f ---> lam x.b(x);  b(a) ---> c |] ==> f ` a ---> c";
    1.21 +by (ceval_tac prems);
    1.22 +val applyV = result();
    1.23 +
    1.24 +EVal_rls := !EVal_rls @ [applyV];
    1.25 +
    1.26 +val major::prems = goalw thy [let_def]
    1.27 +   "[| t ---> a;  f(a) ---> c |] ==> let x be t in f(x) ---> c";
    1.28 +br (major RS canonical) 1;
    1.29 +by (REPEAT (DEPTH_SOLVE_1 (resolve_tac ([major]@prems@(!EVal_rls)) 1 ORELSE
    1.30 +                           eresolve_tac [substitute] 1)));
    1.31 +val letV = result();
    1.32 +
    1.33 +val prems = goalw thy [fix_def]
    1.34 +   "f(fix(f)) ---> c ==> fix(f) ---> c";
    1.35 +br applyV 1;
    1.36 +br lamV 1;
    1.37 +brs prems 1;
    1.38 +val fixV = result();
    1.39 +
    1.40 +val prems = goalw thy [letrec_def]
    1.41 +    "h(t,%y.letrec g x be h(x,g) in g(y)) ---> c ==> \
    1.42 +\                  letrec g x be h(x,g) in g(t) ---> c";
    1.43 +by (REPEAT (resolve_tac (prems @ [fixV,applyV,lamV]) 1));
    1.44 +val letrecV = result();
    1.45 +
    1.46 +EVal_rls := !EVal_rls @ [letV,letrecV,fixV];
    1.47 +
    1.48 +fun mk_V_rl s = prove_goalw thy data_defs s (fn prems => [ceval_tac prems]);
    1.49 +
    1.50 +val V_rls = map mk_V_rl 
    1.51 +             ["true ---> true",
    1.52 +              "false ---> false",
    1.53 +              "[| b--->true;  t--->c |] ==> if b then t else u ---> c",
    1.54 +              "[| b--->false;  u--->c |] ==> if b then t else u ---> c",
    1.55 +              "<a,b> ---> <a,b>",
    1.56 +              "[| t ---> <a,b>;  h(a,b) ---> c |] ==> split(t,h) ---> c",
    1.57 +              "zero ---> zero",
    1.58 +              "succ(n) ---> succ(n)",
    1.59 +              "[| n ---> zero; t ---> c |] ==> ncase(n,t,u) ---> c",
    1.60 +              "[| n ---> succ(x); u(x) ---> c |] ==> ncase(n,t,u) ---> c",
    1.61 +              "[| n ---> zero; t ---> c |] ==> nrec(n,t,u) ---> c",
    1.62 +              "[| n--->succ(x); u(x,nrec(x,t,u))--->c |] ==> nrec(n,t,u)--->c",
    1.63 +              "[] ---> []",
    1.64 +              "h.t ---> h.t",
    1.65 +              "[| l ---> []; t ---> c |] ==> lcase(l,t,u) ---> c",
    1.66 +              "[| l ---> x.xs; u(x,xs) ---> c |] ==> lcase(l,t,u) ---> c",
    1.67 +              "[| l ---> []; t ---> c |] ==> lrec(l,t,u) ---> c",
    1.68 +              "[| l--->x.xs; u(x,xs,lrec(xs,t,u))--->c |] ==> lrec(l,t,u)--->c"];
    1.69 +
    1.70 +EVal_rls := !EVal_rls @ V_rls;
    1.71 +
    1.72 +(* Factorial *)
    1.73 +
    1.74 +val prems = goal thy
    1.75 +    "letrec f n be ncase(n,succ(zero),%x.nrec(n,zero,%y g.nrec(f(x),g,%z h.succ(h)))) \
    1.76 +\              in f(succ(succ(zero))) ---> ?a";
    1.77 +by (ceval_tac []);
    1.78 +
    1.79 +val prems = goal thy
    1.80 +    "letrec f n be ncase(n,succ(zero),%x.nrec(n,zero,%y g.nrec(f(x),g,%z h.succ(h)))) \
    1.81 +\              in f(succ(succ(succ(zero)))) ---> ?a";
    1.82 +by (ceval_tac []);
    1.83 +
    1.84 +(* Less Than Or Equal *)
    1.85 +
    1.86 +fun isle x y = prove_goal thy 
    1.87 +    ("letrec f p be split(p,%m n.ncase(m,true,%x.ncase(n,false,%y.f(<x,y>)))) \
    1.88 +\              in f(<"^x^","^y^">) ---> ?a")
    1.89 +    (fn prems => [ceval_tac []]);
    1.90 +
    1.91 +isle "succ(zero)" "succ(zero)";
    1.92 +isle "succ(zero)" "succ(succ(succ(succ(zero))))";
    1.93 +isle "succ(succ(succ(succ(succ(zero)))))" "succ(succ(succ(succ(zero))))";
    1.94 +
    1.95 +
    1.96 +(* Reverse *)
    1.97 +
    1.98 +val prems = goal thy
    1.99 +    "letrec id l be lcase(l,[],%x xs.x.id(xs)) \
   1.100 +\              in id(zero.succ(zero).[]) ---> ?a";
   1.101 +by (ceval_tac []);
   1.102 +
   1.103 +val prems = goal thy
   1.104 +    "letrec rev l be lcase(l,[],%x xs.lrec(rev(xs),x.[],%y ys g.y.g)) \
   1.105 +\              in rev(zero.succ(zero).(succ((lam x.x)`succ(zero))).([])) ---> ?a";
   1.106 +by (ceval_tac []);
   1.107 +