Generate the theorem that relates the old and new function.
(parteval-gen-old-to-new-thm old$ static$ new-name$ thm-name$ thm-enable$ case new-formals 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 theorem is an implication,
whose antecedent is
The hints follow the proof
in the design notes and in
Function:
(defun parteval-gen-old-to-new-thm (old$ static$ new-name$ thm-name$ thm-enable$ case new-formals wrld) (declare (xargs :guard (and (symbolp old$) (symbol-alistp static$) (symbolp new-name$) (symbolp thm-name$) (booleanp thm-enable$) (member case '(1 2 3)) (symbol-listp new-formals) (plist-worldp wrld)))) (let ((__function__ 'parteval-gen-old-to-new-thm)) (declare (ignorable __function__)) (b* ((equalities (parteval-gen-static-equalities static$)) (antecedent (conjoin equalities)) (consequent (cons 'equal (cons (cons old$ (formals old$ wrld)) (cons (cons new-name$ new-formals) 'nil)))) (formula (implicate antecedent consequent)) (formula (untranslate formula t wrld)) (hints (case case (1 (cons (cons '"Goal" (cons ':in-theory (cons (cons 'quote (cons (cons old$ (cons new-name$ 'nil)) 'nil)) 'nil))) 'nil)) (2 (cons (cons '"Goal" (cons ':in-theory (cons (cons 'quote (cons (cons old$ (cons new-name$ 'nil)) 'nil)) (cons ':induct (cons (cons new-name$ new-formals) 'nil))))) 'nil)) (3 (cons (cons '"Goal" (cons ':in-theory (cons (cons 'quote (cons (cons new-name$ 'nil) 'nil)) 'nil))) 'nil)) (t (impossible))))) (evmac-generate-defthm thm-name$ :formula formula :hints hints :enable thm-enable$))))