		Search-engine friendly clone of the ACL2 documentation.

Alist-keys

(alist-keys x) collects all keys bound in an alist.

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

Note that the list of keys returned by alist-keys may contain duplicates. This happens whenever the input alist contains "shadowed" bindings, as in ((a . 1) (a . 2)).

Note about Normal Forms

A key is a among the alist-keys of an alist exactly when hons-assoc-equal is non-nil. We generally prefer hons-assoc-equal as the normal form, so the following rule is enabled by default::

Theorem: alist-keys-member-hons-assoc-equal

(defthm alist-keys-member-hons-assoc-equal
  (iff (member-equal x (alist-keys a))
       (hons-assoc-equal x a)))

However, sometimes the member-based normal form works better when you want to tie into powerful set-reasoning strategies. To support this, the following rule is available but is disabled by default:

Theorem: hons-assoc-equal-iff-member-alist-keys

(defthm hons-assoc-equal-iff-member-alist-keys
  (iff (hons-assoc-equal x a)
       (member-equal x (alist-keys a))))

Obviously these two rules loop, so a theory-invariant insists that you choose one or the other. For greater compatibility between books, please do not non-locally switch the normal form.

Definitions and Theorems

Function: alist-keys

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

Theorem: alist-keys-when-atom

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

Theorem: alist-keys-of-cons

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

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

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

Theorem: true-listp-of-alist-keys

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

Theorem: alist-keys-of-hons-acons

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

Theorem: alist-keys-of-pairlis$

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

Theorem: alist-keys-member-hons-assoc-equal

(defthm alist-keys-member-hons-assoc-equal
  (iff (member-equal x (alist-keys a))
       (hons-assoc-equal x a)))

Theorem: hons-assoc-equal-iff-member-alist-keys

(defthm hons-assoc-equal-iff-member-alist-keys
  (iff (hons-assoc-equal x a)
       (member-equal x (alist-keys a))))

Theorem: hons-assoc-equal-when-not-member-alist-keys

(defthm hons-assoc-equal-when-not-member-alist-keys
  (implies (not (member-equal x (alist-keys a)))
           (equal (hons-assoc-equal x a) nil)))

Theorem: alist-keys-of-append

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

Theorem: alist-keys-of-rev

(defthm alist-keys-of-rev
  (equal (alist-keys (rev x))
         (rev (alist-keys x))))

Theorem: alist-keys-of-revappend

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