		Search-engine friendly clone of the ACL2 documentation.

Tailrec-event-generation

Tailrec-gen-new-to-old-thm

Generate the theorem equating the new function to a combination of the old function with a (f'{}f in the design notes).

Signature
(tailrec-gen-new-to-old-thm old$ nonrec updates combine q r variant$ domain$ new-name$ a new-to-old-name$ new-to-old-enable$ appcond-thm-names old-unnorm-name domain-of-old-name new-formals new-unnorm-name wrld) → (mv local-event exported-event)
Arguments: old$ — Guard (symbolp old$).; nonrec — Guard (pseudo-termp nonrec).; updates — Guard (pseudo-term-listp updates).; combine — Guard (pseudo-termp combine).; q — Guard (symbolp q).; r — Guard (symbolp r).; variant$ — Guard (tailrec-variantp variant$).; domain$ — Guard (pseudo-termfnp domain$).; new-name$ — Guard (symbolp new-name$).; a — Guard (symbolp a).; new-to-old-name$ — Guard (symbolp new-to-old-name$).; new-to-old-enable$ — Guard (booleanp new-to-old-enable$).; appcond-thm-names — Guard (symbol-symbol-alistp appcond-thm-names).; old-unnorm-name — Guard (symbolp old-unnorm-name).; domain-of-old-name — Guard (symbolp domain-of-old-name).; new-formals — Guard (symbol-listp new-formals).; 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 theorem's formula is

(implies (domain a)
         (equal (new x1 ... xn a)
                combine<a,(old x1 ... xn)>))

if the variant is :monoid, :monoid-alt, or :assoc, while it is

(equal (new x1 ... xn a)
       combine<a,(old x1 ... xn)>)

if the variant is :assoc-alt.

The hints follow the proofs in the design notes. Note that combine-right-identity-thm? is nil iff the :combine-right-identity applicability condition is absent, which happens exactly when the :variant input to the transformation is :assoc or :assoc-alt. In this case, no instance of that applicability condition is used in the proof.

Definitions and Theorems

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

(defun tailrec-gen-new-to-old-thm
       (old$ nonrec updates combine q r variant$
             domain$ new-name$ a new-to-old-name$
             new-to-old-enable$ appcond-thm-names
             old-unnorm-name domain-of-old-name
             new-formals new-unnorm-name wrld)
 (declare
      (xargs :guard (and (symbolp old$)
                         (pseudo-termp nonrec)
                         (pseudo-term-listp updates)
                         (pseudo-termp combine)
                         (symbolp q)
                         (symbolp r)
                         (tailrec-variantp variant$)
                         (pseudo-termfnp domain$)
                         (symbolp new-name$)
                         (symbolp a)
                         (symbolp new-to-old-name$)
                         (booleanp new-to-old-enable$)
                         (symbol-symbol-alistp appcond-thm-names)
                         (symbolp old-unnorm-name)
                         (symbolp domain-of-old-name)
                         (symbol-listp new-formals)
                         (symbolp new-unnorm-name)
                         (plist-worldp wrld))))
 (let ((__function__ 'tailrec-gen-new-to-old-thm))
  (declare (ignorable __function__))
  (b*
   ((formula
     (cons
      'equal
      (cons
         (apply-term new-name$ new-formals)
         (cons (apply-term* (tailrec-gen-combine-op combine q r)
                            a (apply-term old$ (formals old$ wrld)))
               'nil))))
    (formula (if (eq variant$ :assoc-alt)
                 formula
               (implicate (apply-term* domain$ a)
                          formula)))
    (formula (untranslate formula t wrld))
    (hints
     (case variant$
      ((:monoid :assoc)
       (b*
        ((domain-of-nonrec-thm
              (cdr (assoc-eq :domain-of-nonrec appcond-thm-names)))
         (domain-of-combine-thm
              (cdr (assoc-eq :domain-of-combine appcond-thm-names)))
         (combine-associativity-thm
          (cdr (assoc-eq :combine-associativity appcond-thm-names)))
         (combine-right-identity-thm?
          (cdr
              (assoc-eq :combine-right-identity appcond-thm-names)))
         (domain-of-combine-instance
          (cons
              ':instance
              (cons domain-of-combine-thm
                    (cons ':extra-bindings-ok
                          (cons (cons (tailrec-gen-var-u old$)
                                      (cons a 'nil))
                                (cons (cons (tailrec-gen-var-v old$)
                                            (cons nonrec 'nil))
                                      'nil))))))
         (combine-associativity-instance
          (cons
           ':instance
           (cons
            combine-associativity-thm
            (cons
             ':extra-bindings-ok
             (cons
              (cons (tailrec-gen-var-u old$)
                    (cons a 'nil))
              (cons
                  (cons (tailrec-gen-var-v old$)
                        (cons nonrec 'nil))
                  (cons (cons (tailrec-gen-var-w old$)
                              (cons (apply-term old$ updates) 'nil))
                        'nil)))))))
         (combine-right-identity-instance?
          (and
           combine-right-identity-thm?
           (cons
            ':instance
            (cons combine-right-identity-thm?
                  (cons ':extra-bindings-ok
                        (cons (cons (tailrec-gen-id-var-u old$ wrld)
                                    (cons a 'nil))
                              'nil))))))
         (domain-of-old-instance
          (cons
           ':instance
           (cons
              domain-of-old-name
              (cons ':extra-bindings-ok
                    (alist-to-doublets (pairlis$ (formals old$ wrld)
                                                 updates)))))))
        (cons
         (cons
          '"Goal"
          (cons
           ':in-theory
           (cons
            (cons
             'quote
             (cons
              (cons
                old-unnorm-name
                (cons new-unnorm-name
                      (cons (cons ':induction (cons new-name$ 'nil))
                            'nil)))
              'nil))
            (cons ':induct
                  (cons (cons new-name$ new-formals)
                        'nil)))))
         (cons
          (cons
           'quote
           (cons
            (cons
             ':use
             (cons
              (append
               (and combine-right-identity-thm?
                    (list combine-right-identity-instance?))
               (cons
                domain-of-nonrec-thm
                (cons
                 domain-of-combine-instance
                 (cons
                      domain-of-old-instance
                      (cons combine-associativity-instance 'nil)))))
              'nil))
            'nil))
          'nil))))
      (:monoid-alt
       (b*
        ((domain-of-combine-uncond-thm
          (cdr
            (assoc-eq :domain-of-combine-uncond appcond-thm-names)))
         (combine-associativity-uncond-thm
          (cdr
             (assoc-eq
                  :combine-associativity-uncond appcond-thm-names)))
         (combine-right-identity-thm
          (cdr
              (assoc-eq :combine-right-identity appcond-thm-names)))
         (domain-of-combine-uncond-instance
          (cons
              ':instance
              (cons domain-of-combine-uncond-thm
                    (cons ':extra-bindings-ok
                          (cons (cons (tailrec-gen-var-u old$)
                                      (cons a 'nil))
                                (cons (cons (tailrec-gen-var-v old$)
                                            (cons nonrec 'nil))
                                      'nil))))))
         (combine-associativity-uncond-instance
          (cons
           ':instance
           (cons
            combine-associativity-uncond-thm
            (cons
             ':extra-bindings-ok
             (cons
              (cons (tailrec-gen-var-u old$)
                    (cons a 'nil))
              (cons
                  (cons (tailrec-gen-var-v old$)
                        (cons nonrec 'nil))
                  (cons (cons (tailrec-gen-var-w old$)
                              (cons (apply-term old$ updates) 'nil))
                        'nil)))))))
         (combine-right-identity-instance
          (cons
            ':instance
            (cons combine-right-identity-thm
                  (cons ':extra-bindings-ok
                        (cons (cons (tailrec-gen-id-var-u old$ wrld)
                                    (cons a 'nil))
                              'nil))))))
        (cons
         (cons
          '"Goal"
          (cons
           ':in-theory
           (cons
            (cons
             'quote
             (cons
              (cons
                old-unnorm-name
                (cons new-unnorm-name
                      (cons (cons ':induction (cons new-name$ 'nil))
                            'nil)))
              'nil))
            (cons ':induct
                  (cons (cons new-name$ new-formals)
                        'nil)))))
         (cons
          (cons
           'quote
           (cons
            (cons
             ':use
             (cons
              (cons
                   combine-right-identity-instance
                   (cons domain-of-combine-uncond-instance
                         (cons combine-associativity-uncond-instance
                               'nil)))
              'nil))
            'nil))
          'nil))))
      (:assoc-alt
       (b*
        ((combine-associativity-uncond-thm
          (cdr
             (assoc-eq
                  :combine-associativity-uncond appcond-thm-names)))
         (combine-associativity-uncond-instance
          (cons
           ':instance
           (cons
            combine-associativity-uncond-thm
            (cons
             ':extra-bindings-ok
             (cons
              (cons (tailrec-gen-var-u old$)
                    (cons a 'nil))
              (cons
                  (cons (tailrec-gen-var-v old$)
                        (cons nonrec 'nil))
                  (cons (cons (tailrec-gen-var-w old$)
                              (cons (apply-term old$ updates) 'nil))
                        'nil))))))))
        (cons
         (cons
          '"Goal"
          (cons
           ':in-theory
           (cons
            (cons
             'quote
             (cons
              (cons
                old-unnorm-name
                (cons new-unnorm-name
                      (cons (cons ':induction (cons new-name$ 'nil))
                            'nil)))
              'nil))
            (cons ':induct
                  (cons (cons new-name$ new-formals)
                        'nil)))))
         (cons
          (cons
           'quote
           (cons
             (cons ':use
                   (cons (cons combine-associativity-uncond-instance
                               'nil)
                         'nil))
             'nil))
          'nil))))
      (t (impossible)))))
   (evmac-generate-defthm new-to-old-name$
                          :formula formula
                          :hints hints
                          :enable new-to-old-enable$))))