Record that a numbered name is in use.
This macro generates an event form to add a numbered name to the table of numbered names in use. If the name is not a numbered name, or it is a numbered name with a wildcard, tha table is unchanged (via an empty progn).
Macro:
(defmacro add-numbered-name-in-use (name) (cons 'make-event (cons (cons 'add-numbered-name-in-use-fn (cons (cons 'quote (cons name 'nil)) '((w state)))) 'nil)))
Function:
(defun add-numbered-name-in-use-fn (name wrld) (declare (xargs :guard (and (symbolp name) (plist-worldp wrld)))) (let ((__function__ 'add-numbered-name-in-use-fn)) (declare (ignorable __function__)) (b* (((mv is-numbered-name base index) (check-numbered-name name wrld))) (if (and is-numbered-name (/= index 0)) (b* ((table (table-alist 'numbered-names-in-use wrld) ) (current-indices (cdr (assoc-eq base table))) (new-indices (add-to-set-eql index current-indices))) (cons 'table (cons 'numbered-names-in-use (cons (cons 'quote (cons base 'nil)) (cons (cons 'quote (cons new-indices 'nil)) 'nil))))) '(progn)))))
Theorem:
(defthm pseudo-event-formp-of-add-numbered-name-in-use-fn (b* ((event (add-numbered-name-in-use-fn name wrld))) (pseudo-event-formp event)) :rule-classes :rewrite)