		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 ((empty 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-when-empty

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

Theorem: keys-iff-not-empty

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

Theorem: in-to-in-of-keys

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

Theorem: in-keys-when-in-forward

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

Theorem: keys-of-update

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