• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
    • Apt
    • Zfc
    • Acre
    • Milawa
    • Smtlink
    • Abnf
    • Vwsim
    • Isar
    • Wp-gen
    • Dimacs-reader
    • Pfcs
    • Legacy-defrstobj
    • Proof-checker-array
    • Soft
    • C
    • Farray
    • Rp-rewriter
    • Instant-runoff-voting
    • Imp-language
    • Sidekick
    • Leftist-trees
    • Java
    • Taspi
    • Bitcoin
    • Riscv
    • Des
    • Ethereum
    • X86isa
    • Sha-2
    • Yul
    • Zcash
    • Proof-checker-itp13
    • Regex
    • ACL2-programming-language
    • Json
    • Jfkr
    • Equational
    • Cryptography
    • Poseidon
    • Where-do-i-place-my-book
    • Axe
    • Bigmems
    • Builtins
    • Execloader
    • Aleo
      • Aleobft
        • Aleobft-static
        • Aleobft-stake2
        • Aleobft-dynamic
        • Aleobft-stake
        • Aleobft-proposals
        • Library-extensions
          • Lists-noforkp
          • Oset-theorems
          • Omap-theorems
          • Arithmetic-theorems
      • Leo
    • Solidity
    • Paco
    • Concurrent-programs
    • Bls12-377-curves
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Library-extensions

Omap-theorems

Some theorems about omaps.

Among other theorems, we introduce pick-a-point reasoning support for omap::submap. This is similar to pick-a-point reasoning fo subset, but we use a defun-sk and a ruleset for omaps, instead of the approach used for osets.

Definitions and Theorems

Theorem: lookup-of-update

(defthm omap::lookup-of-update
  (equal (omap::lookup key (omap::update key1 val map))
         (if (equal key key1)
             val
           (omap::lookup key map))))

Theorem: emptyp-of-keys-to-emptyp

(defthm omap::emptyp-of-keys-to-emptyp
  (equal (emptyp (omap::keys map))
         (omap::emptyp map)))

Theorem: keys-of-delete

(defthm omap::keys-of-delete
  (equal (omap::keys (omap::delete key map))
         (delete key (omap::keys map))))

Theorem: assoc-of-delete

(defthm omap::assoc-of-delete
  (equal (omap::assoc key1 (omap::delete key map))
         (if (equal key1 key)
             nil
           (omap::assoc key1 map))))

Theorem: lookup-of-delete

(defthm omap::lookup-of-delete
  (equal (omap::lookup key1 (omap::delete key map))
         (if (equal key1 key)
             nil
           (omap::lookup key1 map))))

Theorem: assoc-of-submap-is-assoc-of-supermap-when-present

(defthm omap::assoc-of-submap-is-assoc-of-supermap-when-present
  (implies (omap::submap map1 map2)
           (implies (omap::assoc key map1)
                    (equal (omap::assoc key map1)
                           (omap::assoc key map2)))))

Theorem: submap-sk-necc

(defthm omap::submap-sk-necc
  (implies (omap::submap-sk map1 map2)
           (implies (omap::assoc key map1)
                    (equal (omap::assoc key map1)
                           (omap::assoc key map2)))))

Theorem: booleanp-of-submap-sk

(defthm omap::booleanp-of-submap-sk
  (b* ((bool (omap::submap-sk map1 map2)))
    (booleanp bool))
  :rule-classes :type-prescription)

Theorem: submap-sk-of-tail-when-submap-sk

(defthm omap::submap-sk-of-tail-when-submap-sk
  (implies (omap::submap-sk map1 map2)
           (omap::submap-sk (omap::tail map1)
                            map2)))

Theorem: submap-sk-when-submap

(defthm omap::submap-sk-when-submap
  (implies (omap::submap map1 map2)
           (omap::submap-sk map1 map2)))

Theorem: submap-when-submap-sk

(defthm omap::submap-when-submap-sk
  (implies (omap::submap-sk map1 map2)
           (omap::submap map1 map2)))

Theorem: submap-to-submap-sk

(defthm omap::submap-to-submap-sk
  (equal (omap::submap map1 map2)
         (omap::submap-sk map1 map2)))

Theorem: submap-of-delete

(defthm submap-of-delete
  (omap::submap (omap::delete key map)
                map))