• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
    • Std/lists
    • Std/alists
      • Alist-keys
      • Remove-assocs
      • Alist-vals
      • Alist-map-vals
      • Std/alists/strip-cdrs
      • Hons-rassoc-equal
      • Alist-map-keys
      • Std/alists/hons-assoc-equal
      • Fal-extract
      • Std/alists/strip-cars
      • Fal-find-any
      • Fal-extract-vals
      • Std/alists/abstract
      • Fal-all-boundp
      • Std/alists/alistp
      • Append-alist-vals
      • Append-alist-keys
      • Alist-equiv
      • Hons-remove-assoc
      • Std/alists/pairlis$
      • Alists-agree
      • Worth-hashing
      • Sub-alistp
      • Alist-fix
      • Std/alists/remove-assoc-equal
      • Std/alists/assoc-equal
    • Obags
    • Std/util
    • Std/strings
    • Std/io
    • Std/osets
    • Std/system
    • Std/basic
    • Std/typed-lists
    • Std/bitsets
    • Std/testing
    • Std/typed-alists
    • Std/stobjs
    • Std-extensions
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Testing-utilities
  • Math

• Std/alists
• Hons-assoc-equal
• Hons-get

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))))