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