Check if a key is in an omap.
If the key is present, return the cons pair with the key.
Otherwise, return
This is similar to set::in for osets.
Function:
(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:
(defthm listp-of-in (b* ((pair? (in key map))) (listp pair?)) :rule-classes :rewrite)
Theorem:
(defthm in-of-mfix (equal (in key (mfix map)) (in key map)))
Theorem:
(defthm in-when-empty (implies (empty map) (equal (in key map) nil)) :rule-classes (:rewrite :type-prescription))
Theorem:
(defthm in-of-head (iff (in (mv-nth 0 (head map)) map) (not (empty map))))
Theorem:
(defthm in-when-in-tail (implies (in key (tail map)) (in key map)))
Theorem:
(defthm acl2-count-in-<-map (implies (not (empty map)) (< (acl2-count (in key map)) (acl2-count map))))
Theorem:
(defthm in-of-update (equal (in key1 (update key val map)) (if (equal key1 key) (cons key val) (in key1 map))))
Theorem:
(defthm in-of-update* (equal (in key (update* map1 map2)) (or (in key map1) (in key map2))))
Theorem:
(defthm update-of-cdr-of-in-when-in (implies (in k m) (equal (update k (cdr (in k m)) m) m)))
Theorem:
(defthm consp-of-in-iff-in (iff (consp (in key map)) (in key map)))