		Search-engine friendly clone of the ACL2 documentation.

Rewriting

Svex-alist-subst

Signature
(svex-alist-subst x a) → xx
Arguments: x — Guard (svex-alist-p x).; a — Guard (svex-alist-p a).
Returns: xx — Type (svex-alist-p xx).

Definitions and Theorems

Function: svex-alist-subst

(defun svex-alist-subst (x a)
  (declare (xargs :guard (and (svex-alist-p x)
                              (svex-alist-p a))))
  (let ((__function__ 'svex-alist-subst))
    (declare (ignorable __function__))
    (if (atom x)
        nil
      (mbe :logic
           (if (mbt (and (consp (car x)) (svar-p (caar x))))
               (svex-acons (caar x)
                           (svex-subst (cdar x) a)
                           (svex-alist-subst (cdr x) a))
             (svex-alist-subst (cdr x) a))
           :exec (acl2::with-local-nrev
                      (svex-alist-subst-nrev x a acl2::nrev))))))

Theorem: svex-alist-p-of-svex-alist-subst

(defthm svex-alist-p-of-svex-alist-subst
  (b* ((xx (svex-alist-subst x a)))
    (svex-alist-p xx))
  :rule-classes :rewrite)

Theorem: svex-alist-subst-of-svex-alist-fix-x

(defthm svex-alist-subst-of-svex-alist-fix-x
  (equal (svex-alist-subst (svex-alist-fix x) a)
         (svex-alist-subst x a)))

Theorem: svex-alist-subst-svex-alist-equiv-congruence-on-x

(defthm svex-alist-subst-svex-alist-equiv-congruence-on-x
  (implies (svex-alist-equiv x x-equiv)
           (equal (svex-alist-subst x a)
                  (svex-alist-subst x-equiv a)))
  :rule-classes :congruence)

Theorem: svex-alist-subst-of-svex-alist-fix-a

(defthm svex-alist-subst-of-svex-alist-fix-a
  (equal (svex-alist-subst x (svex-alist-fix a))
         (svex-alist-subst x a)))

Theorem: svex-alist-subst-svex-alist-equiv-congruence-on-a

(defthm svex-alist-subst-svex-alist-equiv-congruence-on-a
  (implies (svex-alist-equiv a a-equiv)
           (equal (svex-alist-subst x a)
                  (svex-alist-subst x a-equiv)))
  :rule-classes :congruence)

Theorem: svex-alist-eval-of-svex-subst

(defthm svex-alist-eval-of-svex-subst
  (equal (svex-alist-eval (svex-alist-subst x subst)
                          env)
         (svex-alist-eval x (svex-alist-eval subst env))))

Theorem: vars-of-svex-alist-subst

(defthm vars-of-svex-alist-subst
  (implies (and (not (member v (svex-alist-vars x)))
                (not (member v (svex-alist-vars a))))
           (not (member v
                        (svex-alist-vars (svex-alist-subst x a))))))

Theorem: svex-lookup-of-svex-alist-subst

(defthm svex-lookup-of-svex-alist-subst
  (iff (svex-lookup v (svex-alist-subst x a))
       (svex-lookup v x)))