• Top
    • Documentation
    • Books
    • Recursion-and-induction
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
      • Kestrel-books
        • Crypto-hdwallet
        • Error-checking
        • Apt
        • Abnf
        • Fty-extensions
        • Isar
        • Kestrel-utilities
          • Omaps
            • Defomap
            • Update
              • Mapp
              • Update*
              • Size
              • From-lists
              • In
              • Compatiblep
              • Head
              • Rlookup
              • Map
              • Submap
              • Empty
              • Tail
              • In*
              • Rlookup*
              • Restrict
              • Lookup*
              • Delete*
              • Delete
              • Mfix
              • Lookup
              • Values
              • Keys
              • Head-val
              • Head-key
            • Directed-untranslate
            • Include-book-paths
            • Ubi
            • Checkpoint-list
            • Digits-any-base
            • Context-message-pair
            • Numbered-names
            • With-auto-termination
            • Theorems-about-true-list-lists
            • Make-termination-theorem
            • Sublis-expr+
            • Prove$
            • Defthm<w
            • System-utilities-non-built-in
            • Integer-range-fix
            • Add-const-to-untranslate-preprocess
            • Integers-from-to
            • Minimize-ruler-extenders
            • Unsigned-byte-fix
            • Signed-byte-fix
            • Defthmr
            • Paired-names
            • Unsigned-byte-list-fix
            • Signed-byte-list-fix
            • Show-books
            • Checkpoint-list-pretty
            • List-utilities
            • Skip-in-book
            • Typed-tuplep
            • Defunt
            • Keyword-value-list-to-alist
            • Magic-macroexpand
            • Top-command-number-fn
            • Bits-as-digits-in-base-2
            • Show-checkpoint-list
            • Ubyte11s-as-digits-in-base-2048
            • Named-formulas
            • Bytes-as-digits-in-base-256
            • String-utilities
            • Make-keyword-value-list-from-keys-and-value
            • Integer-range-listp
            • Defmacroq
            • Apply-fn-if-known
            • Trans-eval-error-triple
            • Checkpoint-info-list
            • Previous-subsumer-hints
            • Fms!-lst
            • Zp-listp
            • Doublets-to-alist
            • Trans-eval-state
            • Injections
            • Theorems-about-osets
            • Typed-list-utilities
            • Book-runes-alist
            • User-interface
            • Bits/ubyte11s-digit-grouping
            • Bits/bytes-digit-grouping
            • Message-utilities
            • Subsetp-eq-linear
            • Strict-merge-sort-<
            • Miscellaneous-enumerations
            • Maybe-unquote
            • Oset-utilities
            • Thm<w
            • Defthmd<w
          • Prime-field-constraint-systems
          • Soft
          • Bv
          • Imp-language
          • Event-macros
          • Bitcoin
          • Ethereum
          • Yul
          • Zcash
          • ACL2-programming-language
          • Prime-fields
          • Java
          • C
          • Syntheto
          • Number-theory
          • Cryptography
          • Lists-light
          • File-io-light
          • Json
          • Built-ins
          • Solidity
          • Axe
          • Std-extensions
          • Htclient
          • Typed-lists-light
          • Arithmetic-light
        • X86isa
        • Execloader
        • Axe
      • Testing-utilities
      • Math
    • 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
           ((empty 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 (empty map))
                     (equal (update (mv-nth 0 (head map))
                                    (mv-nth 1 (head map))
                                    (tail map))
                            map))
            :rule-classes :elim)

    Theorem: update-not-empty

    (defthm update-not-empty
            (not (empty (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-empty

    (defthm update-when-empty
            (implies (and (syntaxp (not (equal map ''nil)))
                          (empty 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 ((empty 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 ((empty 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 ((empty 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 ((empty map) nil)
                         ((<< key (mv-nth 0 (head map))) map)
                         ((equal key (mv-nth 0 (head map)))
                          (tail map))
                         (t (update key val (tail map))))))