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 isodata-gen-lemma-instance-x1...xn-to-fn-of-x1...xn (fn) (declare (xargs :guard (member-eq fn '(forth back)))) (b* ((name (packn (list 'isodata-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))) (isodata-gen-fn-of-terms (packn (list 'isodata-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-isomaps isodata-symbol-isomap-alistp) (wrld plist-worldp)) (cons ':guard (cons '(= (len (formals old$ wrld)) (len arg-isomaps)) (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 isodata-gen-fn-of-terms '(x1...xn arg-isomaps)) '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))))))))))))))