		Search-engine friendly clone of the ACL2 documentation.

Tailrec-event-generation

Tailrec-gen-old-to-wrapper-thm

Generate the theorem that relates the old function to the wrapper function (f{}\tilde{f} in the design notes).

Signature
(tailrec-gen-old-to-wrapper-thm old$ wrapper-name$ old-to-wrapper-name$ old-to-wrapper-enable$ old-to-new-name$ wrapper-unnorm-name wrld) → (mv local-event exported-event)
Arguments: old$ — Guard (symbolp old$).; wrapper-name$ — Guard (symbolp wrapper-name$).; old-to-wrapper-name$ — Guard (symbolp old-to-wrapper-name$).; old-to-wrapper-enable$ — Guard (booleanp old-to-wrapper-enable$).; old-to-new-name$ — Guard (symbolp old-to-new-name$).; wrapper-unnorm-name — Guard (symbolp wrapper-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 theorem's formula has the form (equal (old x1 ... xn) (wrapper x1 ... xn)).

The theorem is proved by expanding the (non-normalized) definition of the wrapper function and using the theorem that relates the old function to the new function.

This function is called only if the :wrapper input is t.

Definitions and Theorems

Function: tailrec-gen-old-to-wrapper-thm

(defun tailrec-gen-old-to-wrapper-thm
       (old$ wrapper-name$ old-to-wrapper-name$
             old-to-wrapper-enable$ old-to-new-name$
             wrapper-unnorm-name wrld)
 (declare (xargs :guard (and (symbolp old$)
                             (symbolp wrapper-name$)
                             (symbolp old-to-wrapper-name$)
                             (booleanp old-to-wrapper-enable$)
                             (symbolp old-to-new-name$)
                             (symbolp wrapper-unnorm-name)
                             (plist-worldp wrld))))
 (let ((__function__ 'tailrec-gen-old-to-wrapper-thm))
  (declare (ignorable __function__))
  (b*
   ((formals (formals old$ wrld))
    (formula
         (untranslate
              (cons 'equal
                    (cons (apply-term old$ formals)
                          (cons (apply-term wrapper-name$ formals)
                                'nil)))
              t wrld))
    (hints
     (cons
       (cons '"Goal"
             (cons ':in-theory
                   (cons (cons 'quote
                               (cons (cons wrapper-unnorm-name 'nil)
                                     'nil))
                         (cons ':use
                               (cons old-to-new-name$ 'nil)))))
       'nil)))
   (evmac-generate-defthm old-to-wrapper-name$
                          :formula formula
                          :hints hints
                          :enable old-to-wrapper-enable$))))