Included Books
other
(in-package "ACL2")
include-book
(include-book "std/util/define" :dir :system)
include-book
(include-book "tools/rulesets" :dir :system)
include-book
(include-book "clause-processors/meta-extract-user" :dir :system)
include-book
(include-book "tools/match-tree" :dir :system)
other
(defevaluator evmeta-ev evmeta-ev-lst ((eql a b) (equal a b) (implies a b) (if a b c) (not a) (car x) (cdr x) (nth n x) (cons a b) (consp x) (assoc-equal x a) (kwote-lst lst) (symbolp x) (pairlis$ a b) (return-last fn x y) (hide a) (mv-nth n x) (mv-list n x) (typespec-check ts x) (iff a b) (binary-+ a b) (unary-- a) (len x) (synp vars form term)) :namedp t)
other
(def-meta-extract evmeta-ev evmeta-ev-lst)
local
(local (defthm meta-extract-formula-w-elim (equal (meta-extract-formula-w name (w st)) (meta-extract-formula name st)) :hints (("Goal" :in-theory (enable meta-extract-formula meta-extract-formula-w)))))
evmeta-ev-of-match-treetheorem
(defthmd evmeta-ev-of-match-tree (b* (((mv ok alist) (match-tree pat x alist))) (implies ok (equal (evmeta-ev x a) (evmeta-ev (subst-tree pat alist) a)))) :hints (("Goal" :in-theory (enable match-tree-is-subst-tree))))
local
(local (in-theory (enable match-tree-obj-equals-subst-when-successful match-tree-alist-opener-theory)))
other
(define check-ev-of-fncall-args
((evfn symbolp) (evfn-lst symbolp)
(name symbolp)
(world plist-worldp))
(b* ((form (meta-extract-formula-w name world)) ((unless-match form
(implies (if (consp x)
(if (synp 'nil
'(syntaxp (not (equal a ''nil)))
'(if (not (equal a ''nil))
't
'nil))
(not (equal (car x) 'quote))
'nil)
'nil)
(equal ((:! evfn) x a)
((:! evfn) (cons (car x) (kwote-lst ((:! evfn-lst) (cdr x) a)))
'nil)))) nil))
t)
///
(local (def-match-tree-rewrites (implies (if (consp x)
(if (synp 'nil
'(syntaxp (not (equal a ''nil)))
'(if (not (equal a ''nil))
't
'nil))
(not (equal (car x) 'quote))
'nil)
'nil)
(equal ((:! evfn) x a)
((:! evfn) (cons (car x) (kwote-lst ((:! evfn-lst) (cdr x) a)))
'nil)))))
(defthm check-ev-of-fncall-args-correct
(implies (and (consp (evmeta-ev x1 a))
(not (equal (car (evmeta-ev x1 a)) 'quote))
(evmeta-ev-meta-extract-global-facts)
(check-ev-of-fncall-args evfn evfn-lst name (w state))
(not (eq evfn 'quote))
(not (eq evfn-lst 'quote)))
(equal (evmeta-ev (list evfn x1 a1) a)
(evmeta-ev `(,EVFN (cons (car ,X1) (kwote-lst (,EVFN-LST (cdr ,X1) ,A1)))
'nil)
a)))
:hints (("goal" :use ((:instance evmeta-ev-meta-extract-formula
(name name)
(st state)
(a `((x . ,(EVMETA-EV X1 A)) (a . ,(EVMETA-EV A1 A))))))
:in-theory (e/d (evmeta-ev-of-fncall-args)
(evmeta-ev-meta-extract-formula)))))
(assert-event (check-ev-of-fncall-args 'evmeta-ev
'evmeta-ev-lst
'evmeta-ev-of-fncall-args
(w state))))
other
(define check-ev-of-variable ((evfn symbolp) (name symbolp) (world plist-worldp)) (b* ((form (meta-extract-formula-w name world)) ((unless-match form (implies (symbolp x) (equal ((:! evfn) x a) (if x (cdr (assoc-equal x a)) 'nil)))) nil)) t) /// (defthm check-ev-of-variable-correct (implies (and (symbolp (evmeta-ev x1 a)) (evmeta-ev-meta-extract-global-facts) (check-ev-of-variable evfn name (w state)) (not (eq evfn 'quote))) (equal (evmeta-ev (list evfn x1 a1) a) (evmeta-ev `(if ,X1 (cdr (assoc-equal ,X1 ,A1)) 'nil) a))) :hints (("goal" :use ((:instance evmeta-ev-meta-extract-formula (name name) (st state) (a `((x . ,(EVMETA-EV X1 A)) (a . ,(EVMETA-EV A1 A)))))) :in-theory (e/d (evmeta-ev-of-fncall-args) (evmeta-ev-meta-extract-formula))))) (assert-event (check-ev-of-variable 'evmeta-ev 'evmeta-ev-of-variable (w state))))
other
(define check-ev-of-quote ((evfn symbolp) (name symbolp) (world plist-worldp)) (b* ((form (meta-extract-formula-w name world)) ((unless-match form (implies (if (consp x) (equal (car x) 'quote) 'nil) (equal ((:! evfn) x a) (car (cdr x))))) nil)) t) /// (defthm check-ev-of-quote-correct (implies (and (consp (evmeta-ev x1 a)) (equal (car (evmeta-ev x1 a)) 'quote) (evmeta-ev-meta-extract-global-facts) (check-ev-of-quote evfn name (w state)) (not (eq evfn 'quote))) (equal (evmeta-ev (list evfn x1 a1) a) (evmeta-ev `(car (cdr ,X1)) a))) :hints (("goal" :use ((:instance evmeta-ev-meta-extract-formula (name name) (st state) (a `((x . ,(EVMETA-EV X1 A)) (a . ,(EVMETA-EV A1 A)))))) :in-theory (e/d (evmeta-ev-of-fncall-args) (evmeta-ev-meta-extract-formula))))) (assert-event (check-ev-of-quote 'evmeta-ev 'evmeta-ev-of-quote (w state))))
other
(define check-ev-of-lambda
((evfn symbolp) (evfn-lst symbolp)
(name symbolp)
(world plist-worldp))
(b* ((form (meta-extract-formula-w name world)) ((unless-match form
(implies (if (consp x)
(consp (car x))
'nil)
(equal ((:! evfn) x a)
((:! evfn) (car (cdr (cdr (car x))))
(pairlis$ (car (cdr (car x))) ((:! evfn-lst) (cdr x) a)))))) nil))
t)
///
(defthm check-ev-of-lambda-correct
(implies (and (consp (evmeta-ev x1 a))
(consp (car (evmeta-ev x1 a)))
(evmeta-ev-meta-extract-global-facts)
(check-ev-of-lambda evfn evfn-lst name (w state))
(not (eq evfn 'quote))
(not (eq evfn-lst 'quote)))
(equal (evmeta-ev (list evfn x1 a1) a)
(evmeta-ev `(,EVFN (car (cdr (cdr (car ,X1))))
(pairlis$ (car (cdr (car ,X1))) (,EVFN-LST (cdr ,X1) ,A1)))
a)))
:hints (("goal" :use ((:instance evmeta-ev-meta-extract-formula
(name name)
(st state)
(a `((x . ,(EVMETA-EV X1 A)) (a . ,(EVMETA-EV A1 A))))))
:in-theory (e/d (evmeta-ev-of-fncall-args)
(evmeta-ev-meta-extract-formula)))))
(assert-event (check-ev-of-lambda 'evmeta-ev
'evmeta-ev-lst
'evmeta-ev-of-lambda
(w state))))
other
(define check-ev-of-nonsymbol-atom ((evfn symbolp) (name symbolp) (world plist-worldp)) (b* ((form (meta-extract-formula-w name world)) ((unless-match form (implies (if (not (consp x)) (not (symbolp x)) 'nil) (equal ((:! evfn) x a) 'nil))) nil)) t) /// (defthm check-ev-of-nonsymbol-atom-correct (implies (and (not (evmeta-ev x1 a)) (not (symbolp (evmeta-ev x1 a))) (evmeta-ev-meta-extract-global-facts) (check-ev-of-nonsymbol-atom evfn name (w state)) (not (eq evfn 'quote))) (equal (evmeta-ev (list evfn x1 a1) a) nil)) :hints (("goal" :use ((:instance evmeta-ev-meta-extract-formula (name name) (st state) (a `((x . ,(EVMETA-EV X1 A)) (a . ,(EVMETA-EV A1 A)))))) :in-theory (e/d (evmeta-ev-of-fncall-args) (evmeta-ev-meta-extract-formula))))) (assert-event (check-ev-of-nonsymbol-atom 'evmeta-ev 'evmeta-ev-of-nonsymbol-atom (w state))))
other
(define check-ev-of-bad-fncall ((evfn symbolp) (name symbolp) (world plist-worldp)) (b* ((form (meta-extract-formula-w name world)) ((unless-match form (implies (if (consp x) (if (not (consp (car x))) (not (symbolp (car x))) 'nil) 'nil) (equal ((:! evfn) x a) 'nil))) nil)) t) /// (defthm check-ev-of-bad-fncall-correct (implies (and (consp (evmeta-ev x1 a)) (not (consp (car (evmeta-ev x1 a)))) (not (symbolp (car (evmeta-ev x1 a)))) (evmeta-ev-meta-extract-global-facts) (check-ev-of-bad-fncall evfn name (w state)) (not (eq evfn 'quote))) (equal (evmeta-ev (list evfn x1 a1) a) nil)) :hints (("goal" :use ((:instance evmeta-ev-meta-extract-formula (name name) (st state) (a `((x . ,(EVMETA-EV X1 A)) (a . ,(EVMETA-EV A1 A)))))) :in-theory (e/d (evmeta-ev-of-fncall-args) (evmeta-ev-meta-extract-formula))))) (assert-event (check-ev-of-bad-fncall 'evmeta-ev 'evmeta-ev-of-bad-fncall (w state))))
other
(define ev-of-arglist ((n natp) (evfn symbolp) arglist-obj alist-obj) (if (zp n) nil (cons `(,EVFN ',(EC-CALL (CAR ARGLIST-OBJ)) ',ALIST-OBJ) (ev-of-arglist (1- n) evfn (ec-call (cdr arglist-obj)) alist-obj))) /// (defthm ev-of-arglist-is-ground (implies (and (syntaxp (not (equal a ''nil))) (not (equal evfn 'quote))) (equal (evmeta-ev-lst (ev-of-arglist n evfn arglist alist) a) (evmeta-ev-lst (ev-of-arglist n evfn arglist alist) nil))) :hints (("Goal" :in-theory (enable evmeta-ev-of-fncall-args)))))
other
(define ev-of-arglist-symb ((n natp) (evfn symbolp) arglist-term alist-term) (if (zp n) nil (cons `(,EVFN (car ,ARGLIST-TERM) ,ALIST-TERM) (ev-of-arglist-symb (1- n) evfn `(cdr ,ARGLIST-TERM) alist-term))) /// (defthm evmeta-ev-lst-of-ev-of-arglist-symb (implies (not (equal evfn 'quote)) (equal (evmeta-ev-lst (ev-of-arglist-symb n evfn arglist-term alist-term) a) (evmeta-ev-lst (ev-of-arglist n evfn (evmeta-ev arglist-term a) (evmeta-ev alist-term a)) nil))) :hints (("Goal" :in-theory (enable evmeta-ev-of-fncall-args ev-of-arglist)))))
other
(define ev-of-call-check-args (args (evfn symbolp) (arglist-term pseudo-termp) (alist-var pseudo-termp)) (b* (((when (atom args)) t) (form1 (car args)) ((unless-match form1 ((:! evfn) (car (:! arglist-term)) (:! alist-var))) nil)) (ev-of-call-check-args (cdr args) evfn `(cdr ,ARGLIST-TERM) alist-var)) /// (defthm ev-of-call-check-args-correct (implies (and (ev-of-call-check-args args evfn arglist-term alist-var) (not (equal evfn 'quote))) (equal (evmeta-ev-lst args a) (evmeta-ev-lst (ev-of-arglist (len args) evfn (evmeta-ev arglist-term a) (evmeta-ev alist-var a)) nil))) :hints (("Goal" :in-theory (enable ev-of-arglist evmeta-ev-of-fncall-args)))))
other
(define check-ev-of-call
((evfn symbolp) (fn symbolp)
(arity natp)
(name symbolp)
(world plist-worldp))
(b* ((form (meta-extract-formula-w name world)) ((unless-match form
(implies (if (consp x)
(equal (car x) '(:! fn))
'nil)
(equal ((:! evfn) x a) ((:! fn) :? args)))) nil))
(and (eql (mbe :logic (nfix arity) :exec arity) (len args))
(ev-of-call-check-args args evfn '(cdr x) 'a)))
///
(defthm check-ev-of-call-correct
(implies (and (check-ev-of-call evfn fn arity name (w state))
(consp (evmeta-ev x1 a))
(equal (car (evmeta-ev x1 a)) fn)
(not (equal fn 'quote))
(evmeta-ev-meta-extract-global-facts)
(not (equal evfn 'quote)))
(equal (evmeta-ev (list evfn x1 a1) a)
(evmeta-ev (cons fn
(ev-of-arglist (nfix arity)
evfn
(cdr (evmeta-ev x1 a))
(evmeta-ev a1 a)))
a)))
:hints (("goal" :use ((:instance evmeta-ev-meta-extract-formula
(name name)
(st state)
(a `((x . ,(EVMETA-EV X1 A)) (a . ,(EVMETA-EV A1 A))))))
:in-theory (e/d (evmeta-ev-of-fncall-args)
(evmeta-ev-meta-extract-formula)))))
(assert-event (check-ev-of-call 'evmeta-ev
'synp
3
'evmeta-ev-of-synp-call
(w state))))
other
(define check-ev-of-call-weak
((evfn symbolp) (fn symbolp)
(name symbolp)
(world plist-worldp))
(b* ((form (meta-extract-formula-w name world)) ((unless-match form
(implies (if (consp x)
(equal (car x) '(:! fn))
'nil)
(equal ((:! evfn) x a) (:? rhs)))) nil))
rhs)
///
(defthm check-ev-of-call-weak-correct
(implies (and (check-ev-of-call-weak evfn fn name (w state))
(consp (evmeta-ev x1 a))
(equal (car (evmeta-ev x1 a)) fn)
(not (equal fn 'quote))
(evmeta-ev-meta-extract-global-facts)
(not (equal evfn 'quote)))
(equal (evmeta-ev (list evfn x1 a1) a)
(evmeta-ev `((lambda (x a)
,(CHECK-EV-OF-CALL-WEAK EVFN FN NAME (W STATE))) ,X1
,A1)
a)))
:hints (("goal" :use ((:instance evmeta-ev-meta-extract-formula
(name name)
(st state)
(a `((x . ,(EVMETA-EV X1 A)) (a . ,(EVMETA-EV A1 A))))))
:in-theory (e/d (evmeta-ev-of-fncall-args)
(evmeta-ev-meta-extract-formula)))))
(local (progn (defevaluator test-cwh-ev
test-cwh-ev-lst
((cons-with-hint x y hint))
:namedp t)
(assert-event (check-ev-of-call-weak 'test-cwh-ev
'cons-with-hint
'test-cwh-ev-of-cons-with-hint-call
(w state))))))
is-n-cdrs-of-xfunction
(defun is-n-cdrs-of-x (n term x) (if (zp n) (eq term x) (case-match term (('cdr inner) (is-n-cdrs-of-x (1- n) inner x)))))
list-of-ev-apps-pfunction
(defun list-of-ev-apps-p (lst evfn index x) (if (atom lst) (eq lst nil) (let ((first (car lst))) (case-match first ((!evfn ('car n-cdrs-of-x) 'a) (and (is-n-cdrs-of-x (1+ index) n-cdrs-of-x x) (list-of-ev-apps-p (cdr lst) evfn (1+ index) x)))))))
ev-collect-apply-lemmas1function
(defun ev-collect-apply-lemmas1 (lemmas evfn evlstfn) (if (atom lemmas) nil (b* ((rule (car lemmas)) (hyps (access rewrite-rule rule :hyps)) (equiv (access rewrite-rule rule :equiv)) (lhs (access rewrite-rule rule :lhs)) (rhs (access rewrite-rule rule :rhs)) (rune (access rewrite-rule rule :rune)) (aggregate (list hyps rhs)) (rest (ev-collect-apply-lemmas1 (cdr lemmas) evfn evlstfn))) (if (eq equiv 'equal) (case-match lhs ((!evfn quote (x a)) (case-match aggregate (('((consp x) (synp 'nil '(syntaxp (not (equal a ''nil))) '(if (not (equal a ''nil)) 't 'nil)) (not (equal (car x) 'quote))) (!evfn ('cons '(car x) ('kwote-lst (!evlstfn quote ((cdr x) a)))) ''nil)) (hons-acons :expand-fncall rune rest)) (('((symbolp x)) '(if x (cdr (assoc-equal x a)) 'nil)) (hons-acons :lookup-var rune rest)) (('((consp x) (equal (car x) 'quote)) '(car (cdr x))) (hons-acons :quote rune rest)) (('((consp x) (consp (car x))) (!evfn '(car (cdr (cdr (car x)))) ('pairlis$ '(car (cdr (car x))) (!evlstfn quote ((cdr x) a))))) (hons-acons :lambda rune rest)) (((('consp 'x) ('equal ('car 'x) ''return-last)) (!evfn quote ((car (cdr (cdr (cdr x)))) a))) (hons-acons 'return-last (cons 3 rune) rest)) (((('consp 'x) ('equal ('car 'x) ''mv-list)) (!evfn quote ((car (cdr (cdr x))) a))) (hons-acons 'mv-list (cons 2 rune) rest)) (((('consp 'x) ('equal ('car 'x) ''cons-with-hint)) ('cons (!evfn quote ((car (cdr x)) a)) (!evfn quote ((car (cdr (cdr x))) a)))) (hons-acons 'cons-with-hint (cons 2 rune) rest)) (((('consp 'x) ('equal ('car 'x) ''the-check)) (!evfn quote ((car (cdr (cdr (cdr x)))) a))) (hons-acons 'the-check (cons 3 rune) rest)) (((('consp 'x) ('equal ('car 'x) ('quote fn))) (fn . list-of-ev-apps)) (if (list-of-ev-apps-p list-of-ev-apps evfn 0 'x) (hons-acons fn (cons (len list-of-ev-apps) rune) rest) rest)) (& rest))) ((!evlstfn quote (x-lst a)) (case-match aggregate (('((not (consp x-lst))) ''nil) (hons-acons :lst-atom rune rest)) (('((consp x-lst)) ('cons (!evfn quote ((car x-lst) a)) (!evlstfn quote ((cdr x-lst) a)))) (hons-acons :lst-cons rune rest)) (& rest))) (& rest)) rest))))
ev-collect-apply-lemmasfunction
(defun ev-collect-apply-lemmas (evfn evlstfn world) (ev-collect-apply-lemmas1 (append (fgetprop evfn 'lemmas nil world) (fgetprop evlstfn 'lemmas nil world)) evfn evlstfn))
evmeta-ev-of-fncall-args-even-if-alist-is-niltheorem
(defthmd evmeta-ev-of-fncall-args-even-if-alist-is-nil (implies (and (syntaxp (not (and (consp args) (eq (car args) 'kwote-lst)))) (not (equal fn 'quote))) (equal (evmeta-ev (cons fn args) a) (evmeta-ev (cons fn (kwote-lst (evmeta-ev-lst args a))) nil))) :hints (("Goal" :in-theory (enable evmeta-ev-of-fncall-args))))
kwote-lst-of-constheorem
(defthmd kwote-lst-of-cons (equal (kwote-lst (cons a b)) (cons (kwote a) (kwote-lst b))))
*def-evaluator-expander-theory*constant
(defconst *def-evaluator-expander-theory* '((:definition kwote) (:definition nfix) (:definition synp) (:definition subst-tree) (:executable-counterpart equal) (:executable-counterpart kwote-lst) (:executable-counterpart match-tree-binder-p) (:rewrite car-cons) (:rewrite cdr-cons) (:rewrite check-ev-of-call-correct) (:rewrite check-ev-of-call-weak-correct) (:rewrite evmeta-ev-lst-of-atom) (:rewrite evmeta-ev-lst-of-cons) (:rewrite evmeta-ev-lst-of-ev-of-arglist-symb) (:rewrite evmeta-ev-of-cons-call) (:rewrite evmeta-ev-of-match-tree) (:rewrite evmeta-ev-of-lambda) (:rewrite evmeta-ev-of-fncall-args) (:rewrite evmeta-ev-of-quote) (:rewrite kwote-lst-of-cons) (:rewrite not-quote-by-match-tree-restrictions) (:executable-counterpart intersectp-equal) (:executable-counterpart match-tree-restrictions) (:type-prescription check-ev-of-call) (:type-prescription ev-of-arglist-symb) (:type-prescription len)))
*def-evaluator-expander-guard-theory*constant
(defconst *def-evaluator-expander-guard-theory* '((:compound-recognizer natp-compound-recognizer) (:definition eq) (:definition hons-get) (:definition kwote) (:definition state-p) (:executable-counterpart equal) (:executable-counterpart car) (:executable-counterpart cdr) (:executable-counterpart consp) (:executable-counterpart eqlablep) (:executable-counterpart if) (:executable-counterpart match-tree-binders) (:executable-counterpart member-equal) (:executable-counterpart intersectp-equal) (:executable-counterpart match-tree-restrictions) (:executable-counterpart not) (:executable-counterpart symbol-alistp) (:rewrite match-tree-binders-bound) (:rewrite symbol-alistp-match-tree) (:rewrite symbolp-by-match-tree-restrictions) (:rewrite assoc-eql-exec-is-assoc-equal) (:rewrite plist-worldp-w-state) (:type-prescription ev-of-arglist-symb) (:type-prescription hons-assoc-equal) (:type-prescription len) (:type-prescription state-p1)))
*def-evaluator-expander-form*constant
(defconst *def-evaluator-expander-form* '(progn (make-event `(defconst thm-alist-const ',(EV-COLLECT-APPLY-LEMMAS 'EVFN NIL (W STATE)))) (define metafn (x mfc state) (declare (ignorable mfc)) :guard-hints (("goal" :in-theory *def-evaluator-expander-guard-theory*)) (b* (((unless-match x (evfn (:? form) (:? a))) x) ((mv fn ?args) (b* (((when-match form (cons '(:?f fn) (:? args))) (mv fn args)) ((when-match form '((:?f fn) :? args)) (mv fn (kwote args)))) (mv nil nil))) ((unless fn) x) (pair (hons-get fn thm-alist-const)) ((unless (and pair (consp (cdr pair)) (consp (cddr pair)) (consp (cdddr pair)) (symbolp (caddr (cdr pair))))) x) (arity (len (getpropc fn 'formals t (w state)))) ((unless (check-ev-of-call 'evfn fn arity (caddr (cdr pair)) (w state))) (b* ((rhs (check-ev-of-call-weak 'evfn fn (caddr (cdr pair)) (w state))) ((unless rhs) x)) `((lambda (x a) ,RHS) ,FORM ,A)))) (cons fn (ev-of-arglist-symb arity 'evfn args a))) /// (defthm metafn-correct (implies (evmeta-ev-meta-extract-global-facts) (equal (evmeta-ev x a) (evmeta-ev (metafn x mfc state) a))) :hints (("goal" :do-not-induct t :in-theory (cons 'metafn *def-evaluator-expander-theory*)) (and stable-under-simplificationp '(:in-theory (cons 'evmeta-ev-of-fncall-args-even-if-alist-is-nil (set-difference-equal *def-evaluator-expander-theory* '((:definition kwote-lst) (:rewrite kwote-lst-of-cons))))))) :rule-classes ((:meta :trigger-fns (evfn))) :otf-flg t))))
def-evaluator-expander-fnfunction
(defun def-evaluator-expander-fn (evfn metafn metafn-correct thm-alist-const) (b* ((metafn (or metafn (intern-in-package-of-symbol (concatenate 'string (symbol-name evfn) "-EXPANDER") evfn))) (metafn-correct (or metafn-correct (intern-in-package-of-symbol (concatenate 'string (symbol-name metafn) "-CORRECT") metafn))) (thm-alist-const (or thm-alist-const (intern-in-package-of-symbol (concatenate 'string "*" (symbol-name evfn) "-THM-ALIST*") evfn)))) (sublis `((evfn . ,EVFN) (metafn . ,METAFN) (metafn-correct . ,METAFN-CORRECT) (thm-alist-const . ,THM-ALIST-CONST)) *def-evaluator-expander-form*)))
def-evaluator-expandermacro
(defmacro def-evaluator-expander (evfn &key metafn metafn-correct thm-alist-const) (def-evaluator-expander-fn evfn metafn metafn-correct thm-alist-const))
local
(local (progn (defevaluator test-ev test-ev-lst ((if a b c) (equal p q) (cons-with-hint x y hint)) :namedp t) (encapsulate nil (local (in-theory nil)) (def-evaluator-expander test-ev)) (defthm test-ev-of-equal (equal (test-ev (list 'equal x y) a) (equal (test-ev x a) (test-ev y a))) :hints (("Goal" :in-theory (disable test-ev-of-equal-call)))) (defthm test-ev-of-cons-with-hint (equal (test-ev (list 'cons-with-hint x y z) a) (cons-with-hint (test-ev x a) (test-ev y a) (test-ev z a))) :hints (("Goal" :in-theory (disable test-ev-of-cons-with-hint-call))))))