		Search-engine friendly clone of the ACL2 documentation.

Casesplit-event-generation

Casesplit-gen-new-fn

Generate the new function definition.

Signature
(casesplit-gen-new-fn old$ conditions$ news new-name$ new-enable$ verify-guards$ appcond-thm-names wrld) → (mv local-event exported-event)
Arguments: old$ — Guard (symbolp old$).; conditions$ — Guard (pseudo-term-listp conditions$).; news — Guard (pseudo-term-listp news).; new-name$ — Guard (symbolp new-name$).; new-enable$ — Guard (booleanp new-enable$).; verify-guards$ — Guard (booleanp verify-guards$).; appcond-thm-names — Guard (symbol-symbol-alistp appcond-thm-names).; wrld — Guard (plist-worldp wrld).
Returns: local-event — A pseudo-event-formp.; exported-event — A pseudo-event-formp.

The macro used to introduce the new function is determined by whether the new function must be enabled or not.

The new function has the same formal arguments as the old function.

The body of the new function is obtained as shown in the reference documentation. Starting with the term new0, we recursively wrap the term with (if condk newk ...), thus creating a nest of ifs that, when untranslated, have the cond structure described in the reference documentation (except when p is 1, in which case the if remains an if, which seems appropriate anyhow). The new function is never recursive, so it needs no measure, well-founded relation, or termination hints.

The new function has the same guard as the old function.

The guards are verified 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 remove the first p elements to obtain the applicability condition theorem names to use in the guard hints. We also use the guard theorem of old, which may be needed to discharge the guard obligations within the guard term of old.

Definitions and Theorems

Function: casesplit-gen-new-fn-body

(defun casesplit-gen-new-fn-body (k conditions$ news acc)
  (declare (xargs :guard (and (natp k)
                              (pseudo-term-listp conditions$)
                              (pseudo-term-listp news)
                              (pseudo-termp acc))))
  (let ((__function__ 'casesplit-gen-new-fn-body))
    (declare (ignorable __function__))
    (b* (((when (zp k)) acc)
         (condk (nth (1- k) conditions$))
         (newk (nth (1- k) news))
         (acc (cons 'if
                    (cons condk (cons newk (cons acc 'nil))))))
      (casesplit-gen-new-fn-body (1- k)
                                 conditions$ news acc))))

Theorem: pseudo-termp-of-casesplit-gen-new-fn-body

(defthm pseudo-termp-of-casesplit-gen-new-fn-body
 (implies
     (and (pseudo-termp acc)
          (pseudo-term-listp conditions$)
          (pseudo-term-listp news))
     (b* ((term (casesplit-gen-new-fn-body k conditions$ news acc)))
       (pseudo-termp term)))
 :rule-classes :rewrite)

Function: casesplit-gen-new-fn

(defun casesplit-gen-new-fn
       (old$ conditions$ news new-name$ new-enable$
             verify-guards$ appcond-thm-names wrld)
 (declare
      (xargs :guard (and (symbolp old$)
                         (pseudo-term-listp conditions$)
                         (pseudo-term-listp news)
                         (symbolp new-name$)
                         (booleanp new-enable$)
                         (booleanp verify-guards$)
                         (symbol-symbol-alistp appcond-thm-names)
                         (plist-worldp wrld))))
 (let ((__function__ 'casesplit-gen-new-fn))
  (declare (ignorable __function__))
  (evmac-generate-defun
   new-name$ :formals (formals old$ wrld)
   :guard (uguard old$ wrld)
   :body
   (b* ((new0 (car (last news)))
        (body (casesplit-gen-new-fn-body (len conditions$)
                                         conditions$ news new0)))
     (untranslate body nil wrld))
   :guard-hints
   (b* ((guard-appcond-thm-names
             (nthcdr (len news) appcond-thm-names)))
    (cons
     (cons
      '"Goal"
      (cons
       ':in-theory
       (cons
        'nil
        (cons
         ':use
         (cons (append (strip-cdrs guard-appcond-thm-names)
                       (cons (cons ':guard-theorem (cons old$ 'nil))
                             'nil))
               'nil)))))
     'nil))
   :guard-simplify :limited
   :verify-guards verify-guards$
   :enable new-enable$)))