		Search-engine friendly clone of the ACL2 documentation.

Tailrec-event-generation

Tailrec-gen-base-guard-thm

Generate the theorem asserting that the guard of the base term is satisfied if the guard of the target function is (G{}b in the design notes).

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

The hints follow the proof 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-base-guard-thm

(defun tailrec-gen-base-guard-thm
       (old$ base alpha-name test-of-alpha-name
             old-guard-of-alpha-name
             names-to-avoid state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (and (symbolp old$)
                             (pseudo-termp base)
                             (symbolp alpha-name)
                             (symbolp test-of-alpha-name)
                             (symbolp old-guard-of-alpha-name)
                             (symbol-listp names-to-avoid))))
 (let ((__function__ 'tailrec-gen-base-guard-thm))
  (declare (ignorable __function__))
  (b*
   ((wrld (w state))
    ((mv name names-to-avoid)
     (fresh-logical-name-with-$s-suffix 'base-guard
                                        nil names-to-avoid wrld))
    (formula (implicate (guard old$ nil wrld)
                        (term-guard-obligation base
                                               :limited state)))
    (formals (formals old$ wrld))
    (alpha-comps
         (tailrec-gen-alpha-component-terms alpha-name old$ wrld))
    (hints
     (cons
      (cons
       '"Goal"
       (cons
        ':in-theory
        (cons
         'nil
         (cons
          ':use
          (cons
           (cons
            old-guard-of-alpha-name
            (cons
             test-of-alpha-name
             (cons
              (cons
                 ':instance
                 (cons (cons ':guard-theorem (cons old$ 'nil))
                       (cons ':extra-bindings-ok
                             (alist-to-doublets
                                  (pairlis$ formals alpha-comps)))))
              '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))))