		Search-engine friendly clone of the ACL2 documentation.

Named-formulas

Named-formulas-to-thm-events

Turn a list of named formulas into theorem events.

Signature
(named-formulas-to-thm-events named-formulas named-hints named-rule-classes enableds locals names-to-avoid wrld) → (mv thm-events thm-names)
Arguments: named-formulas — Named formulas to turn into theorems (an alist from names to untranslated terms).
Guard (symbol-alistp named-formulas).; named-hints — Alist from names of formulas to proof hints for the corresponding theorem events.
Guard (symbol-truelist-alistp named-hints).; named-rule-classes — Alist from names of formulas to rule classes for the corresponding theorem events.
Guard (symbol-alistp named-rule-classes).; enableds — List of names of formulas whose corresponding theorem events must be enabled, or t to make all of them enabled.
Guard (or (symbol-listp enableds) (eq enableds t)).; locals — List of names of formulas whose corresponding theorem events must be local, or t to make all of them local.
Guard (or (symbol-listp locals) (eq locals t)).; names-to-avoid — Avoid these as theorem names.
Guard (symbol-listp names-to-avoid).; wrld — Guard (plist-worldp wrld).
Returns: thm-events — Theorem events (a pseudo-event-form-listp).; thm-names — A symbol-symbol-alistp from names of formulas to names of the corresponding theorem events.

Repeatedly call named-formula-to-thm-event, ensuring that all the theorem names are distinct by incrementally adding the generated names to the list of names to avoid.

Definitions and Theorems

Function: named-formulas-to-thm-events-aux

(defun named-formulas-to-thm-events-aux
       (named-formulas named-hints named-rule-classes
                       enableds locals names-to-avoid
                       rev-thm-events rev-thm-names wrld)
 (declare
      (xargs :guard (and (symbol-alistp named-formulas)
                         (symbol-alistp named-hints)
                         (symbol-alistp named-rule-classes)
                         (or (symbol-listp enableds)
                             (eq enableds t))
                         (or (symbol-listp locals) (eq locals t))
                         (symbol-listp names-to-avoid)
                         (pseudo-event-form-listp rev-thm-events)
                         (symbol-symbol-alistp rev-thm-names)
                         (plist-worldp wrld))))
 (let ((__function__ 'named-formulas-to-thm-events-aux))
  (declare (ignorable __function__))
  (cond
     ((endp named-formulas)
      (mv (reverse rev-thm-events)
          (reverse rev-thm-names)))
     (t (b* ((named-formula (car named-formulas))
             (name (car named-formula))
             (formula (cdr named-formula))
             (hints (cdr (assoc-eq name named-hints)))
             (rule-classes (cdr (assoc-eq name named-rule-classes)))
             (enabled (or (eq enableds t)
                          (member-eq name enableds)))
             (local (or (eq locals t)
                        (member-eq name locals)))
             ((mv thm-event thm-name)
              (named-formula-to-thm-event
                   name formula hints rule-classes
                   enabled local names-to-avoid wrld))
             (names-to-avoid (cons thm-name names-to-avoid))
             (rev-thm-names (acons name thm-name rev-thm-names))
             (rev-thm-events (cons thm-event rev-thm-events)))
          (named-formulas-to-thm-events-aux
               (cdr named-formulas)
               named-hints named-rule-classes
               enabled locals names-to-avoid
               rev-thm-events rev-thm-names wrld))))))

Function: named-formulas-to-thm-events

(defun named-formulas-to-thm-events
       (named-formulas named-hints named-rule-classes
                       enableds locals names-to-avoid wrld)
  (declare
       (xargs :guard (and (symbol-alistp named-formulas)
                          (symbol-truelist-alistp named-hints)
                          (symbol-alistp named-rule-classes)
                          (or (symbol-listp enableds)
                              (eq enableds t))
                          (or (symbol-listp locals) (eq locals t))
                          (symbol-listp names-to-avoid)
                          (plist-worldp wrld))))
  (let ((__function__ 'named-formulas-to-thm-events))
    (declare (ignorable __function__))
    (named-formulas-to-thm-events-aux
         named-formulas
         named-hints named-rule-classes enableds
         locals names-to-avoid nil nil wrld)))