		Search-engine friendly clone of the ACL2 documentation.

Decomp.lisp

Svex-decomp-process-env-term

Signature
(svex-decomp-process-env-term x vars) → (mv err sval symenv)
Arguments: x — Guard (svdecomp-symenv-p x).; vars — Guard (svarlist-p vars).
Returns: sval — Type (svex-alist-p sval).; symenv — Type (svdecomp-symenv-p symenv), given the guard.

Definitions and Theorems

Function: svex-decomp-process-env-term

(defun svex-decomp-process-env-term (x vars)
  (declare (xargs :guard (and (svdecomp-symenv-p x)
                              (svarlist-p vars))))
  (let ((__function__ 'svex-decomp-process-env-term))
    (declare (ignorable __function__))
    (b* ((xsymenv (with-fast-alist x (svdecomp-env-extract vars x)))
         ((mv err base-env envmap)
          (alist-collect-compositions xsymenv))
         ((when err) (mv err nil nil))
         ((mv err envunion)
          (envmap-extract-union-env envmap))
         ((when err) (mv err nil nil))
         ((mv err fullenv)
          (svdecomp-symenv-compat-union base-env envunion))
         ((when err) (mv err nil nil)))
      (mv nil (envmap->svex-alist envmap)
          fullenv))))

Theorem: svex-alist-p-of-svex-decomp-process-env-term.sval

(defthm svex-alist-p-of-svex-decomp-process-env-term.sval
  (b* (((mv ?err ?sval ?symenv)
        (svex-decomp-process-env-term x vars)))
    (svex-alist-p sval))
  :rule-classes :rewrite)

Theorem: svdecomp-symenv-p-of-svex-decomp-process-env-term.symenv

(defthm svdecomp-symenv-p-of-svex-decomp-process-env-term.symenv
  (implies (and (svdecomp-symenv-p x)
                (svarlist-p vars))
           (b* (((mv ?err ?sval ?symenv)
                 (svex-decomp-process-env-term x vars)))
             (svdecomp-symenv-p symenv)))
  :rule-classes :rewrite)

Theorem: svex-decomp-process-env-correct

(defthm svex-decomp-process-env-correct
 (b* (((mv err sval symenv)
       (svex-decomp-process-env-term x vars))
      (env (svdecomp-ev-symenv symenv a)))
  (implies
   (and (not err)
        (member (svar-fix k)
                (svarlist-fix vars)))
   (and
    (implies
         (svar-lookup k sval)
         (4vec-equiv (svex-eval (cdr (svar-lookup k sval))
                                env)
                     (svex-env-lookup k (svdecomp-ev-symenv x a))))
    (implies
       (not (svar-lookup k sval))
       (and (svar-lookup k symenv)
            (4vec-equiv
                 (svdecomp-ev (cdr (svar-lookup k symenv))
                              a)
                 (svex-env-lookup k (svdecomp-ev-symenv x a)))))))))

Theorem: svex-eval-with-svex-decomp-process-env

(defthm svex-eval-with-svex-decomp-process-env
  (b* (((mv err sval symenv)
        (svex-decomp-process-env-term env1 vars))
       (env (svdecomp-ev-symenv symenv a)))
    (implies
         (and (not err)
              (double-rewrite (subsetp (svex-vars x)
                                       (svarlist-fix vars))))
         (equal (svex-eval x
                           (append (svex-alist-eval sval env) env))
                (svex-eval x (svdecomp-ev-symenv env1 a))))))

Theorem: svexlist-eval-with-svex-decomp-process-env

(defthm svexlist-eval-with-svex-decomp-process-env
 (b* (((mv err sval symenv)
       (svex-decomp-process-env-term env1 vars))
      (env (svdecomp-ev-symenv symenv a)))
  (implies
      (and (not err)
           (double-rewrite (subsetp (svexlist-vars x)
                                    (svarlist-fix vars))))
      (equal (svexlist-eval x
                            (append (svex-alist-eval sval env) env))
             (svexlist-eval x (svdecomp-ev-symenv env1 a))))))

Theorem: svex-decomp-process-env-term-of-svarlist-fix-vars

(defthm svex-decomp-process-env-term-of-svarlist-fix-vars
  (equal (svex-decomp-process-env-term x (svarlist-fix vars))
         (svex-decomp-process-env-term x vars)))

Theorem: svex-decomp-process-env-term-svarlist-equiv-congruence-on-vars

(defthm
     svex-decomp-process-env-term-svarlist-equiv-congruence-on-vars
  (implies (svarlist-equiv vars vars-equiv)
           (equal (svex-decomp-process-env-term x vars)
                  (svex-decomp-process-env-term x vars-equiv)))
  :rule-classes :congruence)