		Search-engine friendly clone of the ACL2 documentation.

Casesplit-event-generation

Casesplit-gen-old-to-new-thm

Generate the theorem that relates the old and new functions.

Signature
(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)
Arguments: old$ — Guard (symbolp old$).; theorems$ — Guard (symbol-listp theorems$).; new-name$ — Guard (symbolp new-name$).; thm-name$ — Guard (symbolp thm-name$).; thm-enable$ — Guard (booleanp thm-enable$).; appcond-thm-names — Guard (symbol-symbol-alistp appcond-thm-names).; new-unnorm-name — Guard (symbolp new-unnorm-name).; wrld — Guard (plist-worldp wrld).
Returns: local-event — A pseudo-event-formp.; exported-event — A pseudo-event-formp.

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 appcond-thm-names alist is in the same order as the applicability conditions are listed in the reference documentation, so we take the first p elements to obtain the applicability condition theorem names to use in the guard hints; note that, if verify-guards$ is nil, these are all the applicability conditions, because there are no guard-related applicability conditions. We also use the theorem names specified in the theorems input.

Definitions and Theorems

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

(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$))))