• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
    • Vl2014
      • Warnings
      • Primitives
      • Use-set
      • Syntax
      • Getting-started
      • Utilities
      • Loader
      • Transforms
      • Lint
      • Mlib
        • Scopestack
        • Filtering-by-name
        • Vl-namefactory
        • Substitution
          • Vl-packeddimensionlist-subst
          • Vl-namedparamvaluelist-subst
          • Vl-paramvaluelist-subst
          • Vl-paramdecllist-subst
          • Vl-portdecllist-subst
          • Vl-plainarglist-subst
          • Vl-namedarglist-subst
          • Vl-gateinstlist-subst
          • Vl-enumitemlist-subst
          • Vl-vardecllist-subst
          • Vl-modinstlist-subst
          • Vl-initiallist-subst
          • Vl-fundecllist-subst
          • Vl-expr-subst
            • Vl-exprlist-subst
          • Vl-modulelist-subst
          • Vl-evatomlist-subst
          • Vl-assignlist-subst
          • Vl-alwayslist-subst
          • Vl-rangelist-subst
          • Vl-portlist-subst
          • Vl-stmt-subst
          • Vl-maybe-delayoreventcontrol-subst
          • Vl-repeateventcontrol-subst
          • Vl-maybe-packeddimension-subst
          • Vl-delayoreventcontrol-subst
          • Vl-packeddimension-subst
          • Vl-namedparamvalue-subst
          • Vl-module-subst
          • Vl-maybe-paramvalue-subst
          • Vl-paramvalue-subst
          • Vl-paramtype-subst
          • Vl-modinst-subst
          • Vl-maybe-gatedelay-subst
          • Vl-maybe-datatype-subst
          • Vl-interfaceport-subst
          • Vl-gateinst-subst
          • Vl-fundecl-subst
          • Vl-eventcontrol-subst
          • Vl-enumbasetype-subst
          • Vl-delaycontrol-subst
          • Vl-vardecl-subst
          • Vl-regularport-subst
          • Vl-portdecl-subst
          • Vl-plainarg-subst
          • Vl-paramdecl-subst
          • Vl-paramargs-subst
          • Vl-namedarg-subst
          • Vl-maybe-range-subst
          • Vl-gatedelay-subst
          • Vl-enumitem-subst
          • Vl-assign-subst
          • Vl-arguments-subst
          • Vl-range-subst
          • Vl-maybe-expr-subst
          • Vl-initial-subst
          • Vl-evatom-subst
          • Vl-always-subst
          • Vl-port-subst
          • Vl-sigma-count
          • Vl-sigma
        • Allexprs
        • Hid-tools
        • Vl-consteval
        • Range-tools
        • Lvalexprs
        • Hierarchy
        • Finding-by-name
        • Expr-tools
        • Expr-slicing
        • Stripping-functions
        • Stmt-tools
        • Modnamespace
        • Vl-parse-expr-from-str
        • Welltyped
        • Reordering-by-name
        • Flat-warnings
        • Genblob
        • Expr-building
        • Datatype-tools
        • Syscalls
        • Relocate
        • Expr-cleaning
        • Namemangle
        • Caremask
        • Port-tools
        • Lvalues
      • Server
      • Kit
      • Printer
      • Esim-vl
      • Well-formedness
    • Sv
    • Vwsim
    • Fgl
    • Vl
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Substitution

Vl-expr-subst

Substitute into a vl-expr-p.

Signature

(vl-expr-subst x sigma) → new-x

Arguments

x — Guard (vl-expr-p x).

sigma — Guard (vl-sigma-p sigma).

Returns

new-x — Type (vl-expr-p new-x).

