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