Lift evmac-appcond-theorem to lists of applicability conditions.
(evmac-appcond-theorem-list appconds hints names-to-avoid print ctx state) → (mv events thm-names new-hints updated-names-to-avoid)
We call evmac-appcond-theorem on each applicability condition in turn, returning the corresponding list of theorem events. We thread the hints and the list of names to avoid through. If the resulting hints are a non-empty alist from keywords to true lists, it means that there were keywords in the hints' keys not matching any of the applicability conditions. Perhaps those keywords refer to applicability conditions that may be present but were not actually present this time. Callers of this function can decide how to handle this situation, e.g. by issuing a warning or error (see evmac-ensure-no-extra-hints).
Since there may be multiple applicability conditions,
the generated names of the theorems are returned in alist form.
The theorem names are the values,
while the keys are the keywords that name the applicability conditions.
This makes it more convenient to look up the theorem names,
particularly in order to generate proof hints
that reference applicability conditions:
those hints must reference not applicability condition keywords,
but the corresponding theorems.
Given the possible addition of
Function:
(defun evmac-appcond-theorem-list (appconds hints names-to-avoid print ctx state) (declare (xargs :stobjs (state))) (declare (xargs :guard (and (evmac-appcond-listp appconds) (evmac-input-hints-p hints) (symbol-listp names-to-avoid) (evmac-input-print-p print)))) (let ((__function__ 'evmac-appcond-theorem-list)) (declare (ignorable __function__)) (b* (((when (endp appconds)) (mv nil nil hints names-to-avoid)) (appcond (car appconds)) ((mv event thm-name hints names-to-avoid) (evmac-appcond-theorem appcond hints names-to-avoid print ctx state)) ((mv events thm-names hints names-to-avoid) (evmac-appcond-theorem-list (cdr appconds) hints names-to-avoid print ctx state))) (mv (cons event events) (acons (evmac-appcond->name appcond) thm-name thm-names) hints names-to-avoid))))
Theorem:
(defthm pseudo-event-form-listp-of-evmac-appcond-theorem-list.events (b* (((mv ?events ?thm-names ?new-hints ?updated-names-to-avoid) (evmac-appcond-theorem-list appconds hints names-to-avoid print ctx state))) (pseudo-event-form-listp events)) :rule-classes :rewrite)
Theorem:
(defthm keyword-symbol-alistp-of-evmac-appcond-theorem-list.thm-names (implies (evmac-appcond-listp appconds) (b* (((mv ?events ?thm-names ?new-hints ?updated-names-to-avoid) (evmac-appcond-theorem-list appconds hints names-to-avoid print ctx state))) (keyword-symbol-alistp thm-names))) :rule-classes :rewrite)
Theorem:
(defthm evmac-input-hints-p-of-evmac-appcond-theorem-list.new-hints (implies (evmac-input-hints-p hints) (b* (((mv ?events ?thm-names ?new-hints ?updated-names-to-avoid) (evmac-appcond-theorem-list appconds hints names-to-avoid print ctx state))) (evmac-input-hints-p new-hints))) :rule-classes :rewrite)
Theorem:
(defthm symbol-listp-of-evmac-appcond-theorem-list.updated-names-to-avoid (implies (symbol-listp names-to-avoid) (b* (((mv ?events ?thm-names ?new-hints ?updated-names-to-avoid) (evmac-appcond-theorem-list appconds hints names-to-avoid print ctx state))) (symbol-listp updated-names-to-avoid))) :rule-classes :rewrite)