• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
    • Std/lists
    • Std/alists
      • Alist-keys
      • Remove-assocs
      • Alist-vals
      • Alist-map-vals
      • Alist-map-keys
      • Std/alists/strip-cdrs
      • Hons-rassoc-equal
      • Std/alists/hons-assoc-equal
      • Std/alists/strip-cars
      • Fal-find-any
      • Fal-extract
      • Std/alists/abstract
      • Fal-extract-vals
      • Fal-all-boundp
      • Std/alists/alistp
      • Append-alist-vals
      • Append-alist-keys
      • Alist-equiv
      • Hons-remove-assoc
      • Std/alists/pairlis$
      • Worth-hashing
      • Alists-agree
      • 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-rassoc-equal

(hons-rassoc-equal val alist) returns the first pair found in the alist alist whose value is val, if one exists, or nil otherwise.

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

Definitions and Theorems

Function: hons-rassoc-equal

(defun hons-rassoc-equal (val alist)
  (declare (xargs :guard t))
  (cond ((atom alist) nil)
        ((and (consp (car alist))
              (equal val (cdar alist)))
         (car alist))
        (t (hons-rassoc-equal val (cdr alist)))))

Theorem: hons-rassoc-equal-when-atom

(defthm hons-rassoc-equal-when-atom
  (implies (atom alist)
           (equal (hons-rassoc-equal val alist)
                  nil)))

Theorem: hons-rassoc-equal-of-hons-acons

(defthm hons-rassoc-equal-of-hons-acons
  (equal (hons-rassoc-equal a (cons (cons key b) alist))
         (if (equal a b)
             (cons key b)
           (hons-rassoc-equal a alist))))

Theorem: hons-rassoc-equal-type

(defthm hons-rassoc-equal-type
  (or (not (hons-rassoc-equal val alist))
      (consp (hons-rassoc-equal val alist)))
  :rule-classes :type-prescription)

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

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

Theorem: consp-of-hons-rassoc-equal

(defthm consp-of-hons-rassoc-equal
  (equal (consp (hons-rassoc-equal val alist))
         (if (hons-rassoc-equal val alist)
             t
           nil)))

Theorem: cdr-of-hons-rassoc-equal

(defthm cdr-of-hons-rassoc-equal
  (equal (cdr (hons-rassoc-equal val alist))
         (if (hons-rassoc-equal val alist)
             val
           nil)))

Theorem: member-equal-of-alist-vals-under-iff

(defthm member-equal-of-alist-vals-under-iff
  (iff (member-equal val (alist-vals alist))
       (hons-rassoc-equal val alist)))

Theorem: hons-assoc-equal-of-car-when-hons-rassoc-equal

(defthm hons-assoc-equal-of-car-when-hons-rassoc-equal
  (implies (hons-rassoc-equal val alist)
           (hons-assoc-equal (car (hons-rassoc-equal val alist))
                             alist)))

Theorem: hons-assoc-equal-of-car-when-hons-rassoc-equal-and-no-duplicates

(defthm
   hons-assoc-equal-of-car-when-hons-rassoc-equal-and-no-duplicates
  (implies
       (and (no-duplicatesp-equal (alist-keys alist))
            (hons-rassoc-equal val alist))
       (equal (hons-assoc-equal (car (hons-rassoc-equal val alist))
                                alist)
              (hons-rassoc-equal val alist))))

Theorem: member-equal-of-car-when-hons-rassoc-equal

(defthm member-equal-of-car-when-hons-rassoc-equal
  (implies (hons-rassoc-equal val alist)
           (member-equal (car (hons-rassoc-equal val alist))
                         (alist-keys alist))))

Theorem: hons-rassoc-equal-of-cdr-when-hons-assoc-equal

(defthm hons-rassoc-equal-of-cdr-when-hons-assoc-equal
  (implies (hons-assoc-equal key alist)
           (hons-rassoc-equal (cdr (hons-assoc-equal key alist))
                              alist)))

Theorem: hons-rassoc-equal-of-cdr-when-hons-assoc-equal-and-no-duplicates

(defthm
   hons-rassoc-equal-of-cdr-when-hons-assoc-equal-and-no-duplicates
  (implies
       (and (no-duplicatesp-equal (alist-vals alist))
            (hons-assoc-equal key alist))
       (equal (hons-rassoc-equal (cdr (hons-assoc-equal key alist))
                                 alist)
              (hons-assoc-equal key alist))))