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