Generate the lemma use to prove
(isodata-gen-new-to-old-lemma old$ arg-isomaps res-isomaps new$ appcond-thm-names old-fn-unnorm-name new-fn-unnorm-name names-to-avoid wrld) → (mv new-to-old-lemma-name new-to-old-lemma-event updated-names-to-avoid)
This is generated only if
Function:
(defun isodata-gen-new-to-old-lemma (old$ arg-isomaps res-isomaps new$ appcond-thm-names old-fn-unnorm-name new-fn-unnorm-name names-to-avoid wrld) (declare (xargs :guard (and (symbolp old$) (isodata-symbol-isomap-alistp arg-isomaps) (isodata-pos-isomap-alistp res-isomaps) (symbolp new$) (symbol-symbol-alistp appcond-thm-names) (symbolp old-fn-unnorm-name) (symbolp new-fn-unnorm-name) (symbol-listp names-to-avoid) (plist-worldp wrld)))) (let ((__function__ 'isodata-gen-new-to-old-lemma)) (declare (ignorable __function__)) (b* (((mv name names-to-avoid) (fresh-logical-name-with-$s-suffix 'new-to-old-lemma nil names-to-avoid wrld)) (formula (isodata-gen-new-to-old-lemma-formula old$ arg-isomaps res-isomaps new$ wrld)) (hints (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)) ((mv event &) (evmac-generate-defthm name :formula formula :hints hints :enable nil))) (mv name event names-to-avoid))))