		Search-engine friendly clone of the ACL2 documentation.

Defarbrec-event-generation

Defarbrec-gen-measure-fn-natp-lemma

Generate the local lemma about the generated measure function that asserts that the measure function returns a natural number.

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

(natp (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-natp-lemma

(defun defarbrec-gen-measure-fn-natp-lemma
       (x1...xn$ measure-name$ k names-to-avoid wrld)
 (declare (xargs :guard (and (symbol-listp x1...xn$)
                             (symbolp measure-name$)
                             (symbolp k)
                             (symbol-listp names-to-avoid)
                             (plist-worldp wrld))))
 (let ((__function__ 'defarbrec-gen-measure-fn-natp-lemma))
  (declare (ignorable __function__))
  (b*
   ((name (add-suffix measure-name$ "-NATP"))
    ((mv name &)
     (fresh-logical-name-with-$s-suffix
          name nil names-to-avoid wrld))
    (event
     (cons
      'local
      (cons
       (cons
        'defthm
        (cons
         name
         (cons
          (cons 'natp
                (cons (cons measure-name$
                            (append x1...xn$ (cons k 'nil)))
                      'nil))
          (cons
           ':hints
           (cons
            (cons
             (cons
              '"Goal"
              (cons
               ':in-theory
               (cons
                (cons 'quote
                      (cons (cons (cons ':type-prescription
                                        (cons measure-name$ 'nil))
                                  '((:compound-recognizer
                                         natp-compound-recognizer)))
                            'nil))
                'nil)))
             'nil)
            '(:rule-classes nil))))))
       'nil))))
   (mv event name))))