Generate the hints to prove
the lemma used to prove
(isodata-gen-old-to-new-lemma-hints appcond-thm-names old$ arg-isomaps res-isomaps new-to-old-lemma-name wrld) → hints
See isodata-gen-old-to-new-lemma for details.
Note that, compared to the design notes,
we use the new-to-old lemma instead of
Function:
(defun isodata-gen-old-to-new-lemma-hints (appcond-thm-names old$ arg-isomaps res-isomaps new-to-old-lemma-name wrld) (declare (xargs :guard (and (symbol-symbol-alistp appcond-thm-names) (symbolp old$) (isodata-symbol-isomap-alistp arg-isomaps) (isodata-pos-isomap-alistp res-isomaps) (symbolp new-to-old-lemma-name) (plist-worldp wrld)))) (let ((__function__ 'isodata-gen-old-to-new-lemma-hints)) (declare (ignorable __function__)) (b* ((oldp-of-old (cdr (assoc-eq :oldp-of-old appcond-thm-names))) (instances-forth-image (isodata-gen-forth-image-instances-to-x1...xn arg-isomaps wrld)) (instances-back-of-forth (isodata-gen-back-of-forth-instances-to-x1...xn arg-isomaps wrld)) (instance-new-to-old-lemma (isodata-gen-lemma-instance-x1...xn-to-forth-of-x1...xn new-to-old-lemma-name old$ arg-isomaps wrld)) (x1...xn (formals old$ wrld)) (old-call (fcons-term old$ x1...xn)) (instances-back-of-forth-res (isodata-gen-back-of-forth-instances-to-mv-nth old-call res-isomaps wrld))) (cons (cons '"Goal" (cons ':in-theory (cons 'nil (cons ':use (cons (append instances-forth-image (append instances-back-of-forth (cons instance-new-to-old-lemma (cons oldp-of-old instances-back-of-forth-res)))) 'nil))))) 'nil))))