		Search-engine friendly clone of the ACL2 documentation.

Omaps

Update

Set a key to a value in an omap.

Signature
(update key val map) → map1
Arguments: map — Guard (mapp map).
Returns: map1 — Type (mapp map1).

If the key is not already in the map, it is added, with the value. If the key is already in the map, the new value overrides the old value.

This is similar to insert for osets.

Definitions and Theorems

Function: update

(defun update (key val map)
  (declare (xargs :guard (mapp map)))
  (let ((__function__ 'update))
    (declare (ignorable __function__))
    (cond ((emptyp map) (list (cons key val)))
          (t (mv-let (key0 val0)
                     (head map)
               (cond ((equal key key0)
                      (cons (cons key val) (tail map)))
                     ((<< key key0)
                      (cons (cons key val) map))
                     (t (cons (cons key0 val0)
                              (update key val (tail map))))))))))

Theorem: mapp-of-update

(defthm mapp-of-update
  (b* ((map1 (update key val map)))
    (mapp map1))
  :rule-classes :rewrite)

Theorem: update-of-head-and-tail

(defthm update-of-head-and-tail
  (implies (not (emptyp map))
           (equal (update (mv-nth 0 (head map))
                          (mv-nth 1 (head map))
                          (tail map))
                  map))
  :rule-classes :elim)

Theorem: update-not-emptyp

(defthm update-not-emptyp
  (not (emptyp (update key val map))))

Theorem: update-same

(defthm update-same
  (equal (update key val1 (update key val2 map))
         (update key val1 map)))

Theorem: update-different

(defthm update-different
  (implies (not (equal key1 key2))
           (equal (update key1 val1 (update key2 val2 map))
                  (update key2 val2 (update key1 val1 map)))))

Theorem: update-when-emptyp

(defthm update-when-emptyp
  (implies (and (syntaxp (not (equal map ''nil)))
                (emptyp map))
           (equal (update key val map)
                  (update key val nil))))

Theorem: head-key-of-update-of-nil

(defthm head-key-of-update-of-nil
  (equal (mv-nth 0 (head (update key val nil)))
         key))

Theorem: head-value-of-update-of-nil

(defthm head-value-of-update-of-nil
  (equal (mv-nth 1 (head (update key val nil)))
         val))

Theorem: tail-of-update-of-nil

(defthm tail-of-update-of-nil
  (equal (tail (update key val nil)) nil))

Theorem: head-of-update

(defthm head-of-update
  (equal (head (update key val map))
         (cond ((emptyp map) (mv key val))
               ((<< (mv-nth 0 (head map)) key)
                (head map))
               (t (mv key val)))))

Theorem: head-key-of-update

(defthm head-key-of-update
  (equal (mv-nth 0 (head (update key val map)))
         (cond ((emptyp map) key)
               ((<< (mv-nth 0 (head map)) key)
                (mv-nth 0 (head map)))
               (t key))))

Theorem: head-value-of-update

(defthm head-value-of-update
  (equal (mv-nth 1 (head (update key val map)))
         (cond ((emptyp map) val)
               ((<< (mv-nth 0 (head map)) key)
                (mv-nth 1 (head map)))
               (t val))))

Theorem: tail-of-update

(defthm tail-of-update
  (equal (tail (update key val map))
         (cond ((emptyp map) nil)
               ((<< key (mv-nth 0 (head map))) map)
               ((equal key (mv-nth 0 (head map)))
                (tail map))
               (t (update key val (tail map))))))

Theorem: head-value-of-update-emptyp

(defthm head-value-of-update-emptyp
  (implies (emptyp map)
           (equal (mv-nth 1 (head (update key val map)))
                  val)))

Theorem: head-value-of-update-key-<<

(defthm head-value-of-update-key-<<
  (implies (and (not (emptyp map))
                (or (<< key (mv-nth 0 (head map)))
                    (equal key (mv-nth 0 (head map)))))
           (equal (mv-nth 1 (head (update key val map)))
                  val)))

Theorem: head-value-of-update-when-head-key-equal

(defthm head-value-of-update-when-head-key-equal
  (implies (equal (mv-nth 0 (head (update key val x)))
                  key)
           (equal (mv-nth 1 (head (update key val x)))
                  val)))

Theorem: head-value-of-update-not-<<

(defthm head-value-of-update-not-<<
  (implies (and (not (emptyp map))
                (<< (mv-nth 0 (head map)) key))
           (equal (mv-nth 1 (head (update key val map)))
                  (mv-nth 1 (head map)))))

Theorem: tail-of-update-emptyp

(defthm tail-of-update-emptyp
  (implies (emptyp map)
           (equal (tail (update key val map))
                  nil)))

Theorem: tail-of-update-<<

(defthm tail-of-update-<<
  (implies (and (not (emptyp map))
                (<< key (mv-nth 0 (head map))))
           (equal (tail (update key val map))
                  map)))

Theorem: tail-of-update-equal

(defthm tail-of-update-equal
  (implies (and (not (emptyp map))
                (equal key (mv-nth 0 (head map))))
           (equal (tail (update key val map))
                  (tail map))))

Theorem: tail-of-update-<<-rev

(defthm tail-of-update-<<-rev
  (implies (and (not (emptyp map))
                (<< (mv-nth 0 (head map)) key))
           (equal (tail (update key val map))
                  (update key val (tail map)))))