(envmap-extract-union-env envmap) → (mv err union)
Function:
(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:
(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:
(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:
(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:
(defthm svex-env-fix-of-svar-alist-fix (equal (svex-env-fix (svar-alist-fix x)) (svex-env-fix x)))
Theorem:
(defthm svar-alist-equiv-refines-svex-env-equiv (implies (svar-alist-equiv x y) (svex-env-equiv x y)) :rule-classes (:refinement))
Theorem:
(defthm svar-alist-keys-of-svdecomp-ev-symenv (equal (svar-alist-keys (svdecomp-ev-symenv x a)) (svar-alist-keys x)))
Theorem:
(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:
(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:
(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:
(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)