• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
    • Std/lists
    • Std/alists
      • Alist-keys
      • Remove-assocs
      • Alist-vals
      • Alist-map-vals
      • Std/alists/strip-cdrs
      • Hons-rassoc-equal
      • Alist-map-keys
      • Std/alists/hons-assoc-equal
      • Fal-extract
      • Std/alists/strip-cars
      • Fal-find-any
      • Fal-extract-vals
      • Std/alists/abstract
      • Fal-all-boundp
      • Std/alists/alistp
      • Append-alist-vals
      • Append-alist-keys
      • Alist-equiv
      • Hons-remove-assoc
      • Std/alists/pairlis$
      • Alists-agree
      • Worth-hashing
      • 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

Sub-alistp

(sub-alistp a b) determines whether every key bound in the alist a is also bound to the same value in the alist b.

Definitions and Theorems

Function: sub-alistp

(defun
  sub-alistp (a b)
  "Is every key bound in A also bound to the same value in B?"
  (declare (xargs :guard t))
  (mbe :logic (alists-agree (alist-keys a) a b)
       :exec
       (with-fast-alist
            a
            (with-fast-alist b (alists-agree (alist-keys a) a b)))))

Theorem: sub-alistp-self

(defthm sub-alistp-self (sub-alistp x x))

Theorem: sub-alistp-hons-assoc-equal

(defthm sub-alistp-hons-assoc-equal
        (implies (and (sub-alistp a b)
                      (hons-assoc-equal x a))
                 (equal (hons-assoc-equal x a)
                        (hons-assoc-equal x b))))

Function: not-sub-alistp-witness

(defun not-sub-alistp-witness (a b)
       (alists-disagree-witness (alist-keys a)
                                a b))

Theorem: sub-alistp-iff-witness

(defthm sub-alistp-iff-witness
        (iff (sub-alistp a b)
             (let ((x (not-sub-alistp-witness a b)))
                  (implies (hons-assoc-equal x a)
                           (equal (hons-assoc-equal x a)
                                  (hons-assoc-equal x b))))))

Theorem: sub-alistp-when-witness

(defthm sub-alistp-when-witness
        (implies (let ((x (not-sub-alistp-witness a b)))
                      (implies (hons-assoc-equal x a)
                               (equal (hons-assoc-equal x a)
                                      (hons-assoc-equal x b))))
                 (sub-alistp a b)))

Theorem: sub-alistp-trans

(defthm sub-alistp-trans
        (implies (and (sub-alistp x y) (sub-alistp y z))
                 (sub-alistp x z)))