		Search-engine friendly clone of the ACL2 documentation.

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