		Search-engine friendly clone of the ACL2 documentation.

Std/alists

Append-alist-vals

(append-alist-vals x) appends all of the values from the alist x into a single list.

Our guard is merely t, but typically x should be an alist of (key . value) pairs where every value is a list of elements. We walk through the alist, appending together all of the elements of each value into a single, flat list.

Note that we do not really treat x as an association list. That is, we will include the values from any "shadowed pairs" in the list.

Definitions and Theorems

Function: append-alist-vals

(defun append-alist-vals (x)
  (declare (xargs :guard t))
  (mbe :logic
       (if (atom x)
           nil
         (append (cdar x)
                 (append-alist-vals (cdr x))))
       :exec (reverse (append-alist-vals-exec x nil))))

Theorem: append-alist-vals-exec-removal

(defthm append-alist-vals-exec-removal
  (equal (append-alist-vals-exec x acc)
         (revappend (append-alist-vals x) acc)))

Theorem: append-alist-vals-when-atom

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

Theorem: append-alist-vals-of-cons

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

Theorem: true-listp-of-append-alist-vals

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

Theorem: append-alist-vals-of-append

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

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

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

Subtopics

Append-alist-vals-exec: Tail-recursive implementation of append-alist-vals.