Generate the hints to prove
the lemma use to prove
(isodata-gen-new-to-old-lemma-hints appcond-thm-names old$ arg-isomaps res-isomaps new$ old-fn-unnorm-name new-fn-unnorm-name wrld) → hints
See isodata-gen-new-to-old-lemma for details.
Function:
(defun isodata-gen-new-to-old-lemma-hints (appcond-thm-names old$ arg-isomaps res-isomaps new$ old-fn-unnorm-name new-fn-unnorm-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$) (symbolp old-fn-unnorm-name) (symbolp new-fn-unnorm-name) (plist-worldp wrld)))) (let ((__function__ 'isodata-gen-new-to-old-lemma-hints)) (declare (ignorable __function__)) (if (recursivep old$ nil wrld) (b* ((rec-calls (recursive-calls old$ wrld)) (oldp-of-rec-call-args (cdr (assoc-eq :oldp-of-rec-call-args appcond-thm-names))) (oldp-of-old (cdr (assoc-eq :oldp-of-old appcond-thm-names))) (instance-oldp-of-rec-call-args (isodata-gen-lemma-instance-x1...xn-to-back-of-x1...xn oldp-of-rec-call-args old$ arg-isomaps wrld)) (instances-oldp-of-old (isodata-gen-lemma-instances-x1...xn-to-rec-call-args-back oldp-of-old rec-calls old$ arg-isomaps wrld)) (instances-back-image (isodata-gen-back-image-instances-to-x1...xn arg-isomaps wrld)) (instances-forth-image (isodata-gen-all-forth-image-instances-to-terms-back rec-calls old$ arg-isomaps wrld)) (instances-back-of-forth (isodata-gen-all-back-of-forth-instances-to-terms-back rec-calls old$ arg-isomaps wrld)) (instances-back-of-forth-res (isodata-gen-all-back-of-forth-instances-to-mv-nth old$ rec-calls arg-isomaps res-isomaps wrld))) (cons (cons '"Goal" (cons ':in-theory (cons (cons 'quote (cons (cons old-fn-unnorm-name (cons new-fn-unnorm-name (cons (cons ':induction (cons new$ 'nil)) 'nil))) 'nil)) (cons ':induct (cons (cons new$ (formals old$ wrld)) 'nil))))) (cons (cons 'quote (cons (cons ':use (cons (cons instance-oldp-of-rec-call-args (append instances-oldp-of-old (append instances-back-image (append instances-forth-image (append instances-back-of-forth instances-back-of-forth-res))))) 'nil)) 'nil)) 'nil))) (cons (cons '"Goal" (cons ':in-theory (cons (cons 'quote (cons (cons old-fn-unnorm-name (cons new-fn-unnorm-name 'nil)) 'nil)) 'nil))) 'nil))))