		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 ((emptyp sub) t)
          (t (mv-let (key val)
                     (head sub)
               (and (equal (assoc 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-emptyp

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

Theorem: submap-when-right-emptyp

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