		Search-engine friendly clone of the ACL2 documentation.

Tailrec-event-generation

Tailrec-gen-domain-of-old-thm

Generate the theorem asserting that the old function always yields values in the domain (D{}f in the design notes).

Signature
(tailrec-gen-domain-of-old-thm old$ test nonrec updates variant$ domain$ names-to-avoid appcond-thm-names old-unnorm-name wrld) → (mv event name updated-names-to-avoid)
Arguments: old$ — Guard (symbolp old$).; test — Guard (pseudo-termp test).; nonrec — Guard (pseudo-termp nonrec).; updates — Guard (pseudo-term-listp updates).; variant$ — Guard (tailrec-variantp variant$).; domain$ — Guard (pseudo-termfnp domain$).; names-to-avoid — Guard (symbol-listp names-to-avoid).; appcond-thm-names — Guard (symbol-symbol-alistp appcond-thm-names).; old-unnorm-name — Guard (symbolp old-unnorm-name).; wrld — Guard (plist-worldp wrld).
Returns: event — A pseudo-event-formp.; name — A symbolp that names the theorem.; updated-names-to-avoid — A symbol-listp.

This is generated only if the variant is :monoid, :monoid-alt, or :assoc.

The theorem's formula is (domain (old x1 ... xn)). This is just t if domain is (lambda (x) t) (e.g. as default).

The hints follow the proofs in the design notes.

This theorem event is local, because it is a lemma used to prove the exported main theorem.

Definitions and Theorems

Function: tailrec-gen-domain-of-old-thm

(defun tailrec-gen-domain-of-old-thm
       (old$ test nonrec
             updates variant$ domain$ names-to-avoid
             appcond-thm-names old-unnorm-name wrld)
 (declare
      (xargs :guard (and (symbolp old$)
                         (pseudo-termp test)
                         (pseudo-termp nonrec)
                         (pseudo-term-listp updates)
                         (tailrec-variantp variant$)
                         (pseudo-termfnp domain$)
                         (symbol-listp names-to-avoid)
                         (symbol-symbol-alistp appcond-thm-names)
                         (symbolp old-unnorm-name)
                         (plist-worldp wrld))))
 (let ((__function__ 'tailrec-gen-domain-of-old-thm))
  (declare (ignorable __function__))
  (b*
   (((mv name names-to-avoid)
     (fresh-logical-name-with-$s-suffix 'domain-of-old
                                        nil names-to-avoid wrld))
    (formula
         (untranslate
              (apply-term* domain$
                           (apply-term old$ (formals old$ wrld)))
              t wrld))
    (hints
     (case variant$
      ((:monoid :assoc)
       (b*
        ((domain-of-base-thm
              (cdr (assoc-eq :domain-of-base appcond-thm-names)))
         (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)))
         (domain-of-combine-instance
          (cons
           ':instance
           (cons
            domain-of-combine-thm
            (cons ':extra-bindings-ok
                  (cons (cons (tailrec-gen-var-u old$)
                              (cons nonrec 'nil))
                        (cons (cons (tailrec-gen-var-v old$)
                                    (cons (cons old$ updates) 'nil))
                              'nil)))))))
        (cons
         (cons
          '"Goal"
          (cons
           ':in-theory
           (cons
            (cons
               'quote
               (cons (cons old-unnorm-name
                           (cons (cons ':induction (cons old$ 'nil))
                                 'nil))
                     'nil))
            (cons ':induct
                  (cons (cons old$ (formals old$ wrld))
                        'nil)))))
         (cons
          (cons
           'quote
           (cons
            (cons
             ':use
             (cons
                (cons domain-of-base-thm
                      (cons domain-of-nonrec-thm
                            (cons domain-of-combine-instance 'nil)))
                'nil))
            'nil))
          'nil))))
      (:monoid-alt
       (b*
        ((domain-of-base-thm
              (cdr (assoc-eq :domain-of-base appcond-thm-names)))
         (domain-of-combine-uncond-thm
          (cdr
            (assoc-eq :domain-of-combine-uncond 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 nonrec 'nil))
                        (cons (cons (tailrec-gen-var-v old$)
                                    (cons (cons old$ updates) 'nil))
                              'nil)))))))
        (cons
         (cons
          '"Goal"
          (cons ':in-theory
                (cons (cons 'quote
                            (cons (cons old-unnorm-name 'nil) 'nil))
                      (cons ':cases
                            (cons (cons test 'nil) 'nil)))))
         (cons
          (cons
           'quote
           (cons
            (cons
             ':use
             (cons
                (cons domain-of-base-thm
                      (cons domain-of-combine-uncond-instance 'nil))
                'nil))
            'nil))
          'nil))))
      (:assoc-alt
       (raise "Internal error: called when variant is :ASSOC-ALT."))
      (t (impossible))))
    (event
     (cons
      'local
      (cons
       (cons
        'defthm
        (cons
             name
             (cons formula
                   (cons ':rule-classes
                         (cons 'nil
                               (cons ':hints (cons hints 'nil)))))))
       'nil))))
   (mv event name names-to-avoid))))