		Search-engine friendly clone of the ACL2 documentation.

Atc-function-and-loop-generation

Atc-gen-fn-def*

Generate a local theorem that defines fn using if*.

Signature
(atc-gen-fn-def* fn names-to-avoid wrld) → (mv events name names-to-avoid)
Arguments: fn — Guard (symbolp fn).; names-to-avoid — Guard (symbol-listp names-to-avoid).; wrld — Guard (plist-worldp wrld).
Returns: events — Type (pseudo-event-form-listp events).; name — Type (symbolp name).; names-to-avoid — Type (symbol-listp names-to-avoid), given (symbol-listp names-to-avoid).

In order to have more control on case splitting, in our new modular proof generation approach, we use if* instead of if. The target functions use if of course, so we need to convert their definitions to use if*. We do so by generating, for each target function, a rule that expands it to its body but with if replaced with if*.

Definitions and Theorems

Function: atc-gen-fn-def*

(defun atc-gen-fn-def* (fn names-to-avoid wrld)
 (declare (xargs :guard (and (symbolp fn)
                             (symbol-listp names-to-avoid)
                             (plist-worldp wrld))))
 (let ((__function__ 'atc-gen-fn-def*))
  (declare (ignorable __function__))
  (b*
   (((mv event-def fn-def names-to-avoid)
     (install-not-normalized-event fn t names-to-avoid wrld))
    (fn-def* (pack fn "-DEF*"))
    ((mv fn-def* names-to-avoid)
     (fresh-logical-name-with-$s-suffix
          fn-def* nil names-to-avoid wrld))
    (body (ubody+ fn wrld))
    (body* (fty-if-to-if* body))
    (formula (cons 'equal
                   (cons (cons fn (formals+ fn wrld))
                         (cons body* 'nil))))
    (hints
     (cons (cons '"Goal"
                 (cons ':in-theory
                       (cons (cons 'quote
                                   (cons (cons fn-def '(if*)) 'nil))
                             'nil)))
           'nil))
    ((mv event-def* &)
     (evmac-generate-defthm fn-def*
                            :formula formula
                            :hints hints
                            :enable nil)))
   (mv (list event-def event-def*)
       fn-def* names-to-avoid))))

Theorem: pseudo-event-form-listp-of-atc-gen-fn-def*.events

(defthm pseudo-event-form-listp-of-atc-gen-fn-def*.events
  (b* (((mv ?events ?name ?names-to-avoid)
        (atc-gen-fn-def* fn names-to-avoid wrld)))
    (pseudo-event-form-listp events))
  :rule-classes :rewrite)

Theorem: symbolp-of-atc-gen-fn-def*.name

(defthm symbolp-of-atc-gen-fn-def*.name
  (b* (((mv ?events ?name ?names-to-avoid)
        (atc-gen-fn-def* fn names-to-avoid wrld)))
    (symbolp name))
  :rule-classes :rewrite)

Theorem: symbol-listp-of-atc-gen-fn-def*.names-to-avoid

(defthm symbol-listp-of-atc-gen-fn-def*.names-to-avoid
  (implies (symbol-listp names-to-avoid)
           (b* (((mv ?events ?name ?names-to-avoid)
                 (atc-gen-fn-def* fn names-to-avoid wrld)))
             (symbol-listp names-to-avoid)))
  :rule-classes :rewrite)