Generate a theorem event for an applicability condition.
(evmac-appcond-theorem appcond hints names-to-avoid print ctx state) → (mv event thm-name new-hints updated-names-to-avoid)
We generate a name for the theorem that is not in the world
and that is distinct from the given list of names to avoid;
the latter are names not yet in the world,
but are names of other events
that will be added to the world together with this theorem,
and that therefore must be all distinct.
We return an updated list of names to avoid that includes the new name,
so that future calls of this function, or of other event-generating code,
can use the updated list to avoid conflicts with this new name.
The new theorem name is also returned as a result as a convenience
(it could be extracted from the returned event instead);
the event macro may reference this name in generated proofs
(see evmac-appcond-theorem-list for more discussion on this).
The theorem name is the same as
the keyword that names the applicability condition,
if fresh, otherwise
We untranslate the formula so that it is more readable if printed on the screen. The use of untranslate forces this function and its callers into program mode. An alternative could be to use a more limited, logic-mode untranslation.
If the event macro's hints are an alist from keywords to true lists,
we extract the ones associated to the applicability conditions
(if any, otherwise we get
The theorem has no rule classes,
because it is meant to be referenced in
The theorem is wrapped into try-event
in order to provide a terser error message if the proof fails.
This wrapping is not performed if
This function also takes a print specifier as input, meant to be one of the inputs of the event macro. This is used to determine whether events that show progress messages should be generated or not. Since this is a binary choice, the input of this function could be a boolean flag instead of a print specifier. However, having a print specifier makes things more modular (e.g. if print specifiers are extended with more options in the future). If an event macro does not have a print specifier input (perhaps yet), the caller of this function can still set one adequate to whether progress messages must be shown or not.
The returned event, which consists of the theorem
and the optional show-progress events,
is local (to the encapsulate that the event macro expands to).
This is why the exact name of the theorem is not too important,
so long as it is valid and does not clash with others.
If an event macro should generate
(some of) its applicability conditions as persistent events,
the best course of action is to still use this function
to generate local theorems with no rule classes,
and then do another pass over such applicability conditions
to generate non-local theorems
with the same formulas,
without hints (thus keeping the history ``clean'')
and with the desired names and rule classes.
These non-local theorems can be easily proved via
So this function generates a little more than just a theorem event, because of the surrounding things generated. However, those surrounding things are auxiliary: it is still, mainly, a theorem event.
(defun evmac-appcond-theorem (appcond hints names-to-avoid print ctx state) (declare (xargs :stobjs (state))) (declare (xargs :guard (and (evmac-appcondp appcond) (evmac-input-hints-p hints) (symbol-listp names-to-avoid) (evmac-input-print-p print)))) (let ((__function__ 'evmac-appcond-theorem)) (declare (ignorable __function__)) (b* ((wrld (w state)) ((evmac-appcond appcond) appcond) ((mv thm-name updated-names-to-avoid) (fresh-logical-name-with-$s-suffix (intern-in-package-of-symbol (symbol-name appcond.name) (pkg-witness "ACL2")) nil names-to-avoid wrld)) (thm-formula (untranslate$ appcond.formula t state)) ((mv thm-hints new-hints) (if (keyword-truelist-alistp hints) (mv (cdr (assoc-eq appcond.name hints)) (remove-assoc-eq appcond.name hints)) (mv hints hints))) (thm-event (cons 'defthm (cons thm-name (cons thm-formula (cons ':rule-classes (cons 'nil (and thm-hints (list :hints thm-hints)))))))) (error-msg (msg "The proof of the ~x0 applicability condition fails:~%~X12~|" appcond.name thm-formula nil)) (try?-thm-event (if (eq print :all) thm-event (try-event thm-event ctx t nil error-msg))) (show-progress-p (member-eq print '(:info :all))) (progress-start? (and show-progress-p (cons (cons 'cw-event (cons '"~%Attempting to prove the ~x0 ~ applicability condition:~%~X12~|" (cons (cons 'quote (cons appcond.name 'nil)) (cons (cons 'quote (cons thm-formula 'nil)) '(nil))))) 'nil))) (progress-end? (and show-progress-p '((cw-event "Done.~%")))) (event (cons 'local (cons (cons 'progn (append progress-start? (cons try?-thm-event progress-end?))) 'nil)))) (mv event thm-name new-hints updated-names-to-avoid))))
(defthm pseudo-event-formp-of-evmac-appcond-theorem.event (b* (((mv ?event ?thm-name ?new-hints ?updated-names-to-avoid) (evmac-appcond-theorem appcond hints names-to-avoid print ctx state))) (pseudo-event-formp event)) :rule-classes :rewrite)
(defthm symbolp-of-evmac-appcond-theorem.thm-name (b* (((mv ?event ?thm-name ?new-hints ?updated-names-to-avoid) (evmac-appcond-theorem appcond hints names-to-avoid print ctx state))) (symbolp thm-name)) :rule-classes :rewrite)
(defthm evmac-input-hints-p-of-evmac-appcond-theorem.new-hints (implies (evmac-input-hints-p hints) (b* (((mv ?event ?thm-name ?new-hints ?updated-names-to-avoid) (evmac-appcond-theorem appcond hints names-to-avoid print ctx state))) (evmac-input-hints-p new-hints))) :rule-classes :rewrite)
(defthm symbol-listp-of-evmac-appcond-theorem.updated-names-to-avoid (implies (symbol-listp names-to-avoid) (b* (((mv ?event ?thm-name ?new-hints ?updated-names-to-avoid) (evmac-appcond-theorem appcond hints names-to-avoid print ctx state))) (symbol-listp updated-names-to-avoid))) :rule-classes :rewrite)