		Search-engine friendly clone of the ACL2 documentation.

Defarbrec-event-generation

Defarbrec-gen-update-fns-lemma

Generate the local lemma about the iterated argument udpate functions.

Signature
(defarbrec-gen-update-fns-lemma fn$ x1...xn$ test update-names$ k names-to-avoid wrld) → (mv event name)
Arguments: fn$ — Guard (symbolp fn$).; x1...xn$ — Guard (symbol-listp x1...xn$).; test — Guard (pseudo-termp test).; update-names$ — Guard (symbol-listp update-names$).; k — Guard (symbolp k).; names-to-avoid — Guard (symbol-listp names-to-avoid).; wrld — Guard (plist-worldp wrld).
Returns: event — A pseudo-event-formp.; name — A symbolp that is the name of the lemma.

This corresponds to the theorem d*-lemma in the template. Its formula has the following form in general:

(implies (and test<(update*-x1 k x1 ... xn),...,(update*-xn k x1 ... xn)>
              (not (natp k)))
         test<(update*-x1 0 x1 ... xn),...,(update*-xn 0 x1 ... xn)>)

Definitions and Theorems

Function: defarbrec-gen-update-fns-lemma

(defun defarbrec-gen-update-fns-lemma
       (fn$ x1...xn$ test
            update-names$ k names-to-avoid wrld)
 (declare (xargs :guard (and (symbolp fn$)
                             (symbol-listp x1...xn$)
                             (pseudo-termp test)
                             (symbol-listp update-names$)
                             (symbolp k)
                             (symbol-listp names-to-avoid)
                             (plist-worldp wrld))))
 (let ((__function__ 'defarbrec-gen-update-fns-lemma))
  (declare (ignorable __function__))
  (b*
   ((name (add-suffix fn$ "-UPDATE*-LEMMA"))
    ((mv name &)
     (fresh-logical-name-with-$s-suffix
          name nil names-to-avoid wrld))
    (test-of-updates-k (defarbrec-gen-test-of-updates-term
                            x1...xn$ test update-names$ k))
    (test-of-updates-0 (defarbrec-gen-test-of-updates-term
                            x1...xn$ test update-names$ '0))
    (formula
     (cons
      'implies
      (cons
       (cons
           'and
           (cons test-of-updates-k
                 (cons (cons 'not
                             (cons (cons 'natp (cons k 'nil)) 'nil))
                       'nil)))
       (cons test-of-updates-0 'nil))))
    (formula (untranslate formula t wrld))
    (event
     (cons
      'local
      (cons
       (cons
        'defthm
        (cons
         name
         (cons
          formula
          (cons
           ':hints
           (cons
            (cons
             (cons
              '"Goal"
              (cons
                 ':in-theory
                 (cons (cons 'quote
                             (cons (append update-names$ '(natp zp))
                                   'nil))
                       'nil)))
             'nil)
            '(:rule-classes nil))))))
       'nil))))
   (mv event name))))