		Search-engine friendly clone of the ACL2 documentation.

Defarbrec-event-generation

Defarbrec-gen-fn-fn

Generate the definition of the lfn function.

Signature
(defarbrec-gen-fn-fn fn$ x1...xn$ body$ updates update-names$ terminates-name$ measure-name$ nonterminating$ k l measure-fn-natp-lemma-name measure-fn-end-lemma-name measure-fn-min-lemma-name wrld) → (mv local-event exported-event)
Arguments: fn$ — Guard (symbolp fn$).; x1...xn$ — Guard (symbol-listp x1...xn$).; body$ — Guard (pseudo-termp body$).; updates — Guard (pseudo-term-listp updates).; update-names$ — Guard (symbol-listp update-names$).; terminates-name$ — Guard (symbolp terminates-name$).; measure-name$ — Guard (symbolp measure-name$).; nonterminating$ — Guard (pseudo-termp nonterminating$).; k — Guard (symbolp k).; l — Guard (symbolp l).; measure-fn-natp-lemma-name — Guard (symbolp measure-fn-natp-lemma-name).; measure-fn-end-lemma-name — Guard (symbolp measure-fn-end-lemma-name).; measure-fn-min-lemma-name — Guard (symbolp measure-fn-min-lemma-name).; wrld — Guard (plist-worldp wrld).
Returns: local-event — A pseudo-event-formp.; exported-event — A pseudo-event-formp.

This is as described in the documentation. We wrap the body of the program-mode function into a check with the termination testing predicate.

This corresponds to the function f^ in the template, but we directly use measure, which corresponds to nu. The termination proof hints are adapted accordingly, by instantiating the argument k of measure with 0 and by including nfix in the theory (since it is included in the theories that prove mu-end and mu-min in the template).

Definitions and Theorems

Function: defarbrec-gen-fn-fn

(defun defarbrec-gen-fn-fn
       (fn$ x1...xn$ body$
            updates update-names$ terminates-name$
            measure-name$ nonterminating$
            k l measure-fn-natp-lemma-name
            measure-fn-end-lemma-name
            measure-fn-min-lemma-name wrld)
 (declare (xargs :guard (and (symbolp fn$)
                             (symbol-listp x1...xn$)
                             (pseudo-termp body$)
                             (pseudo-term-listp updates)
                             (symbol-listp update-names$)
                             (symbolp terminates-name$)
                             (symbolp measure-name$)
                             (pseudo-termp nonterminating$)
                             (symbolp k)
                             (symbolp l)
                             (symbolp measure-fn-natp-lemma-name)
                             (symbolp measure-fn-end-lemma-name)
                             (symbolp measure-fn-min-lemma-name)
                             (plist-worldp wrld))))
 (let ((__function__ 'defarbrec-gen-fn-fn))
  (declare (ignorable __function__))
  (b*
   ((measure (cons measure-name$ (append x1...xn$ '(0))))
    (doublets (alist-to-doublets (pairlis$ x1...xn$ updates)))
    (hints
     (cons
      (cons
       '"Goal"
       (cons
        ':in-theory
        (cons
         (cons
          'quote
          (cons
           (cons
             'o-p
             (cons 'o-finp
                   (cons 'natp
                         (cons 'o<
                               (cons 'zp
                                     (cons 'nfix update-names$))))))
           'nil))
         (cons
          ':use
          (cons
           (cons
            (cons ':instance
                  (cons measure-fn-natp-lemma-name
                        (cons (cons k '(0)) 'nil)))
            (cons
             (cons
                 ':instance
                 (cons measure-fn-natp-lemma-name
                       (append doublets (cons (cons k '(0)) 'nil))))
             (cons
              (cons ':instance
                    (cons measure-fn-end-lemma-name
                          (cons (cons k '(0)) 'nil)))
              (cons
               (cons
                ':instance
                (cons
                 measure-fn-min-lemma-name
                 (cons
                  (cons
                   l
                   (cons
                    (cons
                     '1-
                     (cons
                         (cons measure-name$ (append x1...xn$ '(0)))
                         'nil))
                    'nil))
                  (append doublets (cons (cons k '(0)) 'nil)))))
               'nil))))
           'nil)))))
      'nil))
    (body (cons 'if
                (cons (cons terminates-name$ x1...xn$)
                      (cons body$ (cons nonterminating$ 'nil)))))
    (body (untranslate body nil wrld))
    (local-event
     (cons
      'local
      (cons
       (cons
        'defun
        (cons
         fn$
         (cons
          x1...xn$
          (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
       fn$
       (cons
        x1...xn$
        (cons
         (cons
          'declare
          (cons
           (cons 'xargs
                 (cons ':measure
                       (cons measure '(:well-founded-relation o<))))
           'nil))
         (cons body 'nil)))))))
   (mv local-event exported-event))))