		Search-engine friendly clone of the ACL2 documentation.

Vl-bindelim-insttable

Vl-bindelim-extend-insttable

Straightforward extension of the vl-bindelim-insttable with a bunch of instances from some context.

Signature
(vl-bindelim-extend-insttable x ctx genp bindp itbl) → new-itbl
Arguments: x — Guard (vl-modinstlist-p x).; ctx — Guard (vl-bindcontext-p ctx).; genp — Guard (booleanp genp).; bindp — Guard (booleanp bindp).; itbl — Guard (vl-bindelim-insttable-p itbl).
Returns: new-itbl — Type (vl-bindelim-insttable-p new-itbl).

Definitions and Theorems

Function: vl-bindelim-extend-insttable

(defun vl-bindelim-extend-insttable (x ctx genp bindp itbl)
  (declare (xargs :guard (and (vl-modinstlist-p x)
                              (vl-bindcontext-p ctx)
                              (booleanp genp)
                              (booleanp bindp)
                              (vl-bindelim-insttable-p itbl))))
  (let ((__function__ 'vl-bindelim-extend-insttable))
    (declare (ignorable __function__))
    (b* ((x (vl-modinstlist-fix x))
         (itbl (vl-bindelim-insttable-fix itbl))
         ((when (atom x)) itbl)
         ((vl-modinst inst1) (first x))
         (item (make-vl-bindelim-institem :ctx ctx
                                          :inst inst1
                                          :genp genp
                                          :bindp bindp))
         (prev-items (cdr (hons-get inst1.modname itbl)))
         (new-items (cons item prev-items))
         (itbl (hons-acons inst1.modname new-items itbl)))
      (vl-bindelim-extend-insttable (rest x)
                                    ctx genp bindp itbl))))

Theorem: vl-bindelim-insttable-p-of-vl-bindelim-extend-insttable

(defthm vl-bindelim-insttable-p-of-vl-bindelim-extend-insttable
  (b*
   ((new-itbl (vl-bindelim-extend-insttable x ctx genp bindp itbl)))
   (vl-bindelim-insttable-p new-itbl))
  :rule-classes :rewrite)

Theorem: vl-bindelim-extend-insttable-of-vl-modinstlist-fix-x

(defthm vl-bindelim-extend-insttable-of-vl-modinstlist-fix-x
  (equal (vl-bindelim-extend-insttable (vl-modinstlist-fix x)
                                       ctx genp bindp itbl)
         (vl-bindelim-extend-insttable x ctx genp bindp itbl)))

Theorem: vl-bindelim-extend-insttable-vl-modinstlist-equiv-congruence-on-x

(defthm
  vl-bindelim-extend-insttable-vl-modinstlist-equiv-congruence-on-x
 (implies
   (vl-modinstlist-equiv x x-equiv)
   (equal
        (vl-bindelim-extend-insttable x ctx genp bindp itbl)
        (vl-bindelim-extend-insttable x-equiv ctx genp bindp itbl)))
 :rule-classes :congruence)

Theorem: vl-bindelim-extend-insttable-of-vl-bindcontext-fix-ctx

(defthm vl-bindelim-extend-insttable-of-vl-bindcontext-fix-ctx
  (equal (vl-bindelim-extend-insttable x (vl-bindcontext-fix ctx)
                                       genp bindp itbl)
         (vl-bindelim-extend-insttable x ctx genp bindp itbl)))

Theorem: vl-bindelim-extend-insttable-vl-bindcontext-equiv-congruence-on-ctx

(defthm
 vl-bindelim-extend-insttable-vl-bindcontext-equiv-congruence-on-ctx
 (implies
   (vl-bindcontext-equiv ctx ctx-equiv)
   (equal
        (vl-bindelim-extend-insttable x ctx genp bindp itbl)
        (vl-bindelim-extend-insttable x ctx-equiv genp bindp itbl)))
 :rule-classes :congruence)

Theorem: vl-bindelim-extend-insttable-of-bool-fix-genp

(defthm vl-bindelim-extend-insttable-of-bool-fix-genp
  (equal (vl-bindelim-extend-insttable x ctx (acl2::bool-fix genp)
                                       bindp itbl)
         (vl-bindelim-extend-insttable x ctx genp bindp itbl)))

Theorem: vl-bindelim-extend-insttable-iff-congruence-on-genp

(defthm vl-bindelim-extend-insttable-iff-congruence-on-genp
 (implies
   (iff genp genp-equiv)
   (equal
        (vl-bindelim-extend-insttable x ctx genp bindp itbl)
        (vl-bindelim-extend-insttable x ctx genp-equiv bindp itbl)))
 :rule-classes :congruence)

Theorem: vl-bindelim-extend-insttable-of-bool-fix-bindp

(defthm vl-bindelim-extend-insttable-of-bool-fix-bindp
 (equal
     (vl-bindelim-extend-insttable x ctx genp (acl2::bool-fix bindp)
                                   itbl)
     (vl-bindelim-extend-insttable x ctx genp bindp itbl)))

Theorem: vl-bindelim-extend-insttable-iff-congruence-on-bindp

(defthm vl-bindelim-extend-insttable-iff-congruence-on-bindp
 (implies
   (iff bindp bindp-equiv)
   (equal
        (vl-bindelim-extend-insttable x ctx genp bindp itbl)
        (vl-bindelim-extend-insttable x ctx genp bindp-equiv itbl)))
 :rule-classes :congruence)

Theorem: vl-bindelim-extend-insttable-of-vl-bindelim-insttable-fix-itbl

(defthm
     vl-bindelim-extend-insttable-of-vl-bindelim-insttable-fix-itbl
  (equal (vl-bindelim-extend-insttable
              x ctx genp
              bindp (vl-bindelim-insttable-fix itbl))
         (vl-bindelim-extend-insttable x ctx genp bindp itbl)))

Theorem: vl-bindelim-extend-insttable-vl-bindelim-insttable-equiv-congruence-on-itbl

(defthm
 vl-bindelim-extend-insttable-vl-bindelim-insttable-equiv-congruence-on-itbl
 (implies
   (vl-bindelim-insttable-equiv itbl itbl-equiv)
   (equal
        (vl-bindelim-extend-insttable x ctx genp bindp itbl)
        (vl-bindelim-extend-insttable x ctx genp bindp itbl-equiv)))
 :rule-classes :congruence)