		Search-engine friendly clone of the ACL2 documentation.

Tailrec-event-generation

Tailrec-gen-alpha-fn

Generate the definition of the \alpha function of the design notes.

Signature
(tailrec-gen-alpha-fn old$ test updates names-to-avoid wrld) → (mv event name updated-names-to-avoid)
Arguments: old$ — Guard (symbolp old$).; test — Guard (pseudo-termp test).; updates — Guard (pseudo-term-listp updates).; names-to-avoid — Guard (symbol-listp names-to-avoid).; wrld — Guard (plist-worldp wrld).
Returns: event — A pseudo-event-formp.; name — A symbolp.; updated-names-to-avoid — A symbol-listp.

This function is generated only locally, because its purpose is just to prove local theorems (a\alpha and \gamma_f\alpha in the design notes). Since this function is only used in theorems, it has a t guard and its guards are not verified. The termination proof follows the design notes: measure and well-founded relation are the same as old. We do not normalize the function, so we can better control the proofs.

The name used for \alpha is returned, along with the event.

Definitions and Theorems

Function: tailrec-gen-alpha-fn

(defun tailrec-gen-alpha-fn (old$ test updates names-to-avoid wrld)
 (declare (xargs :guard (and (symbolp old$)
                             (pseudo-termp test)
                             (pseudo-term-listp updates)
                             (symbol-listp names-to-avoid)
                             (plist-worldp wrld))))
 (let ((__function__ 'tailrec-gen-alpha-fn))
  (declare (ignorable __function__))
  (b*
   (((mv name names-to-avoid)
     (fresh-logical-name-with-$s-suffix 'alpha
                                        'function
                                        names-to-avoid wrld))
    (formals (formals old$ wrld))
    (body (cons 'if
                (cons test
                      (cons (cons 'list formals)
                            (cons (cons name updates) 'nil)))))
    (wfrel (well-founded-relation old$ wrld))
    (measure (measure old$ wrld))
    (termination-hints
         (cons (cons '"Goal"
                     (cons ':use
                           (cons (cons ':termination-theorem
                                       (cons old$ 'nil))
                                 '(:in-theory nil))))
               'nil))
    (event
     (cons
      'local
      (cons
       (cons
        'defun
        (cons
         name
         (cons
          formals
          (cons
           (cons
            'declare
            (cons
             (cons
              'xargs
              (cons
               ':well-founded-relation
               (cons
                wfrel
                (cons
                   ':measure
                   (cons measure
                         (cons ':hints
                               (cons termination-hints
                                     '(:guard t
                                              :verify-guards nil
                                              :normalize nil))))))))
             'nil))
           (cons body 'nil)))))
       'nil))))
   (mv event name names-to-avoid))))