src/CCL/eval.ML

 (*  Title:      92/CCL/eval
     ID:         $Id$
     Author:     Martin Coen, Cambridge University Computer Laboratory
     Copyright   1992  University of Cambridge
-
 *)
-
-
 
 (*** Evaluation ***)
 
 val EVal_rls = ref [trueV,falseV,pairV,lamV,caseVtrue,caseVfalse,caseVpair,caseVlam];
 val eval_tac = DEPTH_SOLVE_1 (resolve_tac (!EVal_rls) 1);
 fun ceval_tac rls = DEPTH_SOLVE_1 (resolve_tac (!EVal_rls@rls) 1);
 
-val prems = goalw thy [apply_def]
+val prems = goalw (the_context ()) [apply_def]
    "[| f ---> lam x. b(x);  b(a) ---> c |] ==> f ` a ---> c";
 by (ceval_tac prems);
 qed "applyV";
 
 EVal_rls := !EVal_rls @ [applyV];
 
-val major::prems = goalw thy [let_def]
+val major::prems = goalw (the_context ()) [let_def]
    "[| t ---> a;  f(a) ---> c |] ==> let x be t in f(x) ---> c";
 by (rtac (major RS canonical) 1);
 by (REPEAT (DEPTH_SOLVE_1 (resolve_tac ([major]@prems@(!EVal_rls)) 1 ORELSE
                            etac substitute 1)));
 qed "letV";
 
-val prems = goalw thy [fix_def]
+val prems = goalw (the_context ()) [fix_def]
    "f(fix(f)) ---> c ==> fix(f) ---> c";
 by (rtac applyV 1);
 by (rtac lamV 1);
 by (resolve_tac prems 1);
 qed "fixV";
 
-val prems = goalw thy [letrec_def]
+val prems = goalw (the_context ()) [letrec_def]
     "h(t,%y. letrec g x be h(x,g) in g(y)) ---> c ==> \
 \                  letrec g x be h(x,g) in g(t) ---> c";
 by (REPEAT (resolve_tac (prems @ [fixV,applyV,lamV]) 1));
 qed "letrecV";
 
 EVal_rls := !EVal_rls @ [letV,letrecV,fixV];
 
-fun mk_V_rl s = prove_goalw thy data_defs s (fn prems => [ceval_tac prems]);
+fun mk_V_rl s = prove_goalw (the_context ()) data_defs s (fn prems => [ceval_tac prems]);
 
-val V_rls = map mk_V_rl 
+val V_rls = map mk_V_rl
              ["true ---> true",
               "false ---> false",
               "[| b--->true;  t--->c |] ==> if b then t else u ---> c",
               "[| b--->false;  u--->c |] ==> if b then t else u ---> c",
               "<a,b> ---> <a,b>",

 
 EVal_rls := !EVal_rls @ V_rls;
 
 (* Factorial *)
 
-val prems = goal thy
+val prems = goal (the_context ())
     "letrec f n be ncase(n,succ(zero),%x. nrec(n,zero,%y g. nrec(f(x),g,%z h. succ(h)))) \
 \              in f(succ(succ(zero))) ---> ?a";
 by (ceval_tac []);
 
-val prems = goal thy
+val prems = goal (the_context ())
     "letrec f n be ncase(n,succ(zero),%x. nrec(n,zero,%y g. nrec(f(x),g,%z h. succ(h)))) \
 \              in f(succ(succ(succ(zero)))) ---> ?a";
 by (ceval_tac []);
 
 (* Less Than Or Equal *)
 
-fun isle x y = prove_goal thy 
+fun isle x y = prove_goal (the_context ())
     ("letrec f p be split(p,%m n. ncase(m,true,%x. ncase(n,false,%y. f(<x,y>)))) \
 \              in f(<"^x^","^y^">) ---> ?a")
     (fn prems => [ceval_tac []]);
 
 isle "succ(zero)" "succ(zero)";

 isle "succ(succ(succ(succ(succ(zero)))))" "succ(succ(succ(succ(zero))))";
 
 
 (* Reverse *)
 
-val prems = goal thy
+val prems = goal (the_context ())
     "letrec id l be lcase(l,[],%x xs. x$id(xs)) \
 \              in id(zero$succ(zero)$[]) ---> ?a";
 by (ceval_tac []);
 
-val prems = goal thy
+val prems = goal (the_context ())
     "letrec rev l be lcase(l,[],%x xs. lrec(rev(xs),x$[],%y ys g. y$g)) \
 \              in rev(zero$succ(zero)$(succ((lam x. x)`succ(zero)))$([])) ---> ?a";
 by (ceval_tac []);
-