		Search-engine friendly clone of the ACL2 documentation.

Moddb.lisp

Elab-modinst-list-names

Signature
(elab-modinst-list-names x) → names
Arguments: x — Guard (elab-modinst-list-p x).
Returns: names — Type (namelist-p names).

Definitions and Theorems

Function: elab-modinst-list-names

(defun elab-modinst-list-names (x)
  (declare (xargs :guard (elab-modinst-list-p x)))
  (let ((__function__ 'elab-modinst-list-names))
    (declare (ignorable __function__))
    (if (atom x)
        nil
      (cons (name-fix (nth *elab-modinst$c->instname* (car x)))
            (elab-modinst-list-names (cdr x))))))

Theorem: namelist-p-of-elab-modinst-list-names

(defthm namelist-p-of-elab-modinst-list-names
  (b* ((names (elab-modinst-list-names x)))
    (namelist-p names))
  :rule-classes :rewrite)

Theorem: elab-modinst-list-names-of-take

(defthm elab-modinst-list-names-of-take
  (equal (elab-modinst-list-names (take n x))
         (namelist-fix (take n (elab-modinst-list-names x)))))

Theorem: len-of-elab-modinst-list-names

(defthm len-of-elab-modinst-list-names
  (equal (len (elab-modinst-list-names x))
         (len x)))

Theorem: instname-of-nth-index-of-elab-modinst-list-names

(defthm instname-of-nth-index-of-elab-modinst-list-names
 (implies
  (member k (elab-modinst-list-names x))
  (and
   (equal
        (name-fix (nth *elab-modinst$c->instname*
                       (nth (index-of k (elab-modinst-list-names x))
                            x)))
        k)
   (implies
        (name-p (nth *elab-modinst$c->instname*
                     (nth (index-of k (elab-modinst-list-names x))
                          x)))
        (equal (nth *elab-modinst$c->instname*
                    (nth (index-of k (elab-modinst-list-names x))
                         x))
               k)))))

Theorem: member-of-names-when-nth

(defthm member-of-names-when-nth
  (implies (and (equal (nth *elab-modinst$c->instname* (nth n x))
                       k)
                (name-p k)
                (< (nfix n) (len x)))
           (member k (elab-modinst-list-names x))))

Theorem: nth-of-elab-modinst-list-names

(defthm nth-of-elab-modinst-list-names
  (implies (< (nfix n) (len x))
           (equal (nth n (elab-modinst-list-names x))
                  (name-fix (nth *elab-modinst$c->instname*
                                 (nth n x))))))

Theorem: elab-modinst-list-names-of-elab-modinst-list-fix-x

(defthm elab-modinst-list-names-of-elab-modinst-list-fix-x
  (equal (elab-modinst-list-names (elab-modinst-list-fix x))
         (elab-modinst-list-names x)))

Theorem: elab-modinst-list-names-elab-modinst-list-equiv-congruence-on-x

(defthm
    elab-modinst-list-names-elab-modinst-list-equiv-congruence-on-x
  (implies (elab-modinst-list-equiv x x-equiv)
           (equal (elab-modinst-list-names x)
                  (elab-modinst-list-names x-equiv)))
  :rule-classes :congruence)

Theorem: elab-modinst-list-names-of-append

(defthm elab-modinst-list-names-of-append
  (equal (elab-modinst-list-names (append a b))
         (append (elab-modinst-list-names a)
                 (elab-modinst-list-names b))))