		Search-engine friendly clone of the ACL2 documentation.

Name-database

Vl-namedb-plain-names

Generate a list of fresh names.

Signature
(vl-namedb-plain-names names db) → (mv fresh-names new-db)
Arguments: names — Guard (string-listp names).; db — Guard (vl-namedb-p db).
Returns: fresh-names — Type (string-listp fresh-names).; new-db — Type (vl-namedb-p new-db).

When possible, fresh-names are just names. When this is not possible due to name collisions, some of the fresh_names may have additional indexes as in vl-namedb-indexed-name, and notes may be printed.

Definitions and Theorems

Function: vl-namedb-plain-names

(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: string-listp-of-vl-namedb-plain-names.fresh-names

(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: vl-namedb-p-of-vl-namedb-plain-names.new-db

(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: vl-namedb-plain-names-are-fresh

(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: vl-namedb-allnames-of-vl-namedb-plain-names

(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: vl-namedb-plain-names-of-string-list-fix-names

(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: vl-namedb-plain-names-string-list-equiv-congruence-on-names

(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: vl-namedb-plain-names-of-vl-namedb-fix-db

(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: vl-namedb-plain-names-vl-namedb-equiv-congruence-on-db

(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)