(svex-env-compat-union x y) → (mv err union)
Function:
(defun svex-env-compat-union (x y) (declare (xargs :guard (and (svex-env-p x) (svex-env-p y)))) (let ((__function__ 'svex-env-compat-union)) (declare (ignorable __function__)) (b* (((when (atom x)) (mv nil (svex-env-fix y))) ((unless (mbt (and (consp (car x)) (svar-p (caar x))))) (svex-env-compat-union (cdr x) y)) ((cons var val) (car x)) (val (4vec-fix val)) (look (svar-lookup var (svex-env-fix y))) ((unless (or (not look) (equal (4vec-fix (cdr look)) val))) (mv (msg "Mismatch: key ~x0, val ~x1 versus ~x2~%" var val (4vec-fix (cdr look))) nil))) (svex-env-compat-union (cdr x) (if look y (hons-acons var val y))))))
Theorem:
(defthm svex-env-p-of-svex-env-compat-union.union (b* (((mv ?err set::?union) (svex-env-compat-union x y))) (svex-env-p union)) :rule-classes :rewrite)
Theorem:
(defthm svar-lookup-in-svex-env-fix (equal (svar-lookup k (svex-env-fix env)) (and (svar-lookup k env) (cons (svar-fix k) (4vec-fix (cdr (svar-lookup k env)))))))
Theorem:
(defthm lookup-in-compat-union-2 (b* (((mv err union) (svex-env-compat-union x y))) (implies (and (svar-lookup k (svex-env-fix y)) (not err)) (equal (svar-lookup k union) (svar-lookup k (svex-env-fix y))))))
Theorem:
(defthm lookup-in-compat-union-1 (b* (((mv err union) (svex-env-compat-union x y))) (implies (and (svar-lookup k (svex-env-fix x)) (not err)) (equal (svar-lookup k union) (svar-lookup k (svex-env-fix x))))))
Theorem:
(defthm lookup-in-compat-union-neither (b* (((mv ?err union) (svex-env-compat-union x y))) (implies (and (not (svar-lookup k (svex-env-fix x))) (not (svar-lookup k (svex-env-fix y)))) (equal (svar-lookup k union) nil))))
Theorem:
(defthm compat-union-reduce-to-append (b* (((mv err union) (svex-env-compat-union x y))) (implies (not err) (svex-envs-similar union (append x y)))))
Theorem:
(defthm svex-eval-compat-union-when-vars-in-first (b* (((mv err union) (svex-env-compat-union env env2))) (implies (and (subsetp (svex-vars x) (svar-alist-keys (svex-env-fix env))) (not err)) (equal (svex-eval x union) (svex-eval x env)))))
Theorem:
(defthm svexlist-eval-compat-union-when-vars-in-first (b* (((mv err union) (svex-env-compat-union env env2))) (implies (and (subsetp (svexlist-vars x) (svar-alist-keys (svex-env-fix env))) (not err)) (equal (svexlist-eval x union) (svexlist-eval x env)))))
Theorem:
(defthm svex-alist-eval-compat-union-when-vars-in-first (b* (((mv err union) (svex-env-compat-union env env2))) (implies (and (subsetp (svex-alist-vars x) (svar-alist-keys (svex-env-fix env))) (not err)) (equal (svex-alist-eval x union) (svex-alist-eval x env)))))
Theorem:
(defthm svex-eval-compat-union-when-vars-in-second (b* (((mv err union) (svex-env-compat-union env env2))) (implies (and (subsetp (svex-vars x) (svar-alist-keys (svex-env-fix env2))) (not err)) (equal (svex-eval x union) (svex-eval x env2)))))
Theorem:
(defthm svexlist-eval-compat-union-when-vars-in-second (b* (((mv err union) (svex-env-compat-union env env2))) (implies (and (subsetp (svexlist-vars x) (svar-alist-keys (svex-env-fix env2))) (not err)) (equal (svexlist-eval x union) (svexlist-eval x env2)))))
Theorem:
(defthm svex-alist-eval-compat-union-when-vars-in-second (b* (((mv err union) (svex-env-compat-union env env2))) (implies (and (subsetp (svex-alist-vars x) (svar-alist-keys (svex-env-fix env2))) (not err)) (equal (svex-alist-eval x union) (svex-alist-eval x env2)))))
Theorem:
(defthm alist-keys-of-svex-env-compat-union (b* (((mv err union) (svex-env-compat-union env env2))) (implies (not err) (set-equiv (svar-alist-keys union) (append (svar-alist-keys (svex-env-fix env)) (svar-alist-keys (svex-env-fix env2)))))))
Theorem:
(defthm svex-env-compat-union-of-svex-env-fix-x (equal (svex-env-compat-union (svex-env-fix x) y) (svex-env-compat-union x y)))
Theorem:
(defthm svex-env-compat-union-svex-env-equiv-congruence-on-x (implies (svex-env-equiv x x-equiv) (equal (svex-env-compat-union x y) (svex-env-compat-union x-equiv y))) :rule-classes :congruence)
Theorem:
(defthm svex-env-compat-union-of-svex-env-fix-y (equal (svex-env-compat-union x (svex-env-fix y)) (svex-env-compat-union x y)))
Theorem:
(defthm svex-env-compat-union-svex-env-equiv-congruence-on-y (implies (svex-env-equiv y y-equiv) (equal (svex-env-compat-union x y) (svex-env-compat-union x y-equiv))) :rule-classes :congruence)