		Search-engine friendly clone of the ACL2 documentation.

Defarbrec-event-generation

Defarbrec-gen-measure-fn-end-lemma

Generate the local lemma about the generated measure function that asserts that iterating the argument updates on terminating arguments for the number indicated by the generated measure function yields values satisfying the exit test.

Signature
(defarbrec-gen-measure-fn-end-lemma x1...xn$ test update-names$ terminates-name$ terminates-witness-name$ measure-name$ k update-fns-lemma-name names-to-avoid wrld) → (mv event name)
Arguments: x1...xn$ — Guard (symbol-listp x1...xn$).; test — Guard (pseudo-termp test).; update-names$ — Guard (symbol-listp update-names$).; terminates-name$ — Guard (symbolp terminates-name$).; terminates-witness-name$ — Guard (symbolp terminates-witness-name$).; measure-name$ — Guard (symbolp measure-name$).; k — Guard (symbolp k).; update-fns-lemma-name — Guard (symbolp update-fns-lemma-name).; 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 nu-end in the template. Its formula has the following form in general:

(implies (and (terminates x1 ... xn)
              (natp k)
              (<= k (nfix (terminates-witness x1 ... xn))))
         test<(update*-x1 (measure x1 ... xn k) x1 ... xn),
              ...,
              (update*-xn (measure x1 ... xn k) x1 ... xn)>)

We generate this theorem without rule classes (instead of a rewrite rule as in the template) because we do not generate a function corresponding to mu here and we use this theorem only with :use hints.

Definitions and Theorems

Function: defarbrec-gen-measure-fn-end-lemma

(defun defarbrec-gen-measure-fn-end-lemma
       (x1...xn$ test update-names$ terminates-name$
                 terminates-witness-name$
                 measure-name$ k update-fns-lemma-name
                 names-to-avoid wrld)
 (declare (xargs :guard (and (symbol-listp x1...xn$)
                             (pseudo-termp test)
                             (symbol-listp update-names$)
                             (symbolp terminates-name$)
                             (symbolp terminates-witness-name$)
                             (symbolp measure-name$)
                             (symbolp k)
                             (symbolp update-fns-lemma-name)
                             (symbol-listp names-to-avoid)
                             (plist-worldp wrld))))
 (let ((__function__ 'defarbrec-gen-measure-fn-end-lemma))
  (declare (ignorable __function__))
  (b*
   ((name (add-suffix measure-name$ "-END"))
    ((mv name &)
     (fresh-logical-name-with-$s-suffix
          name nil names-to-avoid wrld))
    (iterations (apply-term measure-name$
                            (append x1...xn$ (cons k 'nil))))
    (test-of-updates-measure
         (defarbrec-gen-test-of-updates-term
              x1...xn$ test update-names$ iterations))
    (test-of-updates-measure
         (untranslate test-of-updates-measure nil wrld))
    (event
     (cons
      'local
      (cons
       (cons
        'defthm
        (cons
         name
         (cons
          (cons
           'implies
           (cons
            (cons
             'and
             (cons
              (cons terminates-name$ x1...xn$)
              (cons
               (cons 'natp (cons k 'nil))
               (cons
                (cons
                 '<=
                 (cons
                  k
                  (cons
                   (cons
                      'nfix
                      (cons (cons terminates-witness-name$ x1...xn$)
                            'nil))
                   'nil)))
                'nil))))
            (cons test-of-updates-measure 'nil)))
          (cons
           ':hints
           (cons
            (cons
             (cons
              '"Goal"
              (cons
               ':in-theory
               (cons
                (cons
                   'quote
                   (cons (cons measure-name$
                               (cons terminates-name$ '(natp nfix)))
                         'nil))
                (cons ':induct
                      (cons (cons measure-name$
                                  (append x1...xn$ (cons k 'nil)))
                            'nil)))))
             (cons
              (cons
               'quote
               (cons
                (cons
                 ':use
                 (cons
                  (cons
                   ':instance
                   (cons
                    update-fns-lemma-name
                    (cons
                     (cons
                      k
                      (cons (cons terminates-witness-name$ x1...xn$)
                            'nil))
                     'nil)))
                  'nil))
                'nil))
              'nil))
            '(:rule-classes nil))))))
       'nil))))
   (mv event name))))