Generate functions to generate certain kinds of lemma instances.
The first function generated by this macro
generates a list of lemma instances of the form
The second function generated by this macro
calls the first function once for each recursively call of
Macro:
(defmacro expdata-gen-thm-instances-to-terms-back (thm) (declare (xargs :guard (member-eq thm '(forth-image back-of-forth forth-guard)))) (b* ((name1 (packn (list 'expdata-gen- thm '-instances-to-terms-back))) (name1-aux (packn (list name1 '-aux))) (name2 (packn (list 'expdata-gen-all- thm '-instances-to-terms-back))) (name1-string (str::downcase-string (symbol-name name1))) (thm-selector (packn (list 'expdata-surjmap-> thm))) (thm-string (case thm (forth-image "forthi-image") (back-of-forth "backi-of-forthi") (forth-guard "forthi-guard") (t (impossible))))) (cons 'progn (cons (cons 'define (cons name1 (cons '((terms pseudo-term-listp) (old$ symbolp) (arg-surjmaps expdata-symbol-surjmap-alistp) (wrld plist-worldp)) (cons ':guard (cons '(= (len terms) (len arg-surjmaps)) (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 @('forthi') with a given term @('termi') in which @('x1'), ..., @('xn') are replaced with @('(back1 x1)'), ..., @('(backn xn)').") (cons (cons 'b* (cons '((x1...xn (formals old$ wrld)) (back-of-x1...xn (expdata-gen-back-of-terms x1...xn arg-surjmaps))) (cons (cons name1-aux '(terms arg-surjmaps x1...xn back-of-x1...xn wrld)) 'nil))) (cons ':prepwork (cons (cons (cons 'define (cons name1-aux (cons '((terms pseudo-term-listp) (arg-surjmaps expdata-symbol-surjmap-alistp) (x1...xn symbol-listp) (back-of-x1...xn pseudo-term-listp) (wrld plist-worldp)) (cons ':guard (cons '(= (len terms) (len arg-surjmaps)) (cons ':returns (cons '(lemma-instances true-list-listp) (cons ':verify-guards (cons 'nil (cons (cons 'b* (cons (cons '((when (endp terms)) nil) (cons '(term (car terms)) (cons '(surjmap (cdar arg-surjmaps)) (cons (cons thm (cons (cons thm-selector '(surjmap)) 'nil)) (cons '(var (expdata-formal-of-forth surjmap wrld)) (cons '(term-with-back (subcor-var x1...xn back-of-x1...xn term)) (cons (cons 'instance (cons (cons 'list (cons ':instance (cons thm '(:extra-bindings-ok (list var term-with-back))))) 'nil)) (cons (cons 'instances (cons (cons name1-aux '((cdr terms) (cdr arg-surjmaps) x1...xn back-of-x1...xn wrld)) 'nil)) 'nil)))))))) '((cons instance instances)))) 'nil)))))))))) 'nil) 'nil)))))))))))))) (cons (cons 'define (cons name2 (cons '((rec-calls pseudo-tests-and-call-listp) (old$ symbolp) (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 the concatenation of all the @('n * r') lemma instances generated by @('" name1-string "') for all the recursive call arguments of @('old') passed as the @('terms') input.") (cons (cons 'b* (cons (cons '((when (endp rec-calls)) nil) (cons '(tests-and-call (car rec-calls)) (cons '(rec-call (access tests-and-call tests-and-call :call)) (cons '(updates (fargs rec-call)) (cons (cons 'instances (cons (cons name1 '(updates old$ arg-surjmaps wrld)) 'nil)) (cons (cons 'more-instances (cons (cons name2 '((cdr rec-calls) old$ arg-surjmaps wrld)) 'nil)) 'nil)))))) '((append instances more-instances)))) 'nil)))))))))) 'nil)))))