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 isodata-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 'isodata-gen- thm '-instances-to-x1...xn))) (thm-selector (packn (list 'isodata-isomap-> 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 'isodata-isomap-> fn))) (fn-string (str::downcase-string (symbol-name fn))) (param (packn (list fn '-arg)))) (cons 'define (cons name (cons '((arg-isomaps isodata-symbol-isomap-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-isomaps)) nil) (cons '(arg (caar arg-isomaps)) (cons '(isomap (cdar arg-isomaps)) (cons (cons thm (cons (cons thm-selector '(isomap)) 'nil)) (cons (cons param (cons (cons 'isodata-formal-of-unary (cons (cons fn-selector '(isomap)) '(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-isomaps) wrld)) 'nil)) 'nil))))))) '((cons instance instances)))) 'nil))))))))))))