		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 ((emptyp 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-emptyp

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

Theorem: rlookup-of-mfix-map

(defthm rlookup-of-mfix-map
  (equal (rlookup val (mfix map))
         (rlookup val map)))

Theorem: rlookup-mequiv-congruence-on-map

(defthm rlookup-mequiv-congruence-on-map
  (implies (mequiv map map-equiv)
           (equal (rlookup val map)
                  (rlookup val map-equiv)))
  :rule-classes :congruence)