		Search-engine friendly clone of the ACL2 documentation.

Install-not-normalized-event-lst

Create a list of event forms to install the non-normalized definitions of a list of functions, ensuring that the names of the theorems will not cause a conflict.

Signature
(install-not-normalized-event-lst fns local names-to-avoid wrld) → (mv events names updated-names-to-avoid)
Arguments: fns — Functions to install the non-normalized definitions of.
Guard (symbol-listp fns).; local — Make the event forms local or not.
Guard (booleanp local).; names-to-avoid — Avoid these as theorem names.
Guard (symbol-listp names-to-avoid).; wrld — Guard (plist-worldp wrld).
Returns: events — Type (pseudo-event-form-listp events).; names — The names of the theorems.
Type (symbol-listp names).; updated-names-to-avoid — The input list names-to-avoid augmented with names.
Type (symbol-listp updated-names-to-avoid), given (symbol-listp names-to-avoid).

Ensure that the names of the theorems are not already in use and are not among a list of names to avoid. Start with the default names (i.e. the concatenation of the names of each function suffixed with $not-normalized) and ensure their uniqueness via fresh-logical-name-with-$s-suffix.

Definitions and Theorems

Function: install-not-normalized-event-lst

(defun
 install-not-normalized-event-lst
 (fns local names-to-avoid wrld)
 (declare (xargs :guard (and (symbol-listp fns)
                             (booleanp local)
                             (symbol-listp names-to-avoid)
                             (plist-worldp wrld))))
 (let
  ((__function__ 'install-not-normalized-event-lst))
  (declare (ignorable __function__))
  (cond
   ((endp fns) (mv nil nil names-to-avoid))
   (t
    (mv-let
     (event name names-to-avoid)
     (install-not-normalized-event (car fns)
                                   local names-to-avoid wrld)
     (mv-let
        (rest-events rest-names names-to-avoid)
        (install-not-normalized-event-lst (cdr fns)
                                          local names-to-avoid wrld)
        (mv (cons event rest-events)
            (cons name rest-names)
            names-to-avoid)))))))

Theorem: pseudo-event-form-listp-of-install-not-normalized-event-lst.events

(defthm
  pseudo-event-form-listp-of-install-not-normalized-event-lst.events
  (b* (((mv ?events ?names ?updated-names-to-avoid)
        (install-not-normalized-event-lst
             fns local names-to-avoid wrld)))
      (pseudo-event-form-listp events))
  :rule-classes :rewrite)

Theorem: symbol-listp-of-install-not-normalized-event-lst.names

(defthm symbol-listp-of-install-not-normalized-event-lst.names
        (b* (((mv ?events ?names ?updated-names-to-avoid)
              (install-not-normalized-event-lst
                   fns local names-to-avoid wrld)))
            (symbol-listp names))
        :rule-classes :rewrite)

Theorem: symbol-listp-of-install-not-normalized-event-lst.updated-names-to-avoid

(defthm
 symbol-listp-of-install-not-normalized-event-lst.updated-names-to-avoid
 (implies (symbol-listp names-to-avoid)
          (b* (((mv ?events ?names ?updated-names-to-avoid)
                (install-not-normalized-event-lst
                     fns local names-to-avoid wrld)))
              (symbol-listp updated-names-to-avoid)))
 :rule-classes :rewrite)