		Search-engine friendly clone of the ACL2 documentation.

Alist-vals

(alist-vals x) collects all values bound in an alist.

This is a "modern" equivalent of strip-cdrs, which properly respects the non-alist convention; see std/alists for discussion of this convention.

Note that the list of values returned by alist-vals may include "shadowed" bindings, as in ((a . 1) (a . 2)).

Definitions and Theorems

Function: alist-vals

(defun alist-vals (x)
       (declare (xargs :guard t))
       (cond ((atom x) nil)
             ((atom (car x)) (alist-vals (cdr x)))
             (t (cons (cdar x) (alist-vals (cdr x))))))

Theorem: alist-vals-when-atom

(defthm alist-vals-when-atom
        (implies (atom x)
                 (equal (alist-vals x) nil)))

Theorem: alist-vals-of-cons

(defthm alist-vals-of-cons
        (equal (alist-vals (cons a x))
               (if (consp a)
                   (cons (cdr a) (alist-vals x))
                   (alist-vals x))))

Theorem: list-equiv-implies-equal-alist-vals-1

(defthm list-equiv-implies-equal-alist-vals-1
        (implies (list-equiv x x-equiv)
                 (equal (alist-vals x)
                        (alist-vals x-equiv)))
        :rule-classes (:congruence))

Theorem: true-listp-of-alist-vals

(defthm true-listp-of-alist-vals
        (true-listp (alist-vals x))
        :rule-classes :type-prescription)

Theorem: alist-vals-of-hons-acons

(defthm alist-vals-of-hons-acons
        (equal (alist-vals (hons-acons key val x))
               (cons val (alist-vals x))))

Theorem: alist-vals-of-pairlis$

(defthm alist-vals-of-pairlis$
        (implies (equal (len keys) (len vals))
                 (equal (alist-vals (pairlis$ keys vals))
                        (list-fix vals))))

Theorem: len-of-alist-vals

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

Theorem: alist-vals-of-append

(defthm alist-vals-of-append
        (equal (alist-vals (append x y))
               (append (alist-vals x) (alist-vals y))))

Theorem: alist-vals-of-revappend

(defthm alist-vals-of-revappend
        (equal (alist-vals (revappend x y))
               (revappend (alist-vals x)
                          (alist-vals y))))

Theorem: member-equal-of-cdr-when-hons-assoc-equal

(defthm member-equal-of-cdr-when-hons-assoc-equal
        (implies (hons-assoc-equal key map)
                 (member-equal (cdr (hons-assoc-equal key map))
                               (alist-vals map))))