		Search-engine friendly clone of the ACL2 documentation.

Omaps

Submap

Check if an omap is a submap of another omap.

Signature
(submap sub sup) → yes/no
Arguments: sub — Guard (mapp sub).; sup — Guard (mapp sup).
Returns: yes/no — Type (booleanp yes/no).

This is true when every key in the first omap is also in the second omap, and the two omaps agree on the common keys.

This is similar to subset for osets.

Definitions and Theorems

Function: submap

(defun submap (sub sup)
  (declare (xargs :guard (and (mapp sub) (mapp sup))))
  (let ((__function__ 'submap))
    (declare (ignorable __function__))
    (cond ((empty sub) t)
          (t (mv-let (key val)
                     (head sub)
               (and (equal (in key sup) (cons key val))
                    (submap (tail sub) sup)))))))

Theorem: booleanp-of-submap

(defthm booleanp-of-submap
  (b* ((yes/no (submap sub sup)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: submap-when-left-empty

(defthm submap-when-left-empty
  (implies (empty sub) (submap sub sup)))

Theorem: submap-when-right-empty

(defthm submap-when-right-empty
  (implies (empty sup)
           (equal (submap sub sup) (empty sub))))