		Search-engine friendly clone of the ACL2 documentation.

Omaps

Keys

Oset of the keys of an omap.

Signature
(keys map) → keys
Arguments: map — Guard (mapp map).
Returns: keys — Type (setp keys).

Definitions and Theorems

Function: keys

(defun keys (map)
  (declare (xargs :guard (mapp map)))
  (let ((__function__ 'keys))
    (declare (ignorable __function__))
    (cond ((emptyp map) nil)
          (t (mv-let (key val)
                     (head map)
               (declare (ignore val))
               (insert key (keys (tail map))))))))

Theorem: setp-of-keys

(defthm setp-of-keys
  (b* ((keys (keys map))) (setp keys))
  :rule-classes :rewrite)

Theorem: keys-of-mfix

(defthm keys-of-mfix
  (equal (keys (mfix map)) (keys map)))

Theorem: keys-when-emptyp

(defthm keys-when-emptyp
  (implies (emptyp map)
           (equal (keys map) nil))
  :rule-classes (:rewrite :type-prescription))

Theorem: keys-iff-not-emptyp

(defthm keys-iff-not-emptyp
  (iff (keys map) (not (emptyp map))))

Theorem: consp-of-assoc-to-in-of-keys

(defthm consp-of-assoc-to-in-of-keys
  (equal (consp (assoc key map))
         (set::in key (keys map))))

Theorem: assoc-to-in-of-keys

(defthm assoc-to-in-of-keys
  (iff (assoc key map)
       (set::in key (keys map))))

Theorem: in-of-keys-to-assoc

(defthm in-of-keys-to-assoc
  (iff (set::in key (keys map))
       (assoc key map)))

Theorem: in-keys-when-assoc-forward

(defthm in-keys-when-assoc-forward
  (implies (assoc key map)
           (set::in key (keys map)))
  :rule-classes :forward-chaining)

Theorem: in-keys-when-assoc-is-cons

(defthm in-keys-when-assoc-is-cons
  (implies (equal (assoc a m) (cons a b))
           (set::in a (keys m))))

Theorem: keys-of-update

(defthm keys-of-update
  (equal (keys (update key val m))
         (insert key (keys m))))

Theorem: keys-of-update*

(defthm keys-of-update*
  (equal (keys (update* new old))
         (union (keys new) (keys old))))

Theorem: keys-of-restrict

(defthm keys-of-restrict
  (equal (keys (restrict keys map))
         (intersect keys (keys map))))

Theorem: head-key-not-in-keys-of-tail

(defthm head-key-not-in-keys-of-tail
  (not (set::in (mv-nth 0 (head map))
                (keys (tail map)))))