		Search-engine friendly clone of the ACL2 documentation.

Event-macro-applicability-condition-utilities

Evmac-appcond-theorem-list

Lift evmac-appcond-theorem to lists of applicability conditions.

Signature
(evmac-appcond-theorem-list appconds hints names-to-avoid print ctx state) → (mv events thm-names new-hints updated-names-to-avoid)
Arguments: appconds — Guard (evmac-appcond-listp appconds).; hints — Guard (evmac-input-hints-p hints).; names-to-avoid — Guard (symbol-listp names-to-avoid).; print — Guard (evmac-input-print-p print).
Returns: events — Type (pseudo-event-form-listp events).; thm-names — Type (keyword-symbol-alistp thm-names), given (evmac-appcond-listp appconds).; new-hints — Type (evmac-input-hints-p new-hints), given (evmac-input-hints-p hints).; updated-names-to-avoid — Type (symbol-listp updated-names-to-avoid), given (symbol-listp 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 $ characters to ensure the freshness of the theorem names, the names of the theorems cannot be guaranteed or easily predicted, and so it is best to have them be returned, in alist form, by this function.

Definitions and Theorems

Function: evmac-appcond-theorem-list

(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: pseudo-event-form-listp-of-evmac-appcond-theorem-list.events

(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: keyword-symbol-alistp-of-evmac-appcond-theorem-list.thm-names

(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: evmac-input-hints-p-of-evmac-appcond-theorem-list.new-hints

(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: symbol-listp-of-evmac-appcond-theorem-list.updated-names-to-avoid

(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)