fal-all-boundp

(in-package "ACL2")

(define fal-all-boundp-fast
  (keys alist)
  :parents (fal-all-boundp)
  (if (atom keys)
    t
    (and (hons-get (car keys) alist)
      (fal-all-boundp-fast (cdr keys) alist))))

(define fal-all-boundp-slow
  (keys alist)
  :parents (fal-all-boundp)
  (if (atom keys)
    t
    (and (hons-assoc-equal (car keys) alist)
      (fal-all-boundp-slow (cdr keys) alist))))

(define fal-all-boundp
  (keys alist)
  :parents (std/alists)
  :short "@(call fal-all-boundp) determines if every key in @('keys') is bound
in the alist @('alist')."
  :long "<p>The @('alist') need not be fast.  If it is not fast, it may be made
temporarily fast, depending on its length.</p>"
  :returns bool
  (declare (xargs :guard t :verify-guards nil))
  (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))))
  ///
  (defthm fal-all-boundp-fast-removal
    (equal (fal-all-boundp-fast keys alist)
      (fal-all-boundp keys alist))
    :hints (("Goal" :in-theory (enable fal-all-boundp-fast))))
  (defthm fal-all-boundp-slow-removal
    (equal (fal-all-boundp-slow keys alist)
      (fal-all-boundp keys alist))
    :hints (("Goal" :in-theory (enable fal-all-boundp-slow))))
  (verify-guards fal-all-boundp)
  (defthm fal-all-boundp-when-atom
    (implies (atom keys) (equal (fal-all-boundp keys alist) t)))
  (defthm fal-all-boundp-of-cons
    (equal (fal-all-boundp (cons a keys) alist)
      (and (hons-get a alist) (fal-all-boundp keys alist))))
  (encapsulate nil
    (local (defthm l0
        (implies (and (fal-all-boundp y alist) (member-equal a y))
          (hons-assoc-equal a alist))))
    (local (defthm l1
        (implies (and (fal-all-boundp y alist) (subsetp-equal x y))
          (fal-all-boundp x alist))
        :hints (("Goal" :induct (len x)))))
    (defcong set-equiv
      equal
      (fal-all-boundp x alist)
      1
      :hints (("Goal" :in-theory (e/d (set-equiv) (l1))
         :use ((:instance l1 (x x) (y x-equiv)) (:instance l1 (x x-equiv) (y x)))))))
  (defcong alist-equiv equal (fal-all-boundp x alist) 2)
  (defthm fal-all-boundp-of-list-fix
    (equal (fal-all-boundp (list-fix x) alist)
      (fal-all-boundp x alist)))
  (defthm fal-all-boundp-of-rev
    (equal (fal-all-boundp (rev x) alist)
      (fal-all-boundp x alist)))
  (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))))
  (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)))))