		Search-engine friendly clone of the ACL2 documentation.

Basic-bind-elim

Vl-interface-bindelim

Signature
(vl-interface-bindelim x ss itbl delta) → (mv new-x delta)
Arguments: x — Guard (vl-interface-p x).; ss — Guard (vl-scopestack-p ss).; itbl — Guard (vl-bindelim-insttable-p itbl).; delta — Guard (vl-binddelta-p delta).
Returns: new-x — Type (vl-interface-p new-x).; delta — Type (vl-binddelta-p delta).

Definitions and Theorems

Function: vl-interface-bindelim

(defun vl-interface-bindelim (x ss itbl delta)
 (declare (xargs :guard (and (vl-interface-p x)
                             (vl-scopestack-p ss)
                             (vl-bindelim-insttable-p itbl)
                             (vl-binddelta-p delta))))
 (let ((__function__ 'vl-interface-bindelim))
   (declare (ignorable __function__))
   (b*
     (((vl-interface x) (vl-interface-fix x))
      (blob (vl-interface->genblob x))
      ((mv warnings delta new-blob)
       (vl-genblob-bindelim blob ss x itbl delta nil x.warnings))
      (new-x (change-vl-interface (vl-genblob->interface new-blob x)
                                  :warnings warnings)))
     (mv new-x delta))))

Theorem: vl-interface-p-of-vl-interface-bindelim.new-x

(defthm vl-interface-p-of-vl-interface-bindelim.new-x
  (b* (((mv ?new-x ?delta)
        (vl-interface-bindelim x ss itbl delta)))
    (vl-interface-p new-x))
  :rule-classes :rewrite)

Theorem: vl-binddelta-p-of-vl-interface-bindelim.delta

(defthm vl-binddelta-p-of-vl-interface-bindelim.delta
  (b* (((mv ?new-x ?delta)
        (vl-interface-bindelim x ss itbl delta)))
    (vl-binddelta-p delta))
  :rule-classes :rewrite)

Theorem: vl-interface-bindelim-of-vl-interface-fix-x

(defthm vl-interface-bindelim-of-vl-interface-fix-x
  (equal (vl-interface-bindelim (vl-interface-fix x)
                                ss itbl delta)
         (vl-interface-bindelim x ss itbl delta)))

Theorem: vl-interface-bindelim-vl-interface-equiv-congruence-on-x

(defthm vl-interface-bindelim-vl-interface-equiv-congruence-on-x
  (implies (vl-interface-equiv x x-equiv)
           (equal (vl-interface-bindelim x ss itbl delta)
                  (vl-interface-bindelim x-equiv ss itbl delta)))
  :rule-classes :congruence)

Theorem: vl-interface-bindelim-of-vl-scopestack-fix-ss

(defthm vl-interface-bindelim-of-vl-scopestack-fix-ss
  (equal (vl-interface-bindelim x (vl-scopestack-fix ss)
                                itbl delta)
         (vl-interface-bindelim x ss itbl delta)))

Theorem: vl-interface-bindelim-vl-scopestack-equiv-congruence-on-ss

(defthm vl-interface-bindelim-vl-scopestack-equiv-congruence-on-ss
  (implies (vl-scopestack-equiv ss ss-equiv)
           (equal (vl-interface-bindelim x ss itbl delta)
                  (vl-interface-bindelim x ss-equiv itbl delta)))
  :rule-classes :congruence)

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

(defthm vl-interface-bindelim-of-vl-bindelim-insttable-fix-itbl
 (equal (vl-interface-bindelim x ss (vl-bindelim-insttable-fix itbl)
                               delta)
        (vl-interface-bindelim x ss itbl delta)))

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

(defthm
 vl-interface-bindelim-vl-bindelim-insttable-equiv-congruence-on-itbl
 (implies (vl-bindelim-insttable-equiv itbl itbl-equiv)
          (equal (vl-interface-bindelim x ss itbl delta)
                 (vl-interface-bindelim x ss itbl-equiv delta)))
 :rule-classes :congruence)

Theorem: vl-interface-bindelim-of-vl-binddelta-fix-delta

(defthm vl-interface-bindelim-of-vl-binddelta-fix-delta
  (equal (vl-interface-bindelim x ss itbl (vl-binddelta-fix delta))
         (vl-interface-bindelim x ss itbl delta)))

Theorem: vl-interface-bindelim-vl-binddelta-equiv-congruence-on-delta

(defthm vl-interface-bindelim-vl-binddelta-equiv-congruence-on-delta
  (implies (vl-binddelta-equiv delta delta-equiv)
           (equal (vl-interface-bindelim x ss itbl delta)
                  (vl-interface-bindelim x ss itbl delta-equiv)))
  :rule-classes :congruence)