		Search-engine friendly clone of the ACL2 documentation.

Std/alists

Fal-find-any

Find the first of many keys bound in a fast alist.

Signature
(fal-find-any keys alist) → ans
Arguments: keys — List of keys to look for.; alist — Fast alist to search.
Returns: ans — A (key . value) pair on success, or nil on failure.

We walk over each key in keys. As soon as we find a key that is bound in alist, we return its value. If none of the keys are bound in alist, we return nil.

Definitions and Theorems

Function: fal-find-any

(defun fal-find-any (keys alist)
  (declare (xargs :guard t))
  (let ((__function__ 'fal-find-any))
    (declare (ignorable __function__))
    (if (atom keys)
        nil
      (or (hons-get (car keys) alist)
          (fal-find-any (cdr keys) alist)))))

Theorem: fal-find-any-when-atom

(defthm fal-find-any-when-atom
  (implies (atom keys)
           (equal (fal-find-any keys alist) nil)))

Theorem: fal-find-any-when-empty-alist

(defthm fal-find-any-when-empty-alist
  (implies (atom alist)
           (not (fal-find-any keys alist))))

Theorem: fal-find-any-of-cons

(defthm fal-find-any-of-cons
  (equal (fal-find-any (cons key keys) alist)
         (or (hons-get key alist)
             (fal-find-any keys alist))))

Theorem: type-of-fal-find-any

(defthm type-of-fal-find-any
  (or (not (fal-find-any keys alist))
      (consp (fal-find-any keys alist)))
  :rule-classes :type-prescription)

Theorem: consp-of-fal-find-any

(defthm consp-of-fal-find-any
  (iff (consp (fal-find-any keys alist))
       (fal-find-any keys alist)))

Theorem: fal-find-any-of-list-fix-keys

(defthm fal-find-any-of-list-fix-keys
  (equal (fal-find-any (list-fix keys) alist)
         (fal-find-any keys alist)))

Theorem: list-equiv-implies-equal-fal-find-any-1

(defthm list-equiv-implies-equal-fal-find-any-1
  (implies (list-equiv keys keys-equiv)
           (equal (fal-find-any keys alist)
                  (fal-find-any keys-equiv alist)))
  :rule-classes (:congruence))

Theorem: alist-equiv-implies-equal-fal-find-any-2

(defthm alist-equiv-implies-equal-fal-find-any-2
  (implies (alist-equiv alist alist-equiv)
           (equal (fal-find-any keys alist)
                  (fal-find-any keys alist-equiv)))
  :rule-classes (:congruence))

Theorem: fal-find-any-of-append

(defthm fal-find-any-of-append
  (equal (fal-find-any (append x y) alist)
         (or (fal-find-any x alist)
             (fal-find-any y alist))))

Theorem: fal-find-any-under-iff

(defthm fal-find-any-under-iff
  (iff (fal-find-any keys alist)
       (intersectp-equal keys (alist-keys alist))))

Theorem: set-equiv-implies-iff-fal-find-any-1

(defthm set-equiv-implies-iff-fal-find-any-1
  (implies (set-equiv keys keys-equiv)
           (iff (fal-find-any keys alist)
                (fal-find-any keys-equiv alist)))
  :rule-classes (:congruence))

Theorem: hons-assoc-equal-when-found-by-fal-find-any

(defthm hons-assoc-equal-when-found-by-fal-find-any
  (implies (and (equal (fal-find-any keys alist) ans)
                ans)
           (equal (hons-assoc-equal (car ans) alist)
                  ans)))