• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
    • Kestrel-books
      • Crypto-hdwallet
      • Apt
      • Error-checking
      • Fty-extensions
      • Isar
      • Kestrel-utilities
      • Soft
      • Bv
      • Imp-language
      • C
      • Event-macros
      • Java
      • Bitcoin
      • Ethereum
      • Yul
      • Zcash
      • ACL2-programming-language
      • Prime-fields
      • Json
      • Syntheto
        • Process-syntheto-toplevel-fn
        • Translation
        • Language
          • Static-semantics
          • Abstract-syntax
          • Outcome
          • Abstract-syntax-operations
            • Subst-expression-fns
              • Subst-expression
              • Subst-initializer-list
              • Subst-initializer
              • Subst-expression-list
              • Subst-branch-list
              • Subst-branch
            • Field-list-to-typed-variable-list
            • Negate-expression
            • Get-function-definition-in-function-definitions
            • Get-function-definition
            • Get-type-definition-in-type-definitions
            • Get-type-definition
            • Get-function-specification
            • Get-type-subset
            • Get-alternative-product
            • Direct-supertype
            • Get-function-header-in-list
            • Equate-expression-lists
            • Get-field-type
            • Get-theorem
            • Get-defined-type-names-in-type-definitions
            • Disjoin-expressions
            • Conjoin-expressions
            • Get-type-product
            • Binary-op-nonstrictp
            • Get-type-sum
            • Get-defined-type-names
            • Equate-expressions
            • Field-to-typed-variable
            • Subst-expression
            • Binary-op-strictp
            • Initializer-list-from-flds-vals
            • Typed-variable-list->-expression-variable-list
            • Typed-variable-list->-expression
            • Variable-substitution
            • Local-variables
            • Identifier-list-names
            • Functions-called
            • Subst-expression-list
            • Subst-branch-list
            • Subst-branch
          • Outcome-list
          • Outcomes
        • Process-syntheto-toplevel
        • Shallow-embedding
      • File-io-light
      • Number-theory
      • Cryptography
      • Lists-light
      • Builtins
      • Axe
      • Solidity
      • Helpers
      • Htclient
      • Typed-lists-light
      • Arithmetic-light
    • X86isa
    • Axe
    • Execloader
  • Math
  • Testing-utilities

• Abstract-syntax-operations

Subst-expression-fns

Mutually recursive functions for expression substitution.

Definitions and Theorems

Function: subst-expression

