		Search-engine friendly clone of the ACL2 documentation.

Decomp.lisp

Svex-alist-evaluation-to-symenv

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

Definitions and Theorems

Function: svex-alist-evaluation-to-symenv

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

Theorem: return-type-of-svex-alist-evaluation-to-symenv

(defthm return-type-of-svex-alist-evaluation-to-symenv
  (b* ((al (svex-alist-evaluation-to-symenv x env)))
    (and (svar-alist-p al)
         (implies (pseudo-termp env)
                  (svdecomp-symenv-p al))))
  :rule-classes :rewrite)

Theorem: eval-lookup-of-svex-alist-evaluation-to-symenv

(defthm eval-lookup-of-svex-alist-evaluation-to-symenv
  (b* ((al (svex-alist-evaluation-to-symenv x env)))
    (equal (svdecomp-ev (cdr (svar-lookup k al)) a)
           (and (svar-lookup k x)
                (svex-eval (cdr (svar-lookup k x))
                           (svdecomp-ev env a))))))

Theorem: lookup-exists-of-svex-alist-evaluation-to-symenv

(defthm lookup-exists-of-svex-alist-evaluation-to-symenv
  (b* ((al (svex-alist-evaluation-to-symenv x env)))
    (iff (svar-lookup k al)
         (svar-lookup k x))))

Theorem: svdecomp-ev-symenv-of-svex-alist-evaluation-to-symenv

(defthm svdecomp-ev-symenv-of-svex-alist-evaluation-to-symenv
  (b* ((al (svex-alist-evaluation-to-symenv x env)))
    (equal (svdecomp-ev-symenv al a)
           (svex-alist-eval x (svdecomp-ev env a)))))

Theorem: svex-alist-evaluation-to-symenv-of-svex-alist-fix-x

(defthm svex-alist-evaluation-to-symenv-of-svex-alist-fix-x
  (equal (svex-alist-evaluation-to-symenv (svex-alist-fix x)
                                          env)
         (svex-alist-evaluation-to-symenv x env)))

Theorem: svex-alist-evaluation-to-symenv-svex-alist-equiv-congruence-on-x

(defthm
   svex-alist-evaluation-to-symenv-svex-alist-equiv-congruence-on-x
  (implies (svex-alist-equiv x x-equiv)
           (equal (svex-alist-evaluation-to-symenv x env)
                  (svex-alist-evaluation-to-symenv x-equiv env)))
  :rule-classes :congruence)