		Search-engine friendly clone of the ACL2 documentation.

Svex-alist

Svex-alist-vals

Like alist-vals but with proper fty-discipline for svex-alists.

Signature
(svex-alist-vals x) → vals
Arguments: x — Guard (svex-alist-p x).
Returns: vals — Type (svexlist-p vals).

Definitions and Theorems

Function: svex-alist-vals

(defun svex-alist-vals (x)
  (declare (xargs :guard (svex-alist-p x)))
  (let ((__function__ 'svex-alist-vals))
    (declare (ignorable __function__))
    (mbe :logic
         (if (atom x)
             nil
           (if (mbt (and (consp (car x)) (svar-p (caar x))))
               (cons (mbe :logic (svex-fix (cdar x))
                          :exec (cdar x))
                     (svex-alist-vals (cdr x)))
             (svex-alist-vals (cdr x))))
         :exec (strip-cdrs x))))

Theorem: svexlist-p-of-svex-alist-vals

(defthm svexlist-p-of-svex-alist-vals
  (b* ((vals (svex-alist-vals x)))
    (svexlist-p vals))
  :rule-classes :rewrite)

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

(defthm svex-alist-vals-of-svex-alist-fix-x
  (equal (svex-alist-vals (svex-alist-fix x))
         (svex-alist-vals x)))

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

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

Theorem: member-svex-alist-vals-when-svex-lookup

(defthm member-svex-alist-vals-when-svex-lookup
  (implies (svex-lookup k x)
           (member (svex-lookup k x)
                   (svex-alist-vals x))))

Theorem: svex-alist-vals-of-svex-acons

(defthm svex-alist-vals-of-svex-acons
  (equal (svex-alist-vals (svex-acons k v x))
         (cons (svex-fix v)
               (svex-alist-vals x))))

Theorem: len-of-svex-alist-vals

(defthm len-of-svex-alist-vals
  (equal (len (svex-alist-vals x))
         (len (svex-alist-keys x))))

Theorem: svex-alist-vals-of-pairlis$

(defthm svex-alist-vals-of-pairlis$
  (implies (and (equal (len x) (len y))
                (svarlist-p x))
           (equal (svex-alist-vals (pairlis$ x y))
                  (svexlist-fix y))))