		Search-engine friendly clone of the ACL2 documentation.

Std/alists/hons-assoc-equal

Lemmas about hons-assoc-equal available in the std/alists library.

NOTE: It is a good idea to be very clear on the relationship between hons-get and hons-assoc-equal:

To get hash table speeds out of fast-alists during execution, you must write your functions in terms of hons-get instead of hons-assoc-equal! But,
You should never write theorems about hons-get! It just rewrites into hons-assoc-equal. We always reason in terms of hons-assoc-equal, which is useful, e.g., to avoid spurious slow-alist-warnings during proofs.

hons-assoc-equal is the "modern" alternative to assoc, and properly respect the non-alist convention; see std/alists for discussion of this convention.

Definitions and Theorems

Theorem: hons-assoc-equal-when-atom

(defthm hons-assoc-equal-when-atom
  (implies (atom alist)
           (equal (hons-assoc-equal a alist) nil)))

Theorem: hons-assoc-equal-of-cons

(defthm hons-assoc-equal-of-cons
  (equal (hons-assoc-equal key (cons entry map))
         (if (and (consp entry)
                  (equal key (car entry)))
             entry
           (hons-assoc-equal key map))))

Theorem: list-equiv-implies-equal-hons-assoc-equal-2

(defthm list-equiv-implies-equal-hons-assoc-equal-2
  (implies (list-equiv alist alist-equiv)
           (equal (hons-assoc-equal key alist)
                  (hons-assoc-equal key alist-equiv)))
  :rule-classes (:congruence))

Theorem: hons-assoc-equal-of-hons-acons

(defthm hons-assoc-equal-of-hons-acons
  (equal (hons-assoc-equal key (hons-acons key2 val map))
         (if (equal key key2)
             (cons key val)
           (hons-assoc-equal key map))))

Theorem: consp-of-hons-assoc-equal

(defthm consp-of-hons-assoc-equal
  (equal (consp (hons-assoc-equal x alist))
         (if (hons-assoc-equal x alist) t nil)))

Theorem: car-hons-assoc-equal

(defthm car-hons-assoc-equal
  (implies (hons-assoc-equal k a)
           (equal (car (hons-assoc-equal k a)) k)))

Theorem: car-hons-assoc-equal-split

(defthm car-hons-assoc-equal-split
  (equal (car (hons-assoc-equal key alist))
         (if (hons-assoc-equal key alist)
             key
           nil)))

Theorem: hons-assoc-equal-append

(defthm hons-assoc-equal-append
  (equal (hons-assoc-equal x (append a b))
         (or (hons-assoc-equal x a)
             (hons-assoc-equal x b))))

Theorem: hons-assoc-equal-of-hons-shrink-alist

(defthm hons-assoc-equal-of-hons-shrink-alist
  (equal (hons-assoc-equal a (hons-shrink-alist x y))
         (or (hons-assoc-equal a y)
             (hons-assoc-equal a x))))

Theorem: cons-key-cdr-hons-assoc-equal

(defthm cons-key-cdr-hons-assoc-equal
  (implies (hons-assoc-equal k a)
           (equal (cons k (cdr (hons-assoc-equal k a)))
                  (hons-assoc-equal k a))))