• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Community
  • Std
    • Std/lists
    • Omaps
      • Defomap
      • Update
      • Mapp
      • Assoc
      • Update*
      • From-lists
      • Keys
      • List-lookup
      • Size
      • Compatiblep
      • Submap
      • Tail
      • Restrict
      • Head
      • Update-induction-on-maps
      • Rlookup
      • Lookup
      • List-notin
      • Emptyp
      • Rlookup*
      • Map
      • Lookup*
      • Values
      • List-in
      • Delete*
      • In*
      • Delete
      • From-alist
      • Mfix
      • Head-val
      • Head-key
      • Omap-induction2
      • Omap-order-rules
    • Std/alists
    • Obags
    • Std/util
    • Std/strings
    • Std/osets
    • Std/io
    • Std/basic
    • Std/system
    • Std/typed-lists
    • Std/bitsets
    • Std/testing
    • Std/typed-alists
    • Std/stobjs
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Omaps

Update*

Update a map with another map.

Signature

(update* new old) → map

Arguments

new — Guard (mapp new).

old — Guard (mapp old).

Returns

map — Type (mapp map).

This lifts update from a single key and value to a set of key-value pairs, passed as the first argument map. If a key is in the second but not in the first map, the key is present in the result, with the same value as in the second map. If a key is in the first but not in the second map, the key is present in the result, with the same value as in the first map. If a key is present in both maps, it is present in the result, with the same value as in the first map; i.e. the first map ``wins''. There are no other keys in the result.

Definitions and Theorems

Function: update*

(defun update* (new old)
  (declare (xargs :guard (and (mapp new) (mapp old))))
  (let ((__function__ 'update*))
    (declare (ignorable __function__))
    (cond ((emptyp new) (mfix old))
          (t (mv-let (new-key new-val)
                     (head new)
               (update new-key
                       new-val (update* (tail new) old)))))))

Theorem: mapp-of-update*

(defthm mapp-of-update*
  (b* ((map (update* new old)))
    (mapp map))
  :rule-classes :rewrite)

Theorem: update*-when-left-emptyp

(defthm update*-when-left-emptyp
  (implies (emptyp new)
           (equal (update* new old) (mfix old))))

Theorem: update*-when-right-emptyp

(defthm update*-when-right-emptyp
  (implies (emptyp old)
           (equal (update* new old) (mfix new))))

Theorem: update*-of-mfix-new

(defthm update*-of-mfix-new
  (equal (update* (mfix new) old)
         (update* new old)))

Theorem: update*-mequiv-congruence-on-new

(defthm update*-mequiv-congruence-on-new
  (implies (mequiv new new-equiv)
           (equal (update* new old)
                  (update* new-equiv old)))
  :rule-classes :congruence)

Theorem: update*-of-mfix-old

(defthm update*-of-mfix-old
  (equal (update* new (mfix old))
         (update* new old)))

Theorem: update*-mequiv-congruence-on-old

(defthm update*-mequiv-congruence-on-old
  (implies (mequiv old old-equiv)
           (equal (update* new old)
                  (update* new old-equiv)))
  :rule-classes :congruence)