		Search-engine friendly clone of the ACL2 documentation.

Decomp.lisp

Envmap-extract-union-env

Signature
(envmap-extract-union-env envmap) → (mv err union)
Arguments: envmap — Guard (envmap-p envmap).
Returns: union — Type (svdecomp-symenv-p union), given the guard.

Definitions and Theorems

Function: envmap-extract-union-env

(defun envmap-extract-union-env (envmap)
  (declare (xargs :guard (envmap-p envmap)))
  (let ((__function__ 'envmap-extract-union-env))
    (declare (ignorable __function__))
    (b* (((when (atom envmap)) (mv nil nil))
         ((unless (mbt (consp (car envmap))))
          (envmap-extract-union-env (cdr envmap)))
         ((mv err env-alist)
          (map-alist-term-keys-to-val-terms (caar envmap)))
         ((when err) (mv err nil))
         (first-env (envmap-entry-extract-env (cdar envmap)
                                              env-alist))
         ((mv err rest-env)
          (envmap-extract-union-env (cdr envmap)))
         ((when err) (mv err rest-env)))
      (svdecomp-symenv-compat-union first-env rest-env))))

Theorem: svdecomp-symenv-p-of-envmap-extract-union-env.union

(defthm svdecomp-symenv-p-of-envmap-extract-union-env.union
  (implies (and (envmap-p envmap))
           (b* (((mv ?err set::?union)
                 (envmap-extract-union-env envmap)))
             (svdecomp-symenv-p union)))
  :rule-classes :rewrite)

Theorem: keys-of-envmap-extract-union-env

(defthm keys-of-envmap-extract-union-env
 (b* (((mv err union)
       (envmap-extract-union-env envmap)))
   (implies
        (not err)
        (set-equiv (svar-alist-keys union)
                   (svex-alist-vars (envmap->svex-alist envmap))))))

Theorem: lookup-exists-of-envmap-extract-union-env

(defthm lookup-exists-of-envmap-extract-union-env
 (b* (((mv err union)
       (envmap-extract-union-env envmap)))
  (implies
     (not err)
     (iff (svar-lookup k union)
          (member (svar-fix k)
                  (svex-alist-vars (envmap->svex-alist envmap)))))))

Theorem: svex-env-fix-of-svar-alist-fix

(defthm svex-env-fix-of-svar-alist-fix
  (equal (svex-env-fix (svar-alist-fix x))
         (svex-env-fix x)))

Theorem: svar-alist-equiv-refines-svex-env-equiv

(defthm svar-alist-equiv-refines-svex-env-equiv
  (implies (svar-alist-equiv x y)
           (svex-env-equiv x y))
  :rule-classes (:refinement))

Theorem: svar-alist-keys-of-svdecomp-ev-symenv

(defthm svar-alist-keys-of-svdecomp-ev-symenv
  (equal (svar-alist-keys (svdecomp-ev-symenv x a))
         (svar-alist-keys x)))

Theorem: envmap-extract-union-env-correct

(defthm envmap-extract-union-env-correct
 (b* (((mv err union)
       (envmap-extract-union-env envmap))
      (svalist (envmap->svex-alist envmap)))
  (implies
       (not err)
       (equal (svex-alist-eval svalist (svdecomp-ev-symenv union a))
              (svdecomp-ev-envmap envmap a)))))

Theorem: envmap-extract-union-env-correct-lookup-exists

(defthm envmap-extract-union-env-correct-lookup-exists
 (b* (((mv err union)
       (envmap-extract-union-env envmap))
      (svalist (envmap->svex-alist envmap)))
  (implies
      (and (not err) (svar-lookup k svalist))
      (equal (svex-eval (cdr (svar-lookup k svalist))
                        (svdecomp-ev-symenv union a))
             (cdr (svar-lookup k (svdecomp-ev-envmap envmap a)))))))

Theorem: envmap-extract-union-env-of-svex-alist-alist-fix-envmap

(defthm envmap-extract-union-env-of-svex-alist-alist-fix-envmap
  (equal (envmap-extract-union-env (svex-alist-alist-fix envmap))
         (envmap-extract-union-env envmap)))

Theorem: envmap-extract-union-env-svex-alist-alist-equiv-congruence-on-envmap

(defthm
 envmap-extract-union-env-svex-alist-alist-equiv-congruence-on-envmap
 (implies (svex-alist-alist-equiv envmap envmap-equiv)
          (equal (envmap-extract-union-env envmap)
                 (envmap-extract-union-env envmap-equiv)))
 :rule-classes :congruence)