		Search-engine friendly clone of the ACL2 documentation.

Tailrec-event-generation

Tailrec-gen-old-guard-of-alpha-thm

Generate the theorem asserting that the guard of the old function is preserved by \alpha (\gamma_f\alpha in the design notes).

Signature
(tailrec-gen-old-guard-of-alpha-thm old$ alpha-name names-to-avoid wrld) → (mv event name updated-names-to-avoid)
Arguments: old$ — Guard (symbolp old$).; alpha-name — Guard (symbolp alpha-name).; names-to-avoid — Guard (symbol-listp names-to-avoid).; wrld — Guard (plist-worldp wrld).
Returns: event — A pseudo-event-formp.; name — A symbolp that names the theorem.; updated-names-to-avoid — A symbol-listp.

The theorem's formula is (implies old-guard<x1,...,xn> old-guard<alpha_x1,...,alpha_xn>), where alpha_xi is the i-th result of \alpha, counting from 1.

The hints follow the proof in the design notes. Since the theorem involves nth applied to cons, we enable the built-in theorems nth-0-cons and nth-add1; this is implicit in the design notes.

This theorem is local, because it is just a lemma used to prove other theorems.

Definitions and Theorems

Function: tailrec-gen-old-guard-of-alpha-thm

(defun tailrec-gen-old-guard-of-alpha-thm
       (old$ alpha-name names-to-avoid wrld)
 (declare (xargs :guard (and (symbolp old$)
                             (symbolp alpha-name)
                             (symbol-listp names-to-avoid)
                             (plist-worldp wrld))))
 (let ((__function__ 'tailrec-gen-old-guard-of-alpha-thm))
  (declare (ignorable __function__))
  (b*
   (((mv name names-to-avoid)
     (fresh-logical-name-with-$s-suffix 'old-guard-of-alpha
                                        nil names-to-avoid wrld))
    (formals (formals old$ wrld))
    (alpha-component-terms
         (tailrec-gen-alpha-component-terms alpha-name old$ wrld))
    (old-guard (guard old$ nil wrld))
    (formula
         (implicate old-guard
                    (subcor-var formals
                                alpha-component-terms old-guard)))
    (hints
     (cons
      (cons
       '"Goal"
       (cons
          ':in-theory
          (cons (cons 'quote
                      (cons (cons alpha-name '(nth-0-cons nth-add1))
                            'nil))
                (cons ':induct
                      (cons (cons alpha-name formals)
                            'nil)))))
      (cons
       (cons
           'quote
           (cons (cons ':use
                       (cons (cons ':guard-theorem (cons old$ 'nil))
                             'nil))
                 'nil))
       'nil)))
    (event
     (cons
      'local
      (cons
       (cons
        'defthm
        (cons
             name
             (cons formula
                   (cons ':rule-classes
                         (cons 'nil
                               (cons ':hints (cons hints 'nil)))))))
       'nil))))
   (mv event name names-to-avoid))))