		Search-engine friendly clone of the ACL2 documentation.

Expdata-event-generation

Expdata-gen-new-to-old-thm

Generate the new-to-old theorem.

Signature
(expdata-gen-new-to-old-thm old$ arg-surjmaps res-surjmaps new$ new-to-old$ new-to-old-enable$ appcond-thm-names old-fn-unnorm-name new-fn-unnorm-name wrld) → (mv new-to-old-local-event new-to-old-exported-event)
Arguments: old$ — Guard (symbolp old$).; arg-surjmaps — Guard (expdata-symbol-surjmap-alistp arg-surjmaps).; res-surjmaps — Guard (expdata-pos-surjmap-alistp res-surjmaps).; new$ — Guard (symbolp new$).; new-to-old$ — Guard (symbolp new-to-old$).; new-to-old-enable$ — Guard (booleanp new-to-old-enable$).; appcond-thm-names — Guard (symbol-symbol-alistp appcond-thm-names).; old-fn-unnorm-name — Guard (symbolp old-fn-unnorm-name).; new-fn-unnorm-name — Guard (symbolp new-fn-unnorm-name).; wrld — Guard (plist-worldp wrld).
Returns: new-to-old-local-event — A pseudo-event-formp.; new-to-old-exported-event — A pseudo-event-formp.

Definitions and Theorems

Function: expdata-gen-new-to-old-thm

(defun expdata-gen-new-to-old-thm
       (old$ arg-surjmaps res-surjmaps
             new$ new-to-old$ new-to-old-enable$
             appcond-thm-names old-fn-unnorm-name
             new-fn-unnorm-name wrld)
 (declare
     (xargs :guard (and (symbolp old$)
                        (expdata-symbol-surjmap-alistp arg-surjmaps)
                        (expdata-pos-surjmap-alistp res-surjmaps)
                        (symbolp new$)
                        (symbolp new-to-old$)
                        (booleanp new-to-old-enable$)
                        (symbol-symbol-alistp appcond-thm-names)
                        (symbolp old-fn-unnorm-name)
                        (symbolp new-fn-unnorm-name)
                        (plist-worldp wrld))))
 (let ((__function__ 'expdata-gen-new-to-old-thm))
   (declare (ignorable __function__))
   (b* ((formula (expdata-gen-new-to-old-thm-formula
                      old$
                      arg-surjmaps res-surjmaps new$ wrld))
        (formula (untranslate formula t wrld))
        (hints (expdata-gen-new-to-old-thm-hints
                    appcond-thm-names old$ arg-surjmaps
                    res-surjmaps new$ old-fn-unnorm-name
                    new-fn-unnorm-name wrld)))
     (evmac-generate-defthm new-to-old$
                            :formula formula
                            :hints hints
                            :enable new-to-old-enable$))))