Generate a function to generate certain kinds of lemma instances.
The function generated by this macro
generates a lemma instance of the form
Macro:
(defmacro expdata-gen-lemma-instance-x1...xn-to-fn-of-x1...xn (fn) (declare (xargs :guard (member-eq fn '(forth back)))) (b* ((name (packn (list 'expdata-gen-lemma-instance-x1...xn-to- fn '-of-x1...xn))) (string (str::downcase-string (symbol-name fn))) (fn-of-x1...xn (packn (list fn '-of-x1...xn))) (expdata-gen-fn-of-terms (packn (list 'expdata-gen- fn '-of-terms)))) (cons 'define (cons name (cons '((lemma (or (symbolp lemma) (symbol-listp lemma)) "Lemma to generate an instance of.") (old$ symbolp) (arg-surjmaps expdata-symbol-surjmap-alistp) (wrld plist-worldp)) (cons ':guard (cons '(= (len (formals old$ wrld)) (len arg-surjmaps)) (cons ':returns (cons '(lemma-instance true-listp) (cons ':verify-guards (cons 'nil (cons ':short (cons (str::cat "Generate a lemma instance where each variable @('xi') is instantiated with @('(" string "i xi)').") (cons (cons 'b* (cons (cons '(x1...xn (formals old$ wrld)) (cons (cons fn-of-x1...xn (cons (cons expdata-gen-fn-of-terms '(x1...xn arg-surjmaps)) 'nil)) (cons (cons 'inst (cons (cons 'alist-to-doublets (cons (cons 'pairlis$ (cons 'x1...xn (cons fn-of-x1...xn 'nil))) 'nil)) 'nil)) 'nil))) '((cons ':instance (cons lemma (cons ':extra-bindings-ok inst)))))) 'nil))))))))))))))