		Search-engine friendly clone of the ACL2 documentation.

Std/alists

Fal-extract-vals

(fal-extract keys al) extracts the values associated with the given keys in the alist al. For unbound keys, we arbitrarily assign the value nil.

This is similar to fal-extract except that we only return the values instead of a sub-alist, and we don't skip unbound keys.

This is a "modern" alist function that respects the non-alist convention; see std/alists for discussion of this convention.

This function is optimized for fast-alists. Ordinary alists will be temporarily made fast.

Definitions and Theorems

Function: fal-extract-vals1

(defun fal-extract-vals1 (keys al)
  "Assumes AL is fast"
  (declare (xargs :guard t))
  (if (atom keys)
      nil
    (cons (cdr (hons-get (car keys) al))
          (fal-extract-vals1 (cdr keys) al))))

Function: fal-extract-vals

(defun fal-extract-vals (keys al)
  "Makes AL fast if necessary"
  (declare (xargs :guard t))
  (mbe :logic
       (if (atom keys)
           nil
         (cons (cdr (hons-get (car keys) al))
               (fal-extract-vals (cdr keys) al)))
       :exec (with-fast-alist al (fal-extract-vals1 keys al))))

Theorem: fal-extract-vals1-removal

(defthm fal-extract-vals1-removal
  (equal (fal-extract-vals1 keys al)
         (fal-extract-vals keys al)))

Theorem: fal-extract-vals-when-atom

(defthm fal-extract-vals-when-atom
  (implies (atom keys)
           (equal (fal-extract-vals keys al) nil)))

Theorem: fal-extract-vals-of-cons

(defthm fal-extract-vals-of-cons
  (equal (fal-extract-vals (cons a keys) al)
         (cons (cdr (hons-get a al))
               (fal-extract-vals keys al))))

Theorem: fal-extract-vals-of-list-fix

(defthm fal-extract-vals-of-list-fix
  (equal (fal-extract-vals (list-fix keys) al)
         (fal-extract-vals keys al)))

Theorem: list-equiv-implies-equal-fal-extract-vals-1

(defthm list-equiv-implies-equal-fal-extract-vals-1
  (implies (list-equiv keys keys-equiv)
           (equal (fal-extract-vals keys al)
                  (fal-extract-vals keys-equiv al)))
  :rule-classes (:congruence))

Theorem: alist-equiv-implies-equal-fal-extract-vals-2

(defthm alist-equiv-implies-equal-fal-extract-vals-2
  (implies (alist-equiv al al-equiv)
           (equal (fal-extract-vals keys al)
                  (fal-extract-vals keys al-equiv)))
  :rule-classes (:congruence))

Theorem: fal-extract-vals-of-append

(defthm fal-extract-vals-of-append
  (equal (fal-extract-vals (append x y) al)
         (append (fal-extract-vals x al)
                 (fal-extract-vals y al))))

Theorem: fal-extract-vals-of-rev

(defthm fal-extract-vals-of-rev
  (equal (fal-extract-vals (rev x) al)
         (rev (fal-extract-vals x al))))

Theorem: fal-extract-vals-of-revappend

(defthm fal-extract-vals-of-revappend
  (equal (fal-extract-vals (revappend x y) al)
         (revappend (fal-extract-vals x al)
                    (fal-extract-vals y al))))

Theorem: len-of-fal-extract-vals

(defthm len-of-fal-extract-vals
  (equal (len (fal-extract-vals x al))
         (len x)))