		Search-engine friendly clone of the ACL2 documentation.

Candidates-with-min-votes

All-keys

Returns a list of all the keys in alst with the value val

Signature
(all-keys val alst) → cids
Arguments: val — Guard (natp val).; alst — Guard (count-alistp alst).
Returns: cids — Type (nat-listp cids), given the guard.

Definitions and Theorems

Theorem: consp-of-rassoc-equal

(defthm consp-of-rassoc-equal
  (implies (and (alistp alst)
                (rassoc-equal val alst))
           (consp (rassoc-equal val alst))))

Theorem: count-alistp-of-remove1-assoc-equal

(defthm count-alistp-of-remove1-assoc-equal
  (implies (count-alistp alst)
           (count-alistp (remove1-assoc-equal key alst))))

Function: all-keys

(defun all-keys (val alst)
  (declare (xargs :guard (and (natp val) (count-alistp alst))))
  (let ((__function__ 'all-keys))
    (declare (ignorable __function__))
    (if (endp alst)
        nil
      (b* ((pair (rassoc-equal val alst)))
        (if (equal pair nil)
            nil
          (cons (car pair)
                (all-keys val
                          (remove1-assoc-equal (car pair)
                                               alst))))))))

Theorem: nat-listp-of-all-keys

(defthm nat-listp-of-all-keys
  (implies (and (natp val) (count-alistp alst))
           (b* ((cids (all-keys val alst)))
             (nat-listp cids)))
  :rule-classes :rewrite)

Theorem: remove1-assoc-equal-and-subset-equal

(defthm remove1-assoc-equal-and-subset-equal
  (subsetp-equal (remove1-assoc-equal val alst)
                 alst))

Theorem: strip-cars-of-remove1-assoc-equal-and-subset-equal

(defthm strip-cars-of-remove1-assoc-equal-and-subset-equal
  (subsetp-equal (strip-cars (remove1-assoc-equal val alst))
                 (strip-cars alst)))

Theorem: all-keys-returns-nil-when-value-not-found-in-alist

(defthm all-keys-returns-nil-when-value-not-found-in-alist
  (implies (not (member-equal val (strip-cdrs alst)))
           (equal (all-keys val alst) nil)))

Theorem: rassoc-equal-is-non-empty-when-non-nil-value-found-in-alist

(defthm rassoc-equal-is-non-empty-when-non-nil-value-found-in-alist
  (implies (and (member-equal val (strip-cdrs alst))
                val)
           (rassoc-equal val alst)))

Theorem: all-keys-is-non-empty-when-non-nil-value-found-in-alist

(defthm all-keys-is-non-empty-when-non-nil-value-found-in-alist
  (implies (and (member-equal val (strip-cdrs alst))
                val)
           (all-keys val alst)))

Theorem: nil-is-not-a-member-of-any-nat-listp

(defthm nil-is-not-a-member-of-any-nat-listp
  (implies (nat-listp lst)
           (equal (member-equal nil lst) nil)))

Theorem: all-keys-returns-a-subset-of-keys-helper

(defthm all-keys-returns-a-subset-of-keys-helper
  (implies (member-equal val (strip-cdrs alst))
           (subsetp-equal (all-keys val alst)
                          (strip-cars alst))))

Theorem: all-keys-returns-a-subset-of-keys

(defthm all-keys-returns-a-subset-of-keys
  (subsetp-equal (all-keys val alst)
                 (strip-cars alst)))