(defun subst-expression (subst expr)
 (declare (xargs :guard (and (variable-substitutionp subst)
                             (expressionp expr))))
 (let ((__function__ 'subst-expression))
  (declare (ignorable __function__))
  (expression-case
   expr
   :literal (expression-literal expr.get)
   :variable
   (b* ((pair (omap::assoc expr.name
                           (variable-substitution-fix subst))))
     (if pair (cdr pair)
       (expression-variable expr.name)))
   :unary
   (make-expression-unary
        :operator expr.operator
        :operand (subst-expression subst expr.operand))
   :binary
   (make-expression-binary
        :operator expr.operator
        :left-operand (subst-expression subst expr.left-operand)
        :right-operand (subst-expression subst expr.right-operand))
   :if
   (make-expression-if :test (subst-expression subst expr.test)
                       :then (subst-expression subst expr.then)
                       :else (subst-expression subst expr.else))
   :when
   (make-expression-if :test (subst-expression subst expr.test)
                       :then (subst-expression subst expr.then)
                       :else (subst-expression subst expr.else))
   :unless
   (make-expression-if :test (subst-expression subst expr.test)
                       :then (subst-expression subst expr.then)
                       :else (subst-expression subst expr.else))
   :cond
   (make-expression-cond
        :branches (subst-branch-list subst expr.branches))
   :call
   (make-expression-call
        :function expr.function
        :types expr.types
        :arguments (subst-expression-list subst expr.arguments))
   :multi
   (make-expression-multi
        :arguments (subst-expression-list subst expr.arguments))
   :component
   (make-expression-component
        :multi (subst-expression subst expr.multi)
        :index expr.index)
   :bind
   (b*
    ((new-value (subst-expression subst expr.value))
     (new-subst
      (omap::delete*
         (mergesort (typed-variable-list->name-list expr.variables))
         (variable-substitution-fix subst)))
     (new-body (subst-expression new-subst expr.body)))
    (make-expression-bind :variables expr.variables
                          :value new-value
                          :body new-body))
   :product-construct
   (make-expression-product-construct
        :type expr.type
        :fields (subst-initializer-list subst expr.fields))
   :product-field (make-expression-product-field
                       :type expr.type
                       :target (subst-expression subst expr.target)
                       :field expr.field)
   :product-update
   (make-expression-product-update
        :type expr.type
        :target (subst-expression subst expr.target)
        :fields (subst-initializer-list subst expr.fields))
   :sum-construct
   (make-expression-sum-construct
        :type expr.type
        :alternative expr.alternative
        :fields (subst-initializer-list subst expr.fields))
   :sum-field (make-expression-sum-field
                   :type expr.type
                   :target (subst-expression subst expr.target)
                   :alternative expr.alternative
                   :field expr.field)
   :sum-update
   (make-expression-sum-update
        :type expr.type
        :target (subst-expression subst expr.target)
        :alternative expr.alternative
        :fields (subst-initializer-list subst expr.fields))
   :sum-test (make-expression-sum-test
                  :type expr.type
                  :target (subst-expression subst expr.target)
                  :alternative expr.alternative)
   :bad-expression
   (make-expression-bad-expression :info expr.info))))

Function: subst-expression-list

(defun subst-expression-list (subst exprs)
  (declare (xargs :guard (and (variable-substitutionp subst)
                              (expression-listp exprs))))
  (let ((__function__ 'subst-expression-list))
    (declare (ignorable __function__))
    (cond ((endp exprs) nil)
          (t (cons (subst-expression subst (car exprs))
                   (subst-expression-list subst (cdr exprs)))))))

Function: subst-branch

(defun subst-branch (subst branch)
 (declare (xargs :guard (and (variable-substitutionp subst)
                             (branchp branch))))
 (let ((__function__ 'subst-branch))
  (declare (ignorable __function__))
  (make-branch
      :condition (subst-expression subst (branch->condition branch))
      :action (subst-expression subst (branch->action branch)))))

Function: subst-branch-list

(defun subst-branch-list (subst branches)
  (declare (xargs :guard (and (variable-substitutionp subst)
                              (branch-listp branches))))
  (let ((__function__ 'subst-branch-list))
    (declare (ignorable __function__))
    (cond ((endp branches) nil)
          (t (cons (subst-branch subst (car branches))
                   (subst-branch-list subst (cdr branches)))))))

Function: subst-initializer

(defun subst-initializer (subst init)
 (declare (xargs :guard (and (variable-substitutionp subst)
                             (initializerp init))))
 (let ((__function__ 'subst-initializer))
   (declare (ignorable __function__))
   (make-initializer
        :field (initializer->field init)
        :value (subst-expression subst (initializer->value init)))))

Function: subst-initializer-list

(defun subst-initializer-list (subst inits)
  (declare (xargs :guard (and (variable-substitutionp subst)
                              (initializer-listp inits))))
  (let ((__function__ 'subst-initializer-list))
    (declare (ignorable __function__))
    (cond ((endp inits) nil)
          (t (cons (subst-initializer subst (car inits))
                   (subst-initializer-list subst (cdr inits)))))))

Theorem: return-type-of-subst-expression.new-expr

(defthm return-type-of-subst-expression.new-expr
  (b* ((?new-expr (subst-expression subst expr)))
    (expressionp new-expr))
  :rule-classes :rewrite)

Theorem: return-type-of-subst-expression-list.new-exprs

(defthm return-type-of-subst-expression-list.new-exprs
  (b* ((?new-exprs (subst-expression-list subst exprs)))
    (expression-listp new-exprs))
  :rule-classes :rewrite)

Theorem: return-type-of-subst-branch.new-branch

(defthm return-type-of-subst-branch.new-branch
  (b* ((?new-branch (subst-branch subst branch)))
    (branchp new-branch))
  :rule-classes :rewrite)

Theorem: return-type-of-subst-branch-list.new-branches

(defthm return-type-of-subst-branch-list.new-branches
  (b* ((?new-branches (subst-branch-list subst branches)))
    (branch-listp new-branches))
  :rule-classes :rewrite)

Theorem: return-type-of-subst-initializer.new-init

(defthm return-type-of-subst-initializer.new-init
  (b* ((?new-init (subst-initializer subst init)))
    (initializerp new-init))
  :rule-classes :rewrite)

Theorem: return-type-of-subst-initializer-list.new-inits

(defthm return-type-of-subst-initializer-list.new-inits
  (b* ((?new-inits (subst-initializer-list subst inits)))
    (initializer-listp new-inits))
  :rule-classes :rewrite)

Theorem: subst-expression-of-variable-substitution-fix-subst

(defthm subst-expression-of-variable-substitution-fix-subst
  (equal (subst-expression (variable-substitution-fix subst)
                           expr)
         (subst-expression subst expr)))

Theorem: subst-expression-of-expression-fix-expr

(defthm subst-expression-of-expression-fix-expr
  (equal (subst-expression subst (expression-fix expr))
         (subst-expression subst expr)))

Theorem: subst-expression-list-of-variable-substitution-fix-subst

(defthm subst-expression-list-of-variable-substitution-fix-subst
  (equal (subst-expression-list (variable-substitution-fix subst)
                                exprs)
         (subst-expression-list subst exprs)))

Theorem: subst-expression-list-of-expression-list-fix-exprs

(defthm subst-expression-list-of-expression-list-fix-exprs
  (equal (subst-expression-list subst (expression-list-fix exprs))
         (subst-expression-list subst exprs)))

Theorem: subst-branch-of-variable-substitution-fix-subst

(defthm subst-branch-of-variable-substitution-fix-subst
  (equal (subst-branch (variable-substitution-fix subst)
                       branch)
         (subst-branch subst branch)))

Theorem: subst-branch-of-branch-fix-branch

(defthm subst-branch-of-branch-fix-branch
  (equal (subst-branch subst (branch-fix branch))
         (subst-branch subst branch)))

Theorem: subst-branch-list-of-variable-substitution-fix-subst

(defthm subst-branch-list-of-variable-substitution-fix-subst
  (equal (subst-branch-list (variable-substitution-fix subst)
                            branches)
         (subst-branch-list subst branches)))

Theorem: subst-branch-list-of-branch-list-fix-branches

(defthm subst-branch-list-of-branch-list-fix-branches
  (equal (subst-branch-list subst (branch-list-fix branches))
         (subst-branch-list subst branches)))

Theorem: subst-initializer-of-variable-substitution-fix-subst

(defthm subst-initializer-of-variable-substitution-fix-subst
  (equal (subst-initializer (variable-substitution-fix subst)
                            init)
         (subst-initializer subst init)))

Theorem: subst-initializer-of-initializer-fix-init

(defthm subst-initializer-of-initializer-fix-init
  (equal (subst-initializer subst (initializer-fix init))
         (subst-initializer subst init)))

Theorem: subst-initializer-list-of-variable-substitution-fix-subst

(defthm subst-initializer-list-of-variable-substitution-fix-subst
  (equal (subst-initializer-list (variable-substitution-fix subst)
                                 inits)
         (subst-initializer-list subst inits)))

Theorem: subst-initializer-list-of-initializer-list-fix-inits

(defthm subst-initializer-list-of-initializer-list-fix-inits
  (equal (subst-initializer-list subst (initializer-list-fix inits))
         (subst-initializer-list subst inits)))

Theorem: subst-expression-variable-substitution-equiv-congruence-on-subst

(defthm
   subst-expression-variable-substitution-equiv-congruence-on-subst
  (implies (variable-substitution-equiv subst subst-equiv)
           (equal (subst-expression subst expr)
                  (subst-expression subst-equiv expr)))
  :rule-classes :congruence)

Theorem: subst-expression-expression-equiv-congruence-on-expr

(defthm subst-expression-expression-equiv-congruence-on-expr
  (implies (expression-equiv expr expr-equiv)
           (equal (subst-expression subst expr)
                  (subst-expression subst expr-equiv)))
  :rule-classes :congruence)

Theorem: subst-expression-list-variable-substitution-equiv-congruence-on-subst

(defthm
 subst-expression-list-variable-substitution-equiv-congruence-on-subst
 (implies (variable-substitution-equiv subst subst-equiv)
          (equal (subst-expression-list subst exprs)
                 (subst-expression-list subst-equiv exprs)))
 :rule-classes :congruence)

Theorem: subst-expression-list-expression-list-equiv-congruence-on-exprs

(defthm
    subst-expression-list-expression-list-equiv-congruence-on-exprs
  (implies (expression-list-equiv exprs exprs-equiv)
           (equal (subst-expression-list subst exprs)
                  (subst-expression-list subst exprs-equiv)))
  :rule-classes :congruence)

Theorem: subst-branch-variable-substitution-equiv-congruence-on-subst

(defthm subst-branch-variable-substitution-equiv-congruence-on-subst
  (implies (variable-substitution-equiv subst subst-equiv)
           (equal (subst-branch subst branch)
                  (subst-branch subst-equiv branch)))
  :rule-classes :congruence)

Theorem: subst-branch-branch-equiv-congruence-on-branch

(defthm subst-branch-branch-equiv-congruence-on-branch
  (implies (branch-equiv branch branch-equiv)
           (equal (subst-branch subst branch)
                  (subst-branch subst branch-equiv)))
  :rule-classes :congruence)

Theorem: subst-branch-list-variable-substitution-equiv-congruence-on-subst

(defthm
  subst-branch-list-variable-substitution-equiv-congruence-on-subst
  (implies (variable-substitution-equiv subst subst-equiv)
           (equal (subst-branch-list subst branches)
                  (subst-branch-list subst-equiv branches)))
  :rule-classes :congruence)

Theorem: subst-branch-list-branch-list-equiv-congruence-on-branches

(defthm subst-branch-list-branch-list-equiv-congruence-on-branches
  (implies (branch-list-equiv branches branches-equiv)
           (equal (subst-branch-list subst branches)
                  (subst-branch-list subst branches-equiv)))
  :rule-classes :congruence)

Theorem: subst-initializer-variable-substitution-equiv-congruence-on-subst

(defthm
  subst-initializer-variable-substitution-equiv-congruence-on-subst
  (implies (variable-substitution-equiv subst subst-equiv)
           (equal (subst-initializer subst init)
                  (subst-initializer subst-equiv init)))
  :rule-classes :congruence)

Theorem: subst-initializer-initializer-equiv-congruence-on-init

(defthm subst-initializer-initializer-equiv-congruence-on-init
  (implies (initializer-equiv init init-equiv)
           (equal (subst-initializer subst init)
                  (subst-initializer subst init-equiv)))
  :rule-classes :congruence)

Theorem: subst-initializer-list-variable-substitution-equiv-congruence-on-subst

(defthm
 subst-initializer-list-variable-substitution-equiv-congruence-on-subst
 (implies (variable-substitution-equiv subst subst-equiv)
          (equal (subst-initializer-list subst inits)
                 (subst-initializer-list subst-equiv inits)))
 :rule-classes :congruence)

Theorem: subst-initializer-list-initializer-list-equiv-congruence-on-inits

(defthm
  subst-initializer-list-initializer-list-equiv-congruence-on-inits
  (implies (initializer-list-equiv inits inits-equiv)
           (equal (subst-initializer-list subst inits)
                  (subst-initializer-list subst inits-equiv)))
  :rule-classes :congruence)

Subtopics

Subst-expression

Apply a substitution to an expression.

Subst-initializer-list

Apply a substitution to a list of initializers.

Subst-initializer

Apply a substitution to an initializer.

Subst-expression-list

Apply a substitution to a list of expressions.

Subst-branch-list

Apply a substitution to a list of branches.

Subst-branch

Apply a substitution to a branch.