|
|
|---|
|
|
|
|---|
Mutually recursive functions for expression checking.
Function:
(defun check-expression (expr ctxt) (declare (xargs :guard (and (expressionp expr) (contextp ctxt)))) (let ((__function__ 'check-expression)) (declare (ignorable __function__)) (expression-case expr :literal (check-literal expr.get) :variable (check-variable expr.name ctxt) :unary (check-unary-expression expr.operator expr.operand (check-expression expr.operand ctxt) expr ctxt) :binary (if (binary-op-strictp expr.operator) (check-strict-binary-expression expr.operator expr.left-operand expr.right-operand (check-expression expr.left-operand ctxt) (check-expression expr.right-operand ctxt) expr ctxt) (check-nonstrict-binary-expression expr.operator expr.left-operand expr.right-operand expr ctxt)) :if (check-if/when/unless-expression expr.test nil expr.then expr.else expr ctxt) :when (check-if/when/unless-expression expr.test nil expr.then expr.else expr ctxt) :unless (check-if/when/unless-expression expr.test t expr.then expr.else expr ctxt) :cond (check-cond-expression expr.branches expr ctxt) :call (check-call-expression expr.function expr.types expr.arguments (check-expression-list expr.arguments ctxt) expr ctxt) :multi (check-multi-expression expr.arguments (check-expression-list expr.arguments ctxt)) :component (check-component-expression expr.multi (check-expression expr.multi ctxt) expr.index) :bind (check-bind-expression expr.variables expr.value expr.body expr ctxt) :product-construct (check-product-construct-expression expr.type expr.fields (check-expression-list (initializer-list->value-list expr.fields) ctxt) expr ctxt) :product-field (check-product-field-expression expr.target (check-expression expr.target ctxt) expr.field expr ctxt) :product-update (check-product-update-expression expr.type expr.target (check-expression expr.target ctxt) expr.fields (check-expression-list (initializer-list->value-list expr.fields) ctxt) expr ctxt) :sum-construct (check-sum-construct-expression expr.type expr.alternative expr.fields (check-expression-list (initializer-list->value-list expr.fields) ctxt) expr ctxt) :sum-field (check-sum-field-expression expr.type expr.target (check-expression expr.target ctxt) expr.alternative expr.field expr ctxt) :sum-update (check-sum-update-expression expr.type expr.target (check-expression expr.target ctxt) expr.alternative expr.fields (check-expression-list (initializer-list->value-list expr.fields) ctxt) expr ctxt) :sum-test (check-sum-test-expression expr.target (check-expression expr.target ctxt) expr.alternative expr ctxt) :bad-expression (type-result-err (list :explicit-bad-expression expr.info)))))
Function:
(defun check-nonstrict-binary-expression (op arg1 arg2 expr ctxt) (declare (xargs :guard (and (binary-opp op) (expressionp arg1) (expressionp arg2) (expressionp expr) (contextp ctxt)))) (declare (ignorable expr)) (declare (xargs :guard (binary-op-nonstrictp op))) (let ((__function__ 'check-nonstrict-binary-expression)) (declare (ignorable __function__)) (case (binary-op-kind op) ((:and :implies) (b* ((err-keyword (if (binary-op-case op :and) :type-mismatch-and :type-mismatch-implies)) (left-result (check-expression arg1 ctxt))) (type-result-case left-result :err (type-result-err left-result.info) :ok (b* ((left-type (ensure-single-type left-result.types)) ((when (not left-type)) (type-result-err (list :type-mismatch-multi (expression-fix arg1) left-result.types))) ((unless (subtypep left-type (type-boolean) (context->tops ctxt))) (type-result-err (list err-keyword (expression-fix arg1) left-type (type-boolean)))) (ctxt2 (context-add-condition arg1 ctxt)) (right-result (check-expression arg2 ctxt2))) (type-result-case right-result :err (type-result-err right-result.info) :ok (b* ((right-type (ensure-single-type right-result.types)) ((when (not right-type)) (type-result-err (list :type-mismatch-multi (expression-fix arg2) right-result.types))) ((unless (subtypep right-type (type-boolean) (context->tops ctxt))) (type-result-err (list err-keyword (expression-fix arg2) right-type (type-boolean))))) (make-type-result-ok :types (list (type-boolean)) :obligations (append left-result.obligations right-result.obligations)))))))) (:or (b* ((left-result (check-expression arg1 ctxt))) (type-result-case left-result :err (type-result-err left-result.info) :ok (b* ((left-type (ensure-single-type left-result.types)) ((when (not left-type)) (type-result-err (list :type-mismatch-multi (expression-fix arg1) left-result.types))) ((unless (subtypep left-type (type-boolean) (context->tops ctxt))) (type-result-err (list :type-mismatch-or (expression-fix arg1) left-type (type-boolean)))) (ctxt2 (context-add-condition (negate-expression arg1) ctxt)) (right-result (check-expression arg2 ctxt2))) (type-result-case right-result :err (type-result-err right-result.info) :ok (b* ((right-type (ensure-single-type right-result.types)) ((when (not right-type)) (type-result-err (list :type-mismatch-multi (expression-fix arg2) right-result.types))) ((unless (subtypep right-type (type-boolean) (context->tops ctxt))) (type-result-err (list :type-mismatch-or (expression-fix arg2) right-type (type-boolean))))) (make-type-result-ok :types (list (type-boolean)) :obligations (append left-result.obligations right-result.obligations)))))))) (:implied (b* ((left-result (check-expression arg1 ctxt))) (type-result-case left-result :err (type-result-err left-result.info) :ok (b* ((left-type (ensure-single-type left-result.types)) ((when (not left-type)) (type-result-err (list :type-mismatch-multi (expression-fix arg1) left-result.types))) ((unless (subtypep left-type (type-boolean) (context->tops ctxt))) (type-result-err (list :type-mismatch-implied (expression-fix arg1) left-type (type-boolean)))) (ctxt2 (context-add-condition arg1 ctxt)) (right-result (check-expression arg2 ctxt2))) (type-result-case right-result :err (type-result-err right-result.info) :ok (b* ((right-type (ensure-single-type right-result.types)) ((when (not right-type)) (type-result-err (list :type-mismatch-multi (expression-fix arg2) right-result.types))) ((unless (subtypep right-type (type-boolean) (context->tops ctxt))) (type-result-err (list :type-mismatch-implied (expression-fix arg2) right-type (type-boolean))))) (make-type-result-ok :types (list (type-boolean)) :obligations (append left-result.obligations right-result.obligations)))))))) (t (prog2$ (impossible) (type-result-err :impossible))))))
Function:
(defun check-if/when/unless-expression (test test-negp then else expr ctxt) (declare (xargs :guard (and (expressionp test) (booleanp test-negp) (expressionp then) (expressionp else) (expressionp expr) (contextp ctxt)))) (declare (ignorable expr)) (let ((__function__ 'check-if/when/unless-expression)) (declare (ignorable __function__)) (b* ((test-result (check-expression test ctxt))) (type-result-case test-result :err (type-result-err test-result.info) :ok (b* ((test-type (ensure-single-type test-result.types)) ((when (not test-type)) (type-result-err (list :type-mismatch-multi (expression-fix test) test-result.types))) ((unless (subtypep test-type (type-boolean) (context->tops ctxt))) (type-result-err (list :type-mismatch-if-test (expression-fix test) test-type (type-boolean)))) (ctxt2 (context-add-condition (if test-negp (negate-expression test) test) ctxt)) (then-result (check-expression then ctxt2))) (type-result-case then-result :err (type-result-err then-result.info) :ok (b* ((ctxt2 (context-add-condition (if test-negp test (negate-expression test)) ctxt)) (else-result (check-expression else ctxt2))) (type-result-case else-result :err (type-result-err else-result.info) :ok (b* (((mv okp sup) (supremum-type-list then-result.types else-result.types (context->tops ctxt)))) (if okp (make-type-result-ok :types sup :obligations (append test-result.obligations then-result.obligations else-result.obligations)) (type-result-err (list :no-type-supremum-in-if (expression-fix then) (expression-fix else) then-result.types else-result.types))))))))))))
Function:
(defun check-cond-expression (branches expr ctxt) (declare (xargs :guard (and (branch-listp branches) (expressionp expr) (contextp ctxt)))) (let ((__function__ 'check-cond-expression)) (declare (ignorable __function__)) (b* ((result (check-branch-list branches nil ctxt))) (type-result-case result :err (type-result-err result.info) :ok (b* ((oblig? (non-trivial-proof-obligation (context->obligation-vars ctxt) (context->obligation-hyps ctxt) (disjoin-expressions (branch-list->condition-list branches)) expr))) (make-type-result-ok :types result.types :obligations (append result.obligations oblig?)))))))
Function:
(defun check-bind-expression (vars value body expr ctxt) (declare (xargs :guard (and (typed-variable-listp vars) (expressionp value) (expressionp body) (expressionp expr) (contextp ctxt)))) (declare (ignorable expr)) (let ((__function__ 'check-bind-expression)) (declare (ignorable __function__)) (b* (((mv okp var-names var-types values) (align-let-vars-values vars value)) ((when (not okp)) (type-result-err (list :no-let-variables (expression-fix value) (expression-fix body)))) ((unless (no-duplicatesp-equal var-names)) (type-result-err (list :duplicate-variable-names var-names))) (value-result (check-expression value ctxt))) (type-result-case value-result :err (type-result-err value-result.info) :ok (b* (((unless (= (len values) (len value-result.types))) (type-result-err (list :mismatched-let-types (typed-variable-list-fix vars) value-result.types))) ((mv okp obligs) (match-type-list values value-result.types var-types ctxt)) ((when (not okp)) (type-result-err (list :let-type-mismatch values value-result.types var-types))) (binding (make-binding :variables vars :value value)) (ctxt (context-add-variables (typed-variables-to-variable-context vars) ctxt)) (ctxt (context-add-binding binding ctxt)) (body-result (check-expression body ctxt))) (type-result-case body-result :err (type-result-err body-result.info) :ok (make-type-result-ok :types body-result.types :obligations (append value-result.obligations obligs body-result.obligations))))))))
Function:
(defun check-expression-list (exprs ctxt) (declare (xargs :guard (and (expression-listp exprs) (contextp ctxt)))) (let ((__function__ 'check-expression-list)) (declare (ignorable __function__)) (b* (((when (endp exprs)) (make-type-result-ok :types nil :obligations nil)) (result (check-expression (car exprs) ctxt))) (type-result-case result :err (type-result-err result.info) :ok (b* ((type (ensure-single-type result.types)) ((when (not type)) (type-result-err (list :type-mismatch-multi (expression-fix (car exprs)) result.types))) (obligs result.obligations) (result (check-expression-list (cdr exprs) ctxt))) (type-result-case result :err (type-result-err result.info) :ok (b* ((types result.types) (more-obligs result.obligations)) (make-type-result-ok :types (cons type types) :obligations (append obligs more-obligs)))))))))
Function:
(defun check-branch (branch ctxt) (declare (xargs :guard (and (branchp branch) (contextp ctxt)))) (let ((__function__ 'check-branch)) (declare (ignorable __function__)) (b* (((branch branch) branch) (cond-result (check-expression branch.condition ctxt))) (type-result-case cond-result :err (type-result-err cond-result.info) :ok (b* ((cond-type (ensure-single-type cond-result.types)) ((when (not cond-type)) (type-result-err (list :type-mismatch-multi branch.condition cond-result.types))) ((unless (subtypep cond-type (type-boolean) (context->tops ctxt))) (type-result-err (list :type-mismatch-condition branch.condition cond-type (type-boolean)))) (ctxt2 (context-add-condition branch.condition ctxt)) (act-result (check-expression branch.action ctxt2))) (type-result-case act-result :err (type-result-err act-result.info) :ok (make-type-result-ok :types act-result.types :obligations (append cond-result.obligations act-result.obligations))))))))
Function:
(defun check-branch-list (branches current-sup ctxt) (declare (xargs :guard (and (branch-listp branches) (type-listp current-sup) (contextp ctxt)))) (let ((__function__ 'check-branch-list)) (declare (ignorable __function__)) (b* ((current-sup (type-list-fix current-sup)) ((when (endp branches)) (if current-sup (make-type-result-ok :types current-sup :obligations nil) (type-result-err :empty-conditional))) (branch (car branches)) (result (check-branch branch ctxt))) (type-result-case result :err (type-result-err result.info) :ok (b* (((mv okp new-sup) (if current-sup (supremum-type-list current-sup result.types (context->tops ctxt)) (mv t result.types))) ((unless okp) (type-result-err (list :incompatible-branches current-sup result.types))) (ctxt2 (context-add-condition (negate-expression (branch->condition branch)) ctxt)) (more-result (check-branch-list (cdr branches) new-sup ctxt2))) (type-result-case more-result :err (type-result-err more-result.info) :ok (make-type-result-ok :types more-result.types :obligations (append result.obligations more-result.obligations))))))))
Theorem:
(defthm return-type-of-check-expression.result (b* ((?result (check-expression expr ctxt))) (type-resultp result)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-check-nonstrict-binary-expression.result (b* ((?result (check-nonstrict-binary-expression op arg1 arg2 expr ctxt))) (type-resultp result)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-check-if/when/unless-expression.result (b* ((?result (check-if/when/unless-expression test test-negp then else expr ctxt))) (type-resultp result)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-check-cond-expression.result (b* ((?result (check-cond-expression branches expr ctxt))) (type-resultp result)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-check-bind-expression.result (b* ((?result (check-bind-expression vars value body expr ctxt))) (type-resultp result)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-check-expression-list.result (b* ((?result (check-expression-list exprs ctxt))) (type-resultp result)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-check-branch.result (b* ((?result (check-branch branch ctxt))) (type-resultp result)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-check-branch-list.result (b* ((?result (check-branch-list branches current-sup ctxt))) (type-resultp result)) :rule-classes :rewrite)
Theorem:
(defthm len-of-result-types (b* ((?result (check-expression-list exprs ctxt))) (implies (type-result-case result :ok) (equal (len (type-result-ok->types result)) (len exprs)))))
Theorem:
(defthm check-expression-of-expression-fix-expr (equal (check-expression (expression-fix expr) ctxt) (check-expression expr ctxt)))
Theorem:
(defthm check-expression-of-context-fix-ctxt (equal (check-expression expr (context-fix ctxt)) (check-expression expr ctxt)))
Theorem:
(defthm check-nonstrict-binary-expression-of-binary-op-fix-op (equal (check-nonstrict-binary-expression (binary-op-fix op) arg1 arg2 expr ctxt) (check-nonstrict-binary-expression op arg1 arg2 expr ctxt)))
Theorem:
(defthm check-nonstrict-binary-expression-of-expression-fix-arg1 (equal (check-nonstrict-binary-expression op (expression-fix arg1) arg2 expr ctxt) (check-nonstrict-binary-expression op arg1 arg2 expr ctxt)))
Theorem:
(defthm check-nonstrict-binary-expression-of-expression-fix-arg2 (equal (check-nonstrict-binary-expression op arg1 (expression-fix arg2) expr ctxt) (check-nonstrict-binary-expression op arg1 arg2 expr ctxt)))
Theorem:
(defthm check-nonstrict-binary-expression-of-expression-fix-expr (equal (check-nonstrict-binary-expression op arg1 arg2 (expression-fix expr) ctxt) (check-nonstrict-binary-expression op arg1 arg2 expr ctxt)))
Theorem:
(defthm check-nonstrict-binary-expression-of-context-fix-ctxt (equal (check-nonstrict-binary-expression op arg1 arg2 expr (context-fix ctxt)) (check-nonstrict-binary-expression op arg1 arg2 expr ctxt)))
Theorem:
(defthm check-if/when/unless-expression-of-expression-fix-test (equal (check-if/when/unless-expression (expression-fix test) test-negp then else expr ctxt) (check-if/when/unless-expression test test-negp then else expr ctxt)))
Theorem:
(defthm check-if/when/unless-expression-of-bool-fix-test-negp (equal (check-if/when/unless-expression test (bool-fix test-negp) then else expr ctxt) (check-if/when/unless-expression test test-negp then else expr ctxt)))
Theorem:
(defthm check-if/when/unless-expression-of-expression-fix-then (equal (check-if/when/unless-expression test test-negp (expression-fix then) else expr ctxt) (check-if/when/unless-expression test test-negp then else expr ctxt)))
Theorem:
(defthm check-if/when/unless-expression-of-expression-fix-else (equal (check-if/when/unless-expression test test-negp then (expression-fix else) expr ctxt) (check-if/when/unless-expression test test-negp then else expr ctxt)))
Theorem:
(defthm check-if/when/unless-expression-of-expression-fix-expr (equal (check-if/when/unless-expression test test-negp then else (expression-fix expr) ctxt) (check-if/when/unless-expression test test-negp then else expr ctxt)))
Theorem:
(defthm check-if/when/unless-expression-of-context-fix-ctxt (equal (check-if/when/unless-expression test test-negp then else expr (context-fix ctxt)) (check-if/when/unless-expression test test-negp then else expr ctxt)))
Theorem:
(defthm check-cond-expression-of-branch-list-fix-branches (equal (check-cond-expression (branch-list-fix branches) expr ctxt) (check-cond-expression branches expr ctxt)))
Theorem:
(defthm check-cond-expression-of-expression-fix-expr (equal (check-cond-expression branches (expression-fix expr) ctxt) (check-cond-expression branches expr ctxt)))
Theorem:
(defthm check-cond-expression-of-context-fix-ctxt (equal (check-cond-expression branches expr (context-fix ctxt)) (check-cond-expression branches expr ctxt)))
Theorem:
(defthm check-bind-expression-of-typed-variable-list-fix-vars (equal (check-bind-expression (typed-variable-list-fix vars) value body expr ctxt) (check-bind-expression vars value body expr ctxt)))
Theorem:
(defthm check-bind-expression-of-expression-fix-value (equal (check-bind-expression vars (expression-fix value) body expr ctxt) (check-bind-expression vars value body expr ctxt)))
Theorem:
(defthm check-bind-expression-of-expression-fix-body (equal (check-bind-expression vars value (expression-fix body) expr ctxt) (check-bind-expression vars value body expr ctxt)))
Theorem:
(defthm check-bind-expression-of-expression-fix-expr (equal (check-bind-expression vars value body (expression-fix expr) ctxt) (check-bind-expression vars value body expr ctxt)))
Theorem:
(defthm check-bind-expression-of-context-fix-ctxt (equal (check-bind-expression vars value body expr (context-fix ctxt)) (check-bind-expression vars value body expr ctxt)))
Theorem:
(defthm check-expression-list-of-expression-list-fix-exprs (equal (check-expression-list (expression-list-fix exprs) ctxt) (check-expression-list exprs ctxt)))
Theorem:
(defthm check-expression-list-of-context-fix-ctxt (equal (check-expression-list exprs (context-fix ctxt)) (check-expression-list exprs ctxt)))
Theorem:
(defthm check-branch-of-branch-fix-branch (equal (check-branch (branch-fix branch) ctxt) (check-branch branch ctxt)))
Theorem:
(defthm check-branch-of-context-fix-ctxt (equal (check-branch branch (context-fix ctxt)) (check-branch branch ctxt)))
Theorem:
(defthm check-branch-list-of-branch-list-fix-branches (equal (check-branch-list (branch-list-fix branches) current-sup ctxt) (check-branch-list branches current-sup ctxt)))
Theorem:
(defthm check-branch-list-of-type-list-fix-current-sup (equal (check-branch-list branches (type-list-fix current-sup) ctxt) (check-branch-list branches current-sup ctxt)))
Theorem:
(defthm check-branch-list-of-context-fix-ctxt (equal (check-branch-list branches current-sup (context-fix ctxt)) (check-branch-list branches current-sup ctxt)))
Theorem:
(defthm check-expression-expression-equiv-congruence-on-expr (implies (expression-equiv expr expr-equiv) (equal (check-expression expr ctxt) (check-expression expr-equiv ctxt))) :rule-classes :congruence)
Theorem:
(defthm check-expression-context-equiv-congruence-on-ctxt (implies (context-equiv ctxt ctxt-equiv) (equal (check-expression expr ctxt) (check-expression expr ctxt-equiv))) :rule-classes :congruence)
Theorem:
(defthm check-nonstrict-binary-expression-binary-op-equiv-congruence-on-op (implies (binary-op-equiv op op-equiv) (equal (check-nonstrict-binary-expression op arg1 arg2 expr ctxt) (check-nonstrict-binary-expression op-equiv arg1 arg2 expr ctxt))) :rule-classes :congruence)
Theorem:
(defthm check-nonstrict-binary-expression-expression-equiv-congruence-on-arg1 (implies (expression-equiv arg1 arg1-equiv) (equal (check-nonstrict-binary-expression op arg1 arg2 expr ctxt) (check-nonstrict-binary-expression op arg1-equiv arg2 expr ctxt))) :rule-classes :congruence)
Theorem:
(defthm check-nonstrict-binary-expression-expression-equiv-congruence-on-arg2 (implies (expression-equiv arg2 arg2-equiv) (equal (check-nonstrict-binary-expression op arg1 arg2 expr ctxt) (check-nonstrict-binary-expression op arg1 arg2-equiv expr ctxt))) :rule-classes :congruence)
Theorem:
(defthm check-nonstrict-binary-expression-expression-equiv-congruence-on-expr (implies (expression-equiv expr expr-equiv) (equal (check-nonstrict-binary-expression op arg1 arg2 expr ctxt) (check-nonstrict-binary-expression op arg1 arg2 expr-equiv ctxt))) :rule-classes :congruence)
Theorem:
(defthm check-nonstrict-binary-expression-context-equiv-congruence-on-ctxt (implies (context-equiv ctxt ctxt-equiv) (equal (check-nonstrict-binary-expression op arg1 arg2 expr ctxt) (check-nonstrict-binary-expression op arg1 arg2 expr ctxt-equiv))) :rule-classes :congruence)
Theorem:
(defthm check-if/when/unless-expression-expression-equiv-congruence-on-test (implies (expression-equiv test test-equiv) (equal (check-if/when/unless-expression test test-negp then else expr ctxt) (check-if/when/unless-expression test-equiv test-negp then else expr ctxt))) :rule-classes :congruence)
Theorem:
(defthm check-if/when/unless-expression-iff-congruence-on-test-negp (implies (iff test-negp test-negp-equiv) (equal (check-if/when/unless-expression test test-negp then else expr ctxt) (check-if/when/unless-expression test test-negp-equiv then else expr ctxt))) :rule-classes :congruence)
Theorem:
(defthm check-if/when/unless-expression-expression-equiv-congruence-on-then (implies (expression-equiv then then-equiv) (equal (check-if/when/unless-expression test test-negp then else expr ctxt) (check-if/when/unless-expression test test-negp then-equiv else expr ctxt))) :rule-classes :congruence)
Theorem:
(defthm check-if/when/unless-expression-expression-equiv-congruence-on-else (implies (expression-equiv else else-equiv) (equal (check-if/when/unless-expression test test-negp then else expr ctxt) (check-if/when/unless-expression test test-negp then else-equiv expr ctxt))) :rule-classes :congruence)
Theorem:
(defthm check-if/when/unless-expression-expression-equiv-congruence-on-expr (implies (expression-equiv expr expr-equiv) (equal (check-if/when/unless-expression test test-negp then else expr ctxt) (check-if/when/unless-expression test test-negp then else expr-equiv ctxt))) :rule-classes :congruence)
Theorem:
(defthm check-if/when/unless-expression-context-equiv-congruence-on-ctxt (implies (context-equiv ctxt ctxt-equiv) (equal (check-if/when/unless-expression test test-negp then else expr ctxt) (check-if/when/unless-expression test test-negp then else expr ctxt-equiv))) :rule-classes :congruence)
Theorem:
(defthm check-cond-expression-branch-list-equiv-congruence-on-branches (implies (branch-list-equiv branches branches-equiv) (equal (check-cond-expression branches expr ctxt) (check-cond-expression branches-equiv expr ctxt))) :rule-classes :congruence)
Theorem:
(defthm check-cond-expression-expression-equiv-congruence-on-expr (implies (expression-equiv expr expr-equiv) (equal (check-cond-expression branches expr ctxt) (check-cond-expression branches expr-equiv ctxt))) :rule-classes :congruence)
Theorem:
(defthm check-cond-expression-context-equiv-congruence-on-ctxt (implies (context-equiv ctxt ctxt-equiv) (equal (check-cond-expression branches expr ctxt) (check-cond-expression branches expr ctxt-equiv))) :rule-classes :congruence)
Theorem:
(defthm check-bind-expression-typed-variable-list-equiv-congruence-on-vars (implies (typed-variable-list-equiv vars vars-equiv) (equal (check-bind-expression vars value body expr ctxt) (check-bind-expression vars-equiv value body expr ctxt))) :rule-classes :congruence)
Theorem:
(defthm check-bind-expression-expression-equiv-congruence-on-value (implies (expression-equiv value value-equiv) (equal (check-bind-expression vars value body expr ctxt) (check-bind-expression vars value-equiv body expr ctxt))) :rule-classes :congruence)
Theorem:
(defthm check-bind-expression-expression-equiv-congruence-on-body (implies (expression-equiv body body-equiv) (equal (check-bind-expression vars value body expr ctxt) (check-bind-expression vars value body-equiv expr ctxt))) :rule-classes :congruence)
Theorem:
(defthm check-bind-expression-expression-equiv-congruence-on-expr (implies (expression-equiv expr expr-equiv) (equal (check-bind-expression vars value body expr ctxt) (check-bind-expression vars value body expr-equiv ctxt))) :rule-classes :congruence)
Theorem:
(defthm check-bind-expression-context-equiv-congruence-on-ctxt (implies (context-equiv ctxt ctxt-equiv) (equal (check-bind-expression vars value body expr ctxt) (check-bind-expression vars value body expr ctxt-equiv))) :rule-classes :congruence)
Theorem:
(defthm check-expression-list-expression-list-equiv-congruence-on-exprs (implies (expression-list-equiv exprs exprs-equiv) (equal (check-expression-list exprs ctxt) (check-expression-list exprs-equiv ctxt))) :rule-classes :congruence)
Theorem:
(defthm check-expression-list-context-equiv-congruence-on-ctxt (implies (context-equiv ctxt ctxt-equiv) (equal (check-expression-list exprs ctxt) (check-expression-list exprs ctxt-equiv))) :rule-classes :congruence)
Theorem:
(defthm check-branch-branch-equiv-congruence-on-branch (implies (branch-equiv branch branch-equiv) (equal (check-branch branch ctxt) (check-branch branch-equiv ctxt))) :rule-classes :congruence)
Theorem:
(defthm check-branch-context-equiv-congruence-on-ctxt (implies (context-equiv ctxt ctxt-equiv) (equal (check-branch branch ctxt) (check-branch branch ctxt-equiv))) :rule-classes :congruence)
Theorem:
(defthm check-branch-list-branch-list-equiv-congruence-on-branches (implies (branch-list-equiv branches branches-equiv) (equal (check-branch-list branches current-sup ctxt) (check-branch-list branches-equiv current-sup ctxt))) :rule-classes :congruence)
Theorem:
(defthm check-branch-list-type-list-equiv-congruence-on-current-sup (implies (type-list-equiv current-sup current-sup-equiv) (equal (check-branch-list branches current-sup ctxt) (check-branch-list branches current-sup-equiv ctxt))) :rule-classes :congruence)
Theorem:
(defthm check-branch-list-context-equiv-congruence-on-ctxt (implies (context-equiv ctxt ctxt-equiv) (equal (check-branch-list branches current-sup ctxt) (check-branch-list branches current-sup ctxt-equiv))) :rule-classes :congruence)