		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))))