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