Generate a function to generate certain kinds of lemma instances.
The function generated by this macro
generates a list of lemma instances of the form
Macro:
(defmacro expdata-gen-thm-instances-to-x1...xn (thm) (declare (xargs :guard (member-eq thm '(forth-image back-image back-of-forth newp-guard forth-guard back-guard)))) (b* ((name (packn (list 'expdata-gen- thm '-instances-to-x1...xn))) (thm-selector (packn (list 'expdata-surjmap-> thm))) (thm-string (case thm (forth-image "forthi-image") (back-image "backi-image") (back-of-forth "backi-of-forthi") (newp-guard "newpi-guard") (forth-guard "forthi-guard") (back-guard "backi-guard") (t (impossible)))) (fn (case thm (forth-image 'forth) (back-image 'back) (back-of-forth 'forth) (newp-guard 'newp) (forth-guard 'forth) (back-guard 'back) (t (impossible)))) (fn-selector (packn (list 'expdata-surjmap-> fn))) (fn-string (str::downcase-string (symbol-name fn))) (param (packn (list fn '-arg)))) (cons 'define (cons name (cons '((arg-surjmaps expdata-symbol-surjmap-alistp) (wrld plist-worldp)) (cons ':returns (cons '(lemma-instances true-list-listp) (cons ':verify-guards (cons 'nil (cons ':short (cons (str::cat "Generate @('n') lemma instances such that the @('i')-th instance is of theorem @('" thm-string "') and instantiates the formal parameter of @('" fn-string "') with @('xi').") (cons (cons 'b* (cons (cons '((when (endp arg-surjmaps)) nil) (cons '(arg (caar arg-surjmaps)) (cons '(surjmap (cdar arg-surjmaps)) (cons (cons thm (cons (cons thm-selector '(surjmap)) 'nil)) (cons (cons param (cons (cons 'expdata-formal-of-unary (cons (cons fn-selector '(surjmap)) '(wrld))) 'nil)) (cons (cons 'instance (cons (cons 'list (cons ':instance (cons thm (cons ':extra-bindings-ok (cons (cons 'list (cons param '(arg))) 'nil))))) 'nil)) (cons (cons 'instances (cons (cons name '((cdr arg-surjmaps) wrld)) 'nil)) 'nil))))))) '((cons instance instances)))) 'nil))))))))))))