		Search-engine friendly clone of the ACL2 documentation.

Omaps

Rlookup

Set of keys to which a value is associated.

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

The resulting set is empty if the value is not in the omap. The resulting set is a singleton if the value is associated to exactly one key. Otherwise, the resulting set contains two or more keys.

This is the ``reverse'' of lookup, which motivates the r in the name.

Definitions and Theorems

Function: rlookup

(defun
    rlookup (val map)
    (declare (xargs :guard (mapp map)))
    (let ((__function__ 'rlookup))
         (declare (ignorable __function__))
         (cond ((empty map) nil)
               (t (mv-let (key0 val0)
                          (head map)
                          (if (equal val val0)
                              (insert key0 (rlookup val (tail map)))
                              (rlookup val (tail map))))))))

Theorem: setp-of-rlookup

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

Theorem: rlookup-when-empty

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