We substitute into an expression, replacing any simple identifiers (i.e., atoms which are vl-id-p's) that are bound in sigma with their values.

Note that this function does not descend into attributes. It is not clear whether that is the right behavior, but it seems that the handling of attributes is left up to the implementation.

Theorem: return-type-of-vl-expr-subst.new-x

(defthm return-type-of-vl-expr-subst.new-x
  (b* ((?new-x (vl-expr-subst x sigma)))
    (vl-expr-p new-x))
  :rule-classes :rewrite)

Theorem: return-type-of-vl-exprlist-subst.new-x

(defthm return-type-of-vl-exprlist-subst.new-x
  (b* ((?new-x (vl-exprlist-subst x sigma)))
    (and (vl-exprlist-p new-x)
         (equal (len new-x) (len x))))
  :rule-classes :rewrite)

Theorem: vl-exprlist-subst-of-update-nth

(defthm vl-exprlist-subst-of-update-nth
 (implies
      (<= (nfix acl2::n) (len acl2::x))
      (equal (vl-exprlist-subst (update-nth acl2::n acl2::v acl2::x)
                                sigma)
             (update-nth acl2::n (vl-expr-subst acl2::v sigma)
                         (vl-exprlist-subst acl2::x sigma))))
 :rule-classes ((:rewrite)))

Theorem: vl-exprlist-subst-of-revappend

(defthm vl-exprlist-subst-of-revappend
  (equal (vl-exprlist-subst (revappend acl2::x acl2::y)
                            sigma)
         (revappend (vl-exprlist-subst acl2::x sigma)
                    (vl-exprlist-subst acl2::y sigma)))
  :rule-classes ((:rewrite)))

Theorem: nthcdr-of-vl-exprlist-subst

(defthm nthcdr-of-vl-exprlist-subst
  (equal (nthcdr acl2::n
                 (vl-exprlist-subst acl2::x sigma))
         (vl-exprlist-subst (nthcdr acl2::n acl2::x)
                            sigma))
  :rule-classes ((:rewrite)))

Theorem: nth-of-vl-exprlist-subst

(defthm nth-of-vl-exprlist-subst
  (equal (nth acl2::n
              (vl-exprlist-subst acl2::x sigma))
         (and (< (nfix acl2::n) (len acl2::x))
              (vl-expr-subst (nth acl2::n acl2::x)
                             sigma)))
  :rule-classes ((:rewrite)))

Theorem: vl-exprlist-subst-of-take

(defthm vl-exprlist-subst-of-take
  (implies (<= (nfix acl2::n) (len acl2::x))
           (equal (vl-exprlist-subst (take acl2::n acl2::x)
                                     sigma)
                  (take acl2::n
                        (vl-exprlist-subst acl2::x sigma))))
  :rule-classes ((:rewrite)))

Theorem: set-equiv-congruence-over-vl-exprlist-subst

(defthm set-equiv-congruence-over-vl-exprlist-subst
  (implies (set-equiv acl2::x acl2::y)
           (set-equiv (vl-exprlist-subst acl2::x sigma)
                      (vl-exprlist-subst acl2::y sigma)))
  :rule-classes ((:congruence)))

Theorem: subsetp-of-vl-exprlist-subst-when-subsetp

(defthm subsetp-of-vl-exprlist-subst-when-subsetp
  (implies (subsetp acl2::x acl2::y)
           (subsetp (vl-exprlist-subst acl2::x sigma)
                    (vl-exprlist-subst acl2::y sigma)))
  :rule-classes ((:rewrite)))

Theorem: member-of-vl-expr-subst-in-vl-exprlist-subst

(defthm member-of-vl-expr-subst-in-vl-exprlist-subst
  (implies (member acl2::k acl2::x)
           (member (vl-expr-subst acl2::k sigma)
                   (vl-exprlist-subst acl2::x sigma)))
  :rule-classes ((:rewrite)))

Theorem: vl-exprlist-subst-of-rev

(defthm vl-exprlist-subst-of-rev
  (equal (vl-exprlist-subst (rev acl2::x) sigma)
         (rev (vl-exprlist-subst acl2::x sigma)))
  :rule-classes ((:rewrite)))

Theorem: vl-exprlist-subst-of-list-fix

(defthm vl-exprlist-subst-of-list-fix
  (equal (vl-exprlist-subst (list-fix acl2::x)
                            sigma)
         (vl-exprlist-subst acl2::x sigma))
  :rule-classes ((:rewrite)))

Theorem: vl-exprlist-subst-of-append

(defthm vl-exprlist-subst-of-append
  (equal (vl-exprlist-subst (append acl2::a acl2::b)
                            sigma)
         (append (vl-exprlist-subst acl2::a sigma)
                 (vl-exprlist-subst acl2::b sigma)))
  :rule-classes ((:rewrite)))

Theorem: cdr-of-vl-exprlist-subst

(defthm cdr-of-vl-exprlist-subst
  (equal (cdr (vl-exprlist-subst acl2::x sigma))
         (vl-exprlist-subst (cdr acl2::x) sigma))
  :rule-classes ((:rewrite)))

Theorem: car-of-vl-exprlist-subst

(defthm car-of-vl-exprlist-subst
  (equal (car (vl-exprlist-subst acl2::x sigma))
         (and (consp acl2::x)
              (vl-expr-subst (car acl2::x) sigma)))
  :rule-classes ((:rewrite)))

Theorem: vl-exprlist-subst-under-iff

(defthm vl-exprlist-subst-under-iff
  (iff (vl-exprlist-subst acl2::x sigma)
       (consp acl2::x))
  :rule-classes ((:rewrite)))

Theorem: consp-of-vl-exprlist-subst

(defthm consp-of-vl-exprlist-subst
  (equal (consp (vl-exprlist-subst acl2::x sigma))
         (consp acl2::x))
  :rule-classes ((:rewrite)))

Theorem: len-of-vl-exprlist-subst

(defthm len-of-vl-exprlist-subst
  (equal (len (vl-exprlist-subst acl2::x sigma))
         (len acl2::x))
  :rule-classes ((:rewrite)))

Theorem: true-listp-of-vl-exprlist-subst

(defthm true-listp-of-vl-exprlist-subst
  (true-listp (vl-exprlist-subst acl2::x sigma))
  :rule-classes :type-prescription)

Theorem: vl-exprlist-subst-when-not-consp

(defthm vl-exprlist-subst-when-not-consp
  (implies (not (consp acl2::x))
           (equal (vl-exprlist-subst acl2::x sigma)
                  nil))
  :rule-classes ((:rewrite)))

Theorem: vl-exprlist-subst-of-cons

(defthm vl-exprlist-subst-of-cons
  (equal (vl-exprlist-subst (cons acl2::a acl2::b)
                            sigma)
         (cons (vl-expr-subst acl2::a sigma)
               (vl-exprlist-subst acl2::b sigma)))
  :rule-classes ((:rewrite)))

Theorem: vl-expr-subst-of-vl-expr-fix-x

(defthm vl-expr-subst-of-vl-expr-fix-x
  (equal (vl-expr-subst (vl-expr-fix x) sigma)
         (vl-expr-subst x sigma)))

Theorem: vl-expr-subst-of-vl-sigma-fix-sigma

(defthm vl-expr-subst-of-vl-sigma-fix-sigma
  (equal (vl-expr-subst x (vl-sigma-fix sigma))
         (vl-expr-subst x sigma)))

Theorem: vl-exprlist-subst-of-vl-exprlist-fix-x

(defthm vl-exprlist-subst-of-vl-exprlist-fix-x
  (equal (vl-exprlist-subst (vl-exprlist-fix x)
                            sigma)
         (vl-exprlist-subst x sigma)))

Theorem: vl-exprlist-subst-of-vl-sigma-fix-sigma

(defthm vl-exprlist-subst-of-vl-sigma-fix-sigma
  (equal (vl-exprlist-subst x (vl-sigma-fix sigma))
         (vl-exprlist-subst x sigma)))

Theorem: vl-expr-subst-vl-expr-equiv-congruence-on-x

(defthm vl-expr-subst-vl-expr-equiv-congruence-on-x
  (implies (vl-expr-equiv x x-equiv)
           (equal (vl-expr-subst x sigma)
                  (vl-expr-subst x-equiv sigma)))
  :rule-classes :congruence)

Theorem: vl-expr-subst-vl-sigma-equiv-congruence-on-sigma

(defthm vl-expr-subst-vl-sigma-equiv-congruence-on-sigma
  (implies (vl-sigma-equiv sigma sigma-equiv)
           (equal (vl-expr-subst x sigma)
                  (vl-expr-subst x sigma-equiv)))
  :rule-classes :congruence)

Theorem: vl-exprlist-subst-vl-exprlist-equiv-congruence-on-x

(defthm vl-exprlist-subst-vl-exprlist-equiv-congruence-on-x
  (implies (vl-exprlist-equiv x x-equiv)
           (equal (vl-exprlist-subst x sigma)
                  (vl-exprlist-subst x-equiv sigma)))
  :rule-classes :congruence)

Theorem: vl-exprlist-subst-vl-sigma-equiv-congruence-on-sigma

(defthm vl-exprlist-subst-vl-sigma-equiv-congruence-on-sigma
  (implies (vl-sigma-equiv sigma sigma-equiv)
           (equal (vl-exprlist-subst x sigma)
                  (vl-exprlist-subst x sigma-equiv)))
  :rule-classes :congruence)

Theorem: consp-of-vl-expr-subst

(defthm consp-of-vl-expr-subst
  (consp (vl-expr-subst x sigma))
  :rule-classes :type-prescription)

Subtopics

Vl-exprlist-subst