Generate a lemma instance where
each variable
(isodata-gen-lemma-instance-x1...xn-to-forth-of-x1...xn lemma old$ arg-isomaps wrld) → lemma-instance
Function:
(defun isodata-gen-lemma-instance-x1...xn-to-forth-of-x1...xn (lemma old$ arg-isomaps wrld) (declare (xargs :guard (and (or (symbolp lemma) (symbol-listp lemma)) (symbolp old$) (isodata-symbol-isomap-alistp arg-isomaps) (plist-worldp wrld)))) (declare (xargs :guard (= (len (formals old$ wrld)) (len arg-isomaps)))) (let ((__function__ 'isodata-gen-lemma-instance-x1...xn-to-forth-of-x1...xn)) (declare (ignorable __function__)) (b* ((x1...xn (formals old$ wrld)) (forth-of-x1...xn (isodata-gen-forth-of-terms x1...xn arg-isomaps)) (inst (alist-to-doublets (pairlis$ x1...xn forth-of-x1...xn)))) (cons ':instance (cons lemma (cons ':extra-bindings-ok inst))))))
Theorem:
(defthm true-listp-of-isodata-gen-lemma-instance-x1...xn-to-forth-of-x1...xn (b* ((lemma-instance (isodata-gen-lemma-instance-x1...xn-to-forth-of-x1...xn lemma old$ arg-isomaps wrld))) (true-listp lemma-instance)) :rule-classes :rewrite)