Generate the theorem that relates the new and old functions.
(restrict-gen-new-to-old old restriction new new-to-old new-to-old-enable old-to-new wrld) → (mv local-event exported-event)
The macro used to introduce the theorem is determined by whether the theorem must be enabled or not.
The formula of the theorem equates new and old functions under the restricting predicate, as described in the documentation.
The theorem is easily proved from the
Function:
(defun restrict-gen-new-to-old (old restriction new new-to-old new-to-old-enable old-to-new wrld) (declare (xargs :guard (and (symbolp old) (pseudo-termp restriction) (symbolp new) (symbolp new-to-old) (booleanp new-to-old-enable) (symbolp old-to-new) (plist-worldp wrld)))) (let ((__function__ 'restrict-gen-new-to-old)) (declare (ignorable __function__)) (b* ((formals (formals old wrld)) (formula (implicate restriction (cons 'equal (cons (cons new formals) (cons (cons old formals) 'nil))))) (formula (untranslate formula t wrld)) (hints (cons (cons '"Goal" (cons ':in-theory (cons (cons 'quote (cons (cons old-to-new 'nil) 'nil)) 'nil))) 'nil))) (evmac-generate-defthm new-to-old :formula formula :hints hints :enable new-to-old-enable))))