• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
    • Std/lists
    • Std/alists
      • Alist-keys
      • Remove-assocs
      • Alist-vals
      • Alist-map-vals
      • Alist-map-keys
      • Std/alists/strip-cdrs
      • Hons-rassoc-equal
      • Std/alists/hons-assoc-equal
      • Std/alists/strip-cars
      • Fal-find-any
      • Fal-extract
      • Std/alists/abstract
      • Fal-extract-vals
      • Fal-all-boundp
        • Fal-all-boundp-slow
        • Fal-all-boundp-fast
      • Std/alists/alistp
      • Append-alist-vals
      • Append-alist-keys
      • Alist-equiv
      • Hons-remove-assoc
      • Std/alists/pairlis$
      • Worth-hashing
      • Alists-agree
      • Sub-alistp
      • Alist-fix
      • Std/alists/remove-assoc-equal
      • Std/alists/assoc-equal
    • Obags
    • Std/util
    • Std/strings
    • Std/io
    • Std/osets
    • Std/system
    • Std/basic
    • Std/typed-lists
    • Std/bitsets
    • Std/testing
    • Std/typed-alists
    • Std/stobjs
    • Std-extensions
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Testing-utilities
  • Math

• 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