Major Section: EVENTS
Example: (defevaluator evl evl-list ((length x) (member x y)))See meta.
General Form: (defevaluator ev ev-list ((g1 x1 ... xn_1) ... (gk x1 ... xn_k))where
ev-list are new function symbols and
gkare old function symbols with the indicated number of formals, i.e., each
This function provides a convenient way to constrain
to be mutually-recursive evaluator functions for the symbols
gk. Roughly speaking, an evaluator function for a fixed,
finite set of function symbols is a restriction of the universal
evaluator to terms composed of variables, constants, lambda
expressions, and applications of the given functions. However,
evaluator functions are constrained rather than defined, so that the
proof that a given metafunction is correct vis-a-vis a particular
evaluator function can be lifted (by functional instantiation) to a
proof that it is correct for any larger evaluator function.
See meta for a discussion of metafunctions.
Defevaluator executes an
encapsulate after generating the
defthm events. Perhaps the easiest way to
defevaluator does is to execute the keyword command
:trans1 (defevaluator evl evl-list ((length x) (member x y)))and inspect the output. This trick is also useful in the rare case that the event fails because a hint is needed. In that case, the output of
trans1can be edited by adding hints, then submitted directly.
ev is said to be an ``evaluator function for
gk, with mutually-recursive counterpart
ev-list are constrained functions satisfying just the
constraints discussed below.
ev-list must satisfy constraints (1)-(4) and (k):
(1) How to ev a variable symbol: (implies (symbolp x) (equal (ev x a) (cdr (assoc-eq x a))))
(2) How to ev a constant: (implies (and (consp x) (equal (car x) 'quote)) (equal (ev x a) (cadr x)))
(3) How to ev a lambda application: (implies (and (consp x) (consp (car x))) (equal (ev x a) (ev (caddar x) (pairlis$ (cadar x) (ev-list (cdr x) a)))))
(4) How to ev an argument list: (implies (consp x-lst) (equal (ev-list x-lst a) (cons (ev (car x-lst) a) (ev-list (cdr x-lst) a)))) (implies (not (consp x-lst)) (equal (ev-list x-lst a) nil))
(k) For each i from 1 to k, how to ev an application of gi, where gi is a function symbol of n arguments: (implies (and (consp x) (equal (car x) 'gi)) (equal (ev x a) (gi (ev x1 a) ... (ev xn a)))), where xi is the (cad...dr x) expression equivalent to (nth i x).
Defevaluatordefines suitable witnesses for
ev-list, proves the theorems about them, and constrains
ev-listappropriately. We expect
defevaluatorto work without assistance from you, though the proofs do take some time and generate a lot of output. The proofs are done in the context of a fixed theory, namely the value of the constant
(Aside: (3) above may seem surprising, since the bindings of
a are not
included in the environment that is used to evaluate the lambda body,
(caddar x). However, ACL2 lambda expressions are all closed:
(lambda (v1 ... vn) body), the only free variables in
vi. See term.)