Generate a list of fresh names.
(vl-namedb-plain-names names db) → (mv fresh-names new-db)
When possible,
Function:
(defun vl-namedb-plain-names (names db) (declare (xargs :guard (and (string-listp names) (vl-namedb-p db)))) (let ((__function__ 'vl-namedb-plain-names)) (declare (ignorable __function__)) (b* (((when (atom names)) (mv nil (vl-namedb-fix db))) ((mv name1 db) (vl-namedb-plain-name (car names) db)) ((mv rest db) (vl-namedb-plain-names (cdr names) db))) (mv (cons name1 rest) db))))
Theorem:
(defthm string-listp-of-vl-namedb-plain-names.fresh-names (b* (((mv ?fresh-names ?new-db) (vl-namedb-plain-names names db))) (string-listp fresh-names)) :rule-classes :rewrite)
Theorem:
(defthm vl-namedb-p-of-vl-namedb-plain-names.new-db (b* (((mv ?fresh-names ?new-db) (vl-namedb-plain-names names db))) (vl-namedb-p new-db)) :rule-classes :rewrite)
Theorem:
(defthm vl-namedb-plain-names-are-fresh (implies (member-equal a (vl-namedb-allnames db)) (not (member-equal a (mv-nth 0 (vl-namedb-plain-names names db))))))
Theorem:
(defthm vl-namedb-allnames-of-vl-namedb-plain-names (equal (vl-namedb-allnames (mv-nth 1 (vl-namedb-plain-names names db))) (revappend (mv-nth 0 (vl-namedb-plain-names names db)) (vl-namedb-allnames db))))
Theorem:
(defthm vl-namedb-plain-names-of-string-list-fix-names (equal (vl-namedb-plain-names (string-list-fix names) db) (vl-namedb-plain-names names db)))
Theorem:
(defthm vl-namedb-plain-names-string-list-equiv-congruence-on-names (implies (str::string-list-equiv names names-equiv) (equal (vl-namedb-plain-names names db) (vl-namedb-plain-names names-equiv db))) :rule-classes :congruence)
Theorem:
(defthm vl-namedb-plain-names-of-vl-namedb-fix-db (equal (vl-namedb-plain-names names (vl-namedb-fix db)) (vl-namedb-plain-names names db)))
Theorem:
(defthm vl-namedb-plain-names-vl-namedb-equiv-congruence-on-db (implies (vl-namedb-equiv db db-equiv) (equal (vl-namedb-plain-names names db) (vl-namedb-plain-names names db-equiv))) :rule-classes :congruence)