		Search-engine friendly clone of the ACL2 documentation.

Std/alists

Fal-extract

(fal-extract keys al) extracts a "subset" of the alist al by binding every key in keys to its value in al, skipping any 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-extract1

(defun fal-extract1 (keys al)
       "Assumes AL is fast"
       (declare (xargs :guard t))
       (b* (((when (atom keys)) nil)
            (look (hons-get (car keys) al))
            ((when look)
             (cons look (fal-extract1 (cdr keys) al))))
           (fal-extract1 (cdr keys) al)))

Function: fal-extract

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

Theorem: fal-extract1-removal

(defthm fal-extract1-removal
        (equal (fal-extract1 keys al)
               (fal-extract keys al)))

Theorem: fal-extract-when-atom

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

Theorem: fal-extract-of-cons

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

Theorem: alistp-of-fal-extract

(defthm alistp-of-fal-extract
        (alistp (fal-extract keys al)))

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

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

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

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

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

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

Theorem: fal-extract-of-append

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

Theorem: fal-extract-of-rev

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

Theorem: fal-extract-of-revappend

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

Theorem: len-of-fal-extract

(defthm len-of-fal-extract
        (<= (len (fal-extract x al)) (len x))
        :rule-classes ((:rewrite) (:linear)))

Theorem: hons-assoc-equal-fal-extract

(defthm hons-assoc-equal-fal-extract
        (equal (hons-assoc-equal x (fal-extract keys al))
               (and (member-equal x keys)
                    (hons-assoc-equal x al))))