		Search-engine friendly clone of the ACL2 documentation.

Bit-blasting

Svexlist-x-out-unused-vars

Signature
(svexlist-x-out-unused-vars x svars do-it) → new-x
Arguments: x — Guard (svexlist-p x).; svars — Guard (svarlist-p svars).
Returns: new-x — Type (svexlist-p new-x).

Definitions and Theorems

Function: svexlist-x-out-unused-vars

(defun svexlist-x-out-unused-vars (x svars do-it)
 (declare (xargs :guard (and (svexlist-p x)
                             (svarlist-p svars))))
 (let ((__function__ 'svexlist-x-out-unused-vars))
  (declare (ignorable __function__))
  (if do-it
   (b*
    ((subst (make-fast-alist (pairlis$ (svarlist-fix svars)
                                       (svarlist-svex-vars svars))))
     (ans (svexlist-fastsubst x subst)))
    (clear-memoize-table 'svex-fastsubst)
    (fast-alist-free subst)
    ans)
   (svexlist-fix x))))

Theorem: svexlist-p-of-svexlist-x-out-unused-vars

(defthm svexlist-p-of-svexlist-x-out-unused-vars
  (b* ((new-x (svexlist-x-out-unused-vars x svars do-it)))
    (svexlist-p new-x))
  :rule-classes :rewrite)

Theorem: svex-alist-eval-of-svarlist-svex-vars

(defthm svex-alist-eval-of-svarlist-svex-vars
  (equal (svex-alist-eval (pairlis$ (svarlist-fix svars)
                                    (svarlist-svex-vars svars))
                          env)
         (svex-env-extract svars env)))

Theorem: svex-eval-of-svex-env-extract-when-intersection-subset

(defthm svex-eval-of-svex-env-extract-when-intersection-subset
  (implies (subsetp (intersection$ (svex-vars x)
                                   (alist-keys (svex-env-fix env)))
                    (svarlist-fix svars))
           (equal (svex-eval x (svex-env-extract svars env))
                  (svex-eval x env))))

Theorem: svexlist-eval-of-svex-env-extract-when-intersection-subset

(defthm svexlist-eval-of-svex-env-extract-when-intersection-subset
  (implies (subsetp (intersection$ (svexlist-vars x)
                                   (alist-keys (svex-env-fix env)))
                    (svarlist-fix svars))
           (equal (svexlist-eval x (svex-env-extract svars env))
                  (svexlist-eval x env))))

Theorem: svex-eval-of-svexlist-x-out-unused-vars

(defthm svex-eval-of-svexlist-x-out-unused-vars
 (b* ((?new-x (svexlist-x-out-unused-vars x svars do-it)))
  (implies
   (double-rewrite
       (subsetp (intersection-equal (svexlist-vars x)
                                    (alist-keys (svex-env-fix env)))
                (svarlist-fix svars)))
   (equal (svexlist-eval new-x env)
          (svexlist-eval x env)))))

Theorem: svex-vars-of-svexlist-x-out-unused-vars

(defthm svex-vars-of-svexlist-x-out-unused-vars
  (b* ((?new-x (svexlist-x-out-unused-vars x svars do-it)))
    (implies (not (member v (svexlist-vars x)))
             (not (member v (svexlist-vars new-x))))))

Theorem: len-of-svexlist-x-out-unused-vars

(defthm len-of-svexlist-x-out-unused-vars
  (b* ((?new-x (svexlist-x-out-unused-vars x svars do-it)))
    (equal (len new-x) (len x))))

Theorem: svexlist-x-out-unused-vars-of-svexlist-fix-x

(defthm svexlist-x-out-unused-vars-of-svexlist-fix-x
  (equal (svexlist-x-out-unused-vars (svexlist-fix x)
                                     svars do-it)
         (svexlist-x-out-unused-vars x svars do-it)))

Theorem: svexlist-x-out-unused-vars-svexlist-equiv-congruence-on-x

(defthm svexlist-x-out-unused-vars-svexlist-equiv-congruence-on-x
  (implies (svexlist-equiv x x-equiv)
           (equal (svexlist-x-out-unused-vars x svars do-it)
                  (svexlist-x-out-unused-vars x-equiv svars do-it)))
  :rule-classes :congruence)

Theorem: svexlist-x-out-unused-vars-of-svarlist-fix-svars

(defthm svexlist-x-out-unused-vars-of-svarlist-fix-svars
  (equal (svexlist-x-out-unused-vars x (svarlist-fix svars)
                                     do-it)
         (svexlist-x-out-unused-vars x svars do-it)))

Theorem: svexlist-x-out-unused-vars-svarlist-equiv-congruence-on-svars

(defthm
      svexlist-x-out-unused-vars-svarlist-equiv-congruence-on-svars
  (implies (svarlist-equiv svars svars-equiv)
           (equal (svexlist-x-out-unused-vars x svars do-it)
                  (svexlist-x-out-unused-vars x svars-equiv do-it)))
  :rule-classes :congruence)