alist-vals

(in-package "ACL2")

(defsection alist-vals
  :parents (std/alists strip-cdrs)
  :short "@(call alist-vals) collects all values bound in an alist."
  :long "<p>This is a "modern" equivalent of @(see strip-cdrs), which
properly respects the non-alist convention; see @(see std/alists) for
discussion of this convention.</p>

<p>Note that the list of values returned by @('alist-vals') may include
"shadowed" bindings, as in @('((a . 1) (a . 2))').</p>"
  (defund 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))))))
  (local (in-theory (enable alist-vals)))
  (defthm alist-vals-when-atom
    (implies (atom x) (equal (alist-vals x) nil)))
  (defthm alist-vals-of-cons
    (equal (alist-vals (cons a x))
      (if (consp a)
        (cons (cdr a) (alist-vals x))
        (alist-vals x))))
  (encapsulate nil
    (local (defthmd l0
        (equal (alist-vals (list-fix x)) (alist-vals x))
        :hints (("Goal" :in-theory (enable list-fix)))))
    (defcong list-equiv
      equal
      (alist-vals x)
      1
      :hints (("Goal" :in-theory (enable list-equiv)
         :use ((:instance l0 (x x)) (:instance l0 (x x-equiv)))))))
  (defthm true-listp-of-alist-vals
    (true-listp (alist-vals x))
    :rule-classes :type-prescription)
  (defthm alist-vals-of-hons-acons
    (equal (alist-vals (hons-acons key val x))
      (cons val (alist-vals x))))
  (defthm alist-vals-of-pairlis$
    (implies (equal (len keys) (len vals))
      (equal (alist-vals (pairlis$ keys vals)) (list-fix vals)))
    :hints (("Goal" :in-theory (enable list-fix))))
  (defthm len-of-alist-vals
    (equal (len (alist-vals x)) (len (alist-keys x)))
    :hints (("Goal" :in-theory (enable alist-keys alist-vals))))
  (defthm alist-vals-of-append
    (equal (alist-vals (append x y))
      (append (alist-vals x) (alist-vals y))))
  (defthm alist-vals-of-revappend
    (equal (alist-vals (revappend x y))
      (revappend (alist-vals x) (alist-vals y))))
  (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)))))