		Search-engine friendly clone of the ACL2 documentation.

Omaps

Assoc

Find the pair in the omap with a given key.

Signature
(assoc 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 common-lisp::assoc for alists.

Definitions and Theorems

Function: assoc

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

Theorem: listp-of-assoc

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

Theorem: assoc-of-mfix

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

Theorem: assoc-when-emptyp

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

Theorem: assoc-of-head

(defthm assoc-of-head
  (iff (assoc (mv-nth 0 (head map)) map)
       (not (emptyp map))))

Theorem: assoc-when-assoc-tail

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

Theorem: acl2-count-assoc-<-map

(defthm acl2-count-assoc-<-map
  (implies (not (emptyp map))
           (< (acl2-count (assoc key map))
              (acl2-count map))))

Theorem: assoc-of-update

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

Theorem: assoc-of-update*

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

Theorem: consp-of-assoc-of-update*

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

Theorem: update-of-cdr-of-assoc-when-assoc

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

Theorem: consp-of-assoc-iff-assoc

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

Theorem: head-key-minimal

(defthm head-key-minimal
  (implies (<< key (mv-nth 0 (head map)))
           (not (assoc key map))))

Theorem: head-key-not-assoc-tail

(defthm head-key-not-assoc-tail
  (not (assoc (mv-nth 0 (head map))
              (tail map))))

Theorem: assoc-of-tail-when-assoc-of-tail

(defthm assoc-of-tail-when-assoc-of-tail
  (implies (assoc key (tail map))
           (equal (assoc key (tail map))
                  (assoc key map))))

Theorem: assoc-of-tail-when-not-head

(defthm assoc-of-tail-when-not-head
  (implies (not (equal key (mv-nth 0 (head map))))
           (equal (assoc key (tail map))
                  (assoc key map))))