		Search-engine friendly clone of the ACL2 documentation.

Vl-modulelist-p

Vl-modulelist->modinsts

(vl-modulelist->modinsts x) applies vl-module->modinsts to every member of the list x, and appends together all the resulting lists.

This is an ordinary defmapappend.

Function: vl-modulelist->modinsts

(defun vl-modulelist->modinsts (x)
  (declare (xargs :guard (vl-modulelist-p x)))
  (mbe :logic
       (if (consp x)
           (append (vl-module->modinsts (car x))
                   (vl-modulelist->modinsts (cdr x)))
         nil)
       :exec (reverse (vl-modulelist->modinsts-exec x nil))))

Definitions and Theorems

Function: vl-modulelist->modinsts-exec

(defun vl-modulelist->modinsts-exec (x acc)
  (declare (xargs :guard (vl-modulelist-p x)))
  (if (consp x)
      (vl-modulelist->modinsts-exec
           (cdr x)
           (revappend-without-guard (vl-module->modinsts (car x))
                                    acc))
    acc))

Function: vl-modulelist->modinsts

(defun vl-modulelist->modinsts (x)
  (declare (xargs :guard (vl-modulelist-p x)))
  (mbe :logic
       (if (consp x)
           (append (vl-module->modinsts (car x))
                   (vl-modulelist->modinsts (cdr x)))
         nil)
       :exec (reverse (vl-modulelist->modinsts-exec x nil))))

Theorem: vl-modulelist->modinsts-exec-removal

(defthm vl-modulelist->modinsts-exec-removal
  (equal (vl-modulelist->modinsts-exec acl2::x acl2::acc)
         (revappend (vl-modulelist->modinsts acl2::x)
                    acl2::acc))
  :rule-classes ((:rewrite)))

Theorem: set-equiv-congruence-over-vl-modulelist->modinsts

(defthm set-equiv-congruence-over-vl-modulelist->modinsts
  (implies (set-equiv acl2::x acl2::y)
           (set-equiv (vl-modulelist->modinsts acl2::x)
                      (vl-modulelist->modinsts acl2::y)))
  :rule-classes ((:congruence)))

Theorem: subsetp-of-vl-modulelist->modinsts-when-subsetp

(defthm subsetp-of-vl-modulelist->modinsts-when-subsetp
  (implies (subsetp acl2::x acl2::y)
           (subsetp (vl-modulelist->modinsts acl2::x)
                    (vl-modulelist->modinsts acl2::y)))
  :rule-classes ((:rewrite)))

Theorem: member-in-vl-modulelist->modinsts

(defthm member-in-vl-modulelist->modinsts
  (implies (and (member acl2::k (vl-module->modinsts acl2::j))
                (member acl2::j acl2::x))
           (member acl2::k
                   (vl-modulelist->modinsts acl2::x)))
  :rule-classes ((:rewrite)))

Theorem: vl-modulelist->modinsts-of-list-fix

(defthm vl-modulelist->modinsts-of-list-fix
  (equal (vl-modulelist->modinsts (list-fix acl2::x))
         (vl-modulelist->modinsts acl2::x))
  :rule-classes ((:rewrite)))

Theorem: vl-modulelist->modinsts-of-append

(defthm vl-modulelist->modinsts-of-append
  (equal (vl-modulelist->modinsts (append acl2::a acl2::b))
         (append (vl-modulelist->modinsts acl2::a)
                 (vl-modulelist->modinsts acl2::b)))
  :rule-classes ((:rewrite)))

Theorem: vl-modulelist->modinsts-when-not-consp

(defthm vl-modulelist->modinsts-when-not-consp
  (implies (not (consp acl2::x))
           (equal (vl-modulelist->modinsts acl2::x)
                  nil))
  :rule-classes ((:rewrite)))

Theorem: vl-modulelist->modinsts-of-cons

(defthm vl-modulelist->modinsts-of-cons
  (equal (vl-modulelist->modinsts (cons acl2::a acl2::b))
         (append (vl-module->modinsts acl2::a)
                 (vl-modulelist->modinsts acl2::b)))
  :rule-classes ((:rewrite)))

Theorem: vl-modinstlist-p-of-vl-modulelist->modinsts

(defthm vl-modinstlist-p-of-vl-modulelist->modinsts
  (vl-modinstlist-p (vl-modulelist->modinsts x)))

Theorem: vl-modulelist->modinsts-of-vl-modulelist-fix-x

(defthm vl-modulelist->modinsts-of-vl-modulelist-fix-x
  (equal (vl-modulelist->modinsts (vl-modulelist-fix x))
         (vl-modulelist->modinsts x)))

Theorem: vl-modulelist->modinsts-vl-modulelist-equiv-congruence-on-x

(defthm vl-modulelist->modinsts-vl-modulelist-equiv-congruence-on-x
  (implies (vl-modulelist-equiv x x-equiv)
           (equal (vl-modulelist->modinsts x)
                  (vl-modulelist->modinsts x-equiv)))
  :rule-classes :congruence)