		Search-engine friendly clone of the ACL2 documentation.

Install-not-normalized-event

Create an event form to install the non-normalized definition of a function, ensuring that the name of the theorem will not cause a conflict.

Signature
(install-not-normalized-event fn local names-to-avoid wrld) → (mv event name updated-names-to-avoid)
Arguments: fn — Function to install the non-normalized definition of.
Guard (symbolp fn).; local — Make the event form local or not.
Guard (booleanp local).; names-to-avoid — Avoid these as theorem name.
Guard (symbol-listp names-to-avoid).; wrld — Guard (plist-worldp wrld).
Returns: event — Type (pseudo-event-formp event).; name — The name of the theorem.
Type (symbolp name).; updated-names-to-avoid — The input list names-to-avoid augmented with name.
Type (symbol-listp updated-names-to-avoid), given (symbol-listp names-to-avoid).

Ensure that the name of the theorem is not already in use and is not among a list of names to avoid. Start with the default name (i.e. the concatenation of the name of fn with $not-normalized) and ensure its uniqueness via fresh-logical-name-with-$s-suffix.

Definitions and Theorems

Function: install-not-normalized-event

(defun
 install-not-normalized-event
 (fn local names-to-avoid wrld)
 (declare (xargs :guard (and (symbolp fn)
                             (booleanp local)
                             (symbol-listp names-to-avoid)
                             (plist-worldp wrld))))
 (let
  ((__function__ 'install-not-normalized-event))
  (declare (ignorable __function__))
  (b*
   ((name (install-not-normalized-name fn))
    ((mv name names-to-avoid)
     (fresh-logical-name-with-$s-suffix
          name nil names-to-avoid wrld))
    (event
     (if
      local
      (cons
        'local
        (cons (cons 'install-not-normalized
                    (cons fn
                          (cons ':defthm-name
                                (cons (cons 'quote (cons name 'nil))
                                      '(:allp nil)))))
              'nil))
      (cons 'install-not-normalized
            (cons fn
                  (cons ':defthm-name
                        (cons (cons 'quote (cons name 'nil))
                              '(:allp nil))))))))
   (mv event name names-to-avoid))))

Theorem: pseudo-event-formp-of-install-not-normalized-event.event

(defthm
 pseudo-event-formp-of-install-not-normalized-event.event
 (b* (((mv ?event ?name ?updated-names-to-avoid)
       (install-not-normalized-event fn local names-to-avoid wrld)))
     (pseudo-event-formp event))
 :rule-classes :rewrite)

Theorem: symbolp-of-install-not-normalized-event.name

(defthm
 symbolp-of-install-not-normalized-event.name
 (b* (((mv ?event ?name ?updated-names-to-avoid)
       (install-not-normalized-event fn local names-to-avoid wrld)))
     (symbolp name))
 :rule-classes :rewrite)

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

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