		Search-engine friendly clone of the ACL2 documentation.

Defarbrec-event-generation

Defarbrec-gen-measure-fn

Generate the measure function definition.

Signature
(defarbrec-gen-measure-fn x1...xn$ test update-names$ terminates-witness-name$ measure-name$ k wrld) → (mv local-event exported-event)
Arguments: x1...xn$ — Guard (symbol-listp x1...xn$).; test — Guard (pseudo-termp test).; update-names$ — Guard (symbol-listp update-names$).; terminates-witness-name$ — Guard (symbolp terminates-witness-name$).; measure-name$ — Guard (symbolp measure-name$).; k — Guard (symbolp k).; wrld — Guard (plist-worldp wrld).
Returns: local-event — A pseudo-event-formp.; exported-event — A pseudo-event-formp.

This is the function measure in the documentation. It corresponds to the function nu in the template.

We do not generate a function corresponding to mu in the template. We directly use the equivalent of (nu x 0) for the measure of the logic-mode fn (see defarbrec-gen-fn-fn).

Definitions and Theorems

Function: defarbrec-gen-measure-fn

(defun defarbrec-gen-measure-fn
       (x1...xn$ test
                 update-names$ terminates-witness-name$
                 measure-name$ k wrld)
 (declare (xargs :guard (and (symbol-listp x1...xn$)
                             (pseudo-termp test)
                             (symbol-listp update-names$)
                             (symbolp terminates-witness-name$)
                             (symbolp measure-name$)
                             (symbolp k)
                             (plist-worldp wrld))))
 (let ((__function__ 'defarbrec-gen-measure-fn))
  (declare (ignorable __function__))
  (b*
   ((test-of-updates-k (defarbrec-gen-test-of-updates-term
                            x1...xn$ test update-names$ k))
    (test-of-updates-k (untranslate test-of-updates-k nil wrld))
    (formals (append x1...xn$ (cons k 'nil)))
    (body
     (cons
      'let
      (cons
       (cons (cons k
                   (cons (cons 'nfix (cons k 'nil)) 'nil))
             'nil)
       (cons
        (cons
         'if
         (cons
          (cons
           'or
           (cons
            test-of-updates-k
            (cons
             (cons
              '>=
              (cons
               k
               (cons
                (cons 'nfix
                      (cons (cons terminates-witness-name$ x1...xn$)
                            'nil))
                'nil)))
             'nil)))
          (cons
           k
           (cons
                (cons measure-name$
                      (append x1...xn$
                              (cons (cons '1+ (cons k 'nil)) 'nil)))
                'nil))))
        'nil))))
    (measure
     (cons
          'nfix
          (cons (cons '-
                      (cons (cons terminates-witness-name$ x1...xn$)
                            (cons (cons 'nfix (cons k 'nil)) 'nil)))
                'nil)))
    (hints '(("Goal" :in-theory '(o-p o-finp o< nfix natp))))
    (local-event
     (cons
      'local
      (cons
       (cons
        'defun
        (cons
         measure-name$
         (cons
          formals
          (cons
           (cons
            'declare
            (cons
             (cons
              'xargs
              (cons
               ':measure
               (cons
                   measure
                   (cons ':well-founded-relation
                         (cons 'o<
                               (cons ':hints (cons hints 'nil)))))))
             'nil))
           (cons body 'nil)))))
       'nil)))
    (exported-event
     (cons
      'defun
      (cons
       measure-name$
       (cons
        formals
        (cons
         (cons
          'declare
          (cons
           (cons 'xargs
                 (cons ':measure
                       (cons measure '(:well-founded-relation o<))))
           'nil))
         (cons body 'nil)))))))
   (mv local-event exported-event))))