		Search-engine friendly clone of the ACL2 documentation.

Std/alists

Append-alist-keys

(append-alist-keys 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-keys

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

Theorem: append-alist-keys-exec-removal

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

Theorem: append-alist-keys-when-atom

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

Theorem: append-alist-keys-of-cons

(defthm append-alist-keys-of-cons
  (equal (append-alist-keys (cons a x))
         (append (car a) (append-alist-keys x))))

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

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

Theorem: append-alist-keys-of-append

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

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

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

Subtopics

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