		Search-engine friendly clone of the ACL2 documentation.

Std/alists

Fal-all-boundp

(fal-all-boundp keys alist) determines if every key in keys is bound in the alist alist.

Signature
(fal-all-boundp keys alist) → bool

The alist need not be fast. If it is not fast, it may be made temporarily fast, depending on its length.

Definitions and Theorems

Function: fal-all-boundp

(defun fal-all-boundp (keys alist)
 (declare (xargs :guard t))
 (let ((__function__ 'fal-all-boundp))
  (declare (ignorable __function__))
  (mbe
      :logic
      (if (atom keys)
          t
        (and (hons-assoc-equal (car keys) alist)
             (fal-all-boundp (cdr keys) alist)))
      :exec
      (if (atom keys)
          t
        (if (and (worth-hashing keys)
                 (worth-hashing alist))
            (with-fast-alist alist (fal-all-boundp-fast keys alist))
          (fal-all-boundp-slow keys alist))))))

Theorem: fal-all-boundp-fast-removal

(defthm fal-all-boundp-fast-removal
  (equal (fal-all-boundp-fast keys alist)
         (fal-all-boundp keys alist)))

Theorem: fal-all-boundp-slow-removal

(defthm fal-all-boundp-slow-removal
  (equal (fal-all-boundp-slow keys alist)
         (fal-all-boundp keys alist)))

Theorem: fal-all-boundp-when-atom

(defthm fal-all-boundp-when-atom
  (implies (atom keys)
           (equal (fal-all-boundp keys alist) t)))

Theorem: fal-all-boundp-of-cons

(defthm fal-all-boundp-of-cons
  (equal (fal-all-boundp (cons a keys) alist)
         (and (hons-get a alist)
              (fal-all-boundp keys alist))))

Theorem: set-equiv-implies-equal-fal-all-boundp-1

(defthm set-equiv-implies-equal-fal-all-boundp-1
  (implies (set-equiv x x-equiv)
           (equal (fal-all-boundp x alist)
                  (fal-all-boundp x-equiv alist)))
  :rule-classes (:congruence))

Theorem: alist-equiv-implies-equal-fal-all-boundp-2

(defthm alist-equiv-implies-equal-fal-all-boundp-2
  (implies (alist-equiv alist alist-equiv)
           (equal (fal-all-boundp x alist)
                  (fal-all-boundp x alist-equiv)))
  :rule-classes (:congruence))

Theorem: fal-all-boundp-of-list-fix

(defthm fal-all-boundp-of-list-fix
  (equal (fal-all-boundp (list-fix x) alist)
         (fal-all-boundp x alist)))

Theorem: fal-all-boundp-of-rev

(defthm fal-all-boundp-of-rev
  (equal (fal-all-boundp (rev x) alist)
         (fal-all-boundp x alist)))

Theorem: fal-all-boundp-of-append

(defthm fal-all-boundp-of-append
  (equal (fal-all-boundp (append x y) alist)
         (and (fal-all-boundp x alist)
              (fal-all-boundp y alist))))

Theorem: fal-all-boundp-of-revappend

(defthm fal-all-boundp-of-revappend
  (equal (fal-all-boundp (revappend x y) alist)
         (and (fal-all-boundp x alist)
              (fal-all-boundp y alist))))

Subtopics

Fal-all-boundp-slow
Fal-all-boundp-fast