		Search-engine friendly clone of the ACL2 documentation.

Omaps

In

Check if a key is in an omap.

Signature
(in key map) → pair?
Arguments: map — Guard (mapp map).
Returns: pair? — Type (listp pair?).

If the key is present, return the cons pair with the key. Otherwise, return nil.

This is similar to set::in for osets.

Definitions and Theorems

Function: in

(defun in (key map)
  (declare (xargs :guard (mapp map)))
  (let ((__function__ 'in))
    (declare (ignorable __function__))
    (cond ((empty map) nil)
          (t (mv-let (key0 val0)
                     (head map)
               (cond ((equal key key0) (cons key0 val0))
                     (t (in key (tail map)))))))))

Theorem: listp-of-in

(defthm listp-of-in
  (b* ((pair? (in key map)))
    (listp pair?))
  :rule-classes :rewrite)

Theorem: in-of-mfix

(defthm in-of-mfix
  (equal (in key (mfix map))
         (in key map)))

Theorem: in-when-empty

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

Theorem: in-of-head

(defthm in-of-head
  (iff (in (mv-nth 0 (head map)) map)
       (not (empty map))))

Theorem: in-when-in-tail

(defthm in-when-in-tail
  (implies (in key (tail map))
           (in key map)))

Theorem: acl2-count-in-<-map

(defthm acl2-count-in-<-map
  (implies (not (empty map))
           (< (acl2-count (in key map))
              (acl2-count map))))

Theorem: in-of-update

(defthm in-of-update
  (equal (in key1 (update key val map))
         (if (equal key1 key)
             (cons key val)
           (in key1 map))))

Theorem: in-of-update*

(defthm in-of-update*
  (equal (in key (update* map1 map2))
         (or (in key map1) (in key map2))))

Theorem: update-of-cdr-of-in-when-in

(defthm update-of-cdr-of-in-when-in
  (implies (in k m)
           (equal (update k (cdr (in k m)) m) m)))

Theorem: consp-of-in-iff-in

(defthm consp-of-in-iff-in
  (iff (consp (in key map)) (in key map)))