Generate a local theorem that defines
(atc-gen-fn-def* fn names-to-avoid wrld) → (mv events name 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*.
Function:
(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:
(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:
(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:
(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)