src/CCL/eval.ML
author paulson
Fri Feb 16 17:24:51 1996 +0100 (1996-02-16)
changeset 1511 09354d37a5ab
parent 1459 d12da312eff4
child 3837 d7f033c74b38
permissions -rw-r--r--
Elimination of fully-functorial style.
Type tactic changed to a type abbrevation (from a datatype).
Constructor tactic and function apply deleted.
     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 qed "applyV";
    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 by (rtac (major RS canonical) 1);
    26 by (REPEAT (DEPTH_SOLVE_1 (resolve_tac ([major]@prems@(!EVal_rls)) 1 ORELSE
    27                            etac substitute 1)));
    28 qed "letV";
    29 
    30 val prems = goalw thy [fix_def]
    31    "f(fix(f)) ---> c ==> fix(f) ---> c";
    32 by (rtac applyV 1);
    33 by (rtac lamV 1);
    34 by (resolve_tac prems 1);
    35 qed "fixV";
    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 qed "letrecV";
    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