		Search-engine friendly clone of the ACL2 documentation.

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