		Search-engine friendly clone of the ACL2 documentation.

Tailrec-event-generation

Tailrec-gen-old-to-new-thm

Generate the theorem that relates the old function to the new function (f{}f' and f{}f'_0 in the design notes).

Signature
(tailrec-gen-old-to-new-thm old$ test base nonrec updates a variant$ new-name$ old-to-new-name$ old-to-new-enable$ appcond-thm-names domain-of-old-name domain-of-ground-base-name combine-left-identity-ground-name new-formals new-to-old-name$ wrld) → (mv local-event exported-event)
Arguments: old$ — Guard (symbolp old$).; test — Guard (pseudo-termp test).; base — Guard (pseudo-termp base).; nonrec — Guard (pseudo-termp nonrec).; updates — Guard (pseudo-term-listp updates).; a — Guard (symbolp a).; variant$ — Guard (tailrec-variantp variant$).; new-name$ — Guard (symbolp new-name$).; old-to-new-name$ — Guard (symbolp old-to-new-name$).; old-to-new-enable$ — Guard (booleanp old-to-new-enable$).; appcond-thm-names — Guard (symbol-symbol-alistp appcond-thm-names).; domain-of-old-name — Guard (symbolp domain-of-old-name).; domain-of-ground-base-name — Guard (symbolp domain-of-ground-base-name).; combine-left-identity-ground-name — Guard (symbolp combine-left-identity-ground-name).; new-formals — Guard (symbol-listp new-formals).; new-to-old-name$ — Guard (symbolp new-to-old-name$).; wrld — Guard (plist-worldp wrld).
Returns: local-event — A pseudo-event-formp.; exported-event — A pseudo-event-formp.

The theorem is f{}f' when the variant is :assoc or :assoc-alt, (in this case, left identity does not hold), and f{}f'_0 when the variant is :monoid or :monoid-alt (in this case, left identity holds, and we are in the special case of a ground base term).

The hints follow the proof in the design notes, for the case in which left identity holds when the variant is :monoid or :monoid-alt, and for the case in which left identity does not hold when the variant is :assoc and :assoc-alt. In the first case, the proof is for the special case of a ground base term.

For the :assoc and :assoc-alt variants, since the old function is recursive, we use an explicit :expand hint instead of just enabling the definition of old function.

Definitions and Theorems

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

(defun tailrec-gen-old-to-new-thm
       (old$ test
             base nonrec updates a variant$ new-name$
             old-to-new-name$ old-to-new-enable$
             appcond-thm-names domain-of-old-name
             domain-of-ground-base-name
             combine-left-identity-ground-name
             new-formals new-to-old-name$ wrld)
 (declare
      (xargs :guard (and (symbolp old$)
                         (pseudo-termp test)
                         (pseudo-termp base)
                         (pseudo-termp nonrec)
                         (pseudo-term-listp updates)
                         (symbolp a)
                         (tailrec-variantp variant$)
                         (symbolp new-name$)
                         (symbolp old-to-new-name$)
                         (booleanp old-to-new-enable$)
                         (symbol-symbol-alistp appcond-thm-names)
                         (symbolp domain-of-old-name)
                         (symbolp domain-of-ground-base-name)
                         (symbolp combine-left-identity-ground-name)
                         (symbol-listp new-formals)
                         (symbolp new-to-old-name$)
                         (plist-worldp wrld))))
 (let ((__function__ 'tailrec-gen-old-to-new-thm))
  (declare (ignorable __function__))
  (b*
   ((formula
       (cons 'equal
             (cons (apply-term old$ (formals old$ wrld))
                   (cons (tailrec-gen-old-as-new-term
                              old$ test base nonrec updates
                              a variant$ new-name$ new-formals wrld)
                         'nil))))
    (hints
     (case variant$
      ((:monoid :monoid-alt)
       (b*
        ((combine-left-identity-ground-instance
          (cons
           ':instance
           (cons
            combine-left-identity-ground-name
            (cons
             ':extra-bindings-ok
             (cons (cons (tailrec-gen-id-var-u old$ wrld)
                         (cons (apply-term old$ (formals old$ wrld))
                               'nil))
                   'nil)))))
         (new-to-old-instance
              (cons ':instance
                    (cons new-to-old-name$
                          (cons ':extra-bindings-ok
                                (cons (cons a (cons base 'nil))
                                      'nil))))))
        (cons
         (cons
          '"Goal"
          (cons
           ':in-theory
           (cons
            'nil
            (cons
             ':use
             (cons
              (cons
               domain-of-ground-base-name
               (cons
                   domain-of-old-name
                   (cons new-to-old-instance
                         (cons combine-left-identity-ground-instance
                               'nil))))
              'nil)))))
         'nil)))
      (:assoc
       (b*
        ((formals (formals old$ wrld))
         (domain-of-nonrec-thm
              (cdr (assoc-eq :domain-of-nonrec appcond-thm-names)))
         (new-to-old-instance
          (cons
           ':instance
           (cons
            new-to-old-name$
            (cons
             ':extra-bindings-ok
             (cons
                (cons a (cons nonrec 'nil))
                (alist-to-doublets (pairlis$ formals updates))))))))
        (cons
         (cons
          '"Goal"
          (cons
           ':in-theory
           (cons
            'nil
            (cons
             ':expand
             (cons
                  (cons (cons old$ formals) 'nil)
                  (cons ':use
                        (cons (cons domain-of-nonrec-thm
                                    (cons new-to-old-instance 'nil))
                              'nil)))))))
         'nil)))
      (:assoc-alt
       (b*
        ((formals (formals old$ wrld))
         (new-to-old-instance
          (cons
           ':instance
           (cons
            new-to-old-name$
            (cons
             ':extra-bindings-ok
             (cons
                (cons a (cons nonrec 'nil))
                (alist-to-doublets (pairlis$ formals updates))))))))
        (cons
         (cons
          '"Goal"
          (cons
           ':in-theory
           (cons
             'nil
             (cons ':expand
                   (cons (cons (cons old$ formals) 'nil)
                         (cons ':use
                               (cons (cons new-to-old-instance 'nil)
                                     'nil)))))))
         'nil)))
      (t (impossible)))))
   (evmac-generate-defthm old-to-new-name$
                          :formula formula
                          :hints hints
                          :enable old-to-new-enable$))))