Generate the theorem that relates the old and new functions.
(casesplit-gen-old-to-new-thm old$ theorems$ new-name$ thm-name$ thm-enable$ appcond-thm-names new-unnorm-name 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 old and new function.
The theorem is proved as shown in the template file.
The
Function:
(defun casesplit-gen-old-to-new-thm (old$ theorems$ new-name$ thm-name$ thm-enable$ appcond-thm-names new-unnorm-name wrld) (declare (xargs :guard (and (symbolp old$) (symbol-listp theorems$) (symbolp new-name$) (symbolp thm-name$) (booleanp thm-enable$) (symbol-symbol-alistp appcond-thm-names) (symbolp new-unnorm-name) (plist-worldp wrld)))) (let ((__function__ 'casesplit-gen-old-to-new-thm)) (declare (ignorable __function__)) (b* ((formals (formals old$ wrld)) (formula (cons 'equal (cons (cons old$ formals) (cons (cons new-name$ formals) 'nil)))) (formula (untranslate formula t wrld)) (thm-hyp-appcond-thm-names (take (len theorems$) appcond-thm-names)) (hints (cons (cons '"Goal" (cons ':in-theory (cons (cons 'quote (cons (cons new-unnorm-name 'nil) 'nil)) (cons ':use (cons (append (strip-cdrs thm-hyp-appcond-thm-names) theorems$) 'nil))))) 'nil))) (evmac-generate-defthm thm-name$ :formula formula :hints hints :enable thm-enable$))))