DEFEVALUATOR

introduce an evaluator function 
Major Section:  EVENTS


Example:
(defevaluator evl evl-list
  ((length x) (member-equal x y)))
See meta. 

General Form:
(defevaluator ev ev-list
   ((g1 x1 ... xn_1)
    ...
    (gk x1 ... xn_k))
where ev and ev-list are new function symbols and g1, ..., gk are old function symbols with the indicated number of formals, i.e., each gi has n_i formals.

This function provides a convenient way to constrain ev and ev-list to be mutually-recursive evaluator functions for the symbols g1, ..., 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 appropriate defun and defthm events. Perhaps the easiest way to understand what defevaluator does is to execute the keyword command 

:trans1 (defevaluator evl evl-list ((length x) (member-equal 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 :trans1 can be edited by adding hints, then submitted directly.

Formally, ev is said to be an ``evaluator function for g1, ..., gk, with mutually-recursive counterpart ev-list'' iff ev and ev-list are constrained functions satisfying just the constraints discussed below.

Ev and ev-list must satisfy constraints (0)-(4) and (k): 

(0) How to ev an arbitrary function application:
    (implies (and (consp x)
                  (syntaxp (not (equal a ''nil)))
                  (not (equal (car x) 'quote)))
             (equal (ev x a)
                    (ev (cons (car x)
                              (kwote-lst (ev-list (cdr x) a)))
                        nil)))

(1) How to ev a variable symbol:
    (implies (symbolp x)
             (equal (ev x a) (and x (cdr (assoc-equal 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).
Defevaluator defines suitable witnesses for ev and ev-list, proves the theorems about them, and constrains ev and ev-list appropriately. We expect defevaluator to 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 *defevaluator-form-base-theory*.

(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: in (lambda (v1 ... vn) body), the only free variables in body are among the vi. See term.)