		Search-engine friendly clone of the ACL2 documentation.

Decomp.lisp

Envmap-entry-to-term-alist

Signature
(envmap-entry-to-term-alist x env) → xal
Arguments: x — Guard (svex-alist-p x).; env — Guard (pseudo-termp env).
Returns: xal — Type (and (implies (pseudo-termp env) (svdecomp-symenv-p xal)) (svar-alist-p xal)) .

Definitions and Theorems

Function: envmap-entry-to-term-alist

(defun envmap-entry-to-term-alist (x env)
  (declare (xargs :guard (and (svex-alist-p x)
                              (pseudo-termp env))))
  (let ((__function__ 'envmap-entry-to-term-alist))
    (declare (ignorable __function__))
    (b* (((when (atom x)) nil)
         ((unless (mbt (and (consp (car x))
                            (svar-p (caar x)))))
          (envmap-entry-to-term-alist (cdr x)
                                      env)))
      (cons (cons (caar x)
                  (cons 'svex-eval
                        (cons (cons 'quote
                                    (cons (svex-fix (cdar x)) 'nil))
                              (cons env 'nil))))
            (envmap-entry-to-term-alist (cdr x)
                                        env)))))

Theorem: return-type-of-envmap-entry-to-term-alist

(defthm return-type-of-envmap-entry-to-term-alist
  (b* ((xal (envmap-entry-to-term-alist x env)))
    (and (implies (pseudo-termp env)
                  (svdecomp-symenv-p xal))
         (svar-alist-p xal)))
  :rule-classes :rewrite)

Theorem: eval-of-envmap-entry-to-term-alist

(defthm eval-of-envmap-entry-to-term-alist
  (equal (svdecomp-ev-symenv (envmap-entry-to-term-alist x env)
                             a)
         (svex-alist-eval x (svdecomp-ev env a))))

Theorem: lookup-in-envmap-entry-to-term-alist

(defthm lookup-in-envmap-entry-to-term-alist
  (iff (svar-lookup k (envmap-entry-to-term-alist x env))
       (svar-lookup k x)))

Theorem: no-lookup-when-not-in-svex-alist-fix

(defthm no-lookup-when-not-in-svex-alist-fix
 (implies (not (svar-lookup k x))
          (not (svar-lookup k (envmap-entry-to-term-alist x env)))))

Theorem: envmap-entry-to-term-alist-of-svex-alist-fix-x

(defthm envmap-entry-to-term-alist-of-svex-alist-fix-x
  (equal (envmap-entry-to-term-alist (svex-alist-fix x)
                                     env)
         (envmap-entry-to-term-alist x env)))

Theorem: envmap-entry-to-term-alist-svex-alist-equiv-congruence-on-x

(defthm envmap-entry-to-term-alist-svex-alist-equiv-congruence-on-x
  (implies (svex-alist-equiv x x-equiv)
           (equal (envmap-entry-to-term-alist x env)
                  (envmap-entry-to-term-alist x-equiv env)))
  :rule-classes :congruence)