		Search-engine friendly clone of the ACL2 documentation.

Defarbrec-event-generation

Defarbrec-gen-measure-fn-min-lemma

Generate the local lemma about the generated measure function that asserts that the value of the measure function is the minimum number of iterations of the argument update functions that turn terminating arguments into values satisfying the exit test.

Signature
(defarbrec-gen-measure-fn-min-lemma x1...xn$ test update-names$ measure-name$ k l 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$).; measure-name$ — Guard (symbolp measure-name$).; k — Guard (symbolp k).; l — Guard (symbolp l).; 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-min in the template. Its formula has the following form in general:

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

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-min-lemma

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