• 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

Keys

Oset of the keys of an omap.

Signature

(keys map) → keys

Arguments

map — Guard (mapp map).

Returns

keys — Type (setp keys).

Definitions and Theorems

Function: keys

(defun keys (map)
  (declare (xargs :guard (mapp map)))
  (let ((__function__ 'keys))
    (declare (ignorable __function__))
    (cond ((emptyp map) nil)
          (t (mv-let (key val)
                     (head map)
               (declare (ignore val))
               (insert key (keys (tail map))))))))

Theorem: setp-of-keys

(defthm setp-of-keys
  (b* ((keys (keys map))) (setp keys))
  :rule-classes :rewrite)

Theorem: keys-of-mfix

(defthm keys-of-mfix
  (equal (keys (mfix map)) (keys map)))

Theorem: keys-when-emptyp

(defthm keys-when-emptyp
  (implies (emptyp map)
           (equal (keys map) nil))
  :rule-classes (:rewrite :type-prescription))

Theorem: keys-iff-not-emptyp

(defthm keys-iff-not-emptyp
  (iff (keys map) (not (emptyp map))))

Theorem: consp-of-assoc-to-in-of-keys

(defthm consp-of-assoc-to-in-of-keys
  (equal (consp (assoc key map))
         (set::in key (keys map))))

Theorem: assoc-to-in-of-keys

(defthm assoc-to-in-of-keys
  (iff (assoc key map)
       (set::in key (keys map))))

Theorem: in-of-keys-to-assoc

(defthm in-of-keys-to-assoc
  (iff (set::in key (keys map))
       (assoc key map)))

Theorem: list-in-to-subset-keys

(defthm list-in-to-subset-keys
  (iff (list-in keys map)
       (subset (mergesort keys) (keys map))))

Theorem: in-keys-when-assoc-forward

(defthm in-keys-when-assoc-forward
  (implies (assoc key map)
           (set::in key (keys map)))
  :rule-classes :forward-chaining)

Theorem: in-keys-when-assoc-is-cons

(defthm in-keys-when-assoc-is-cons
  (implies (equal (assoc a m) (cons a b))
           (set::in a (keys m))))

Theorem: keys-of-update

(defthm keys-of-update
  (equal (keys (update key val m))
         (insert key (keys m))))

Theorem: keys-of-update*

(defthm keys-of-update*
  (equal (keys (update* new old))
         (union (keys new) (keys old))))

Theorem: keys-of-restrict

(defthm keys-of-restrict
  (equal (keys (restrict keys map))
         (intersect keys (keys map))))

Theorem: head-key-not-in-keys-of-tail

(defthm head-key-not-in-keys-of-tail
  (not (set::in (mv-nth 0 (head map))
                (keys (tail map)))))

Theorem: keys-of-mfix-map

(defthm keys-of-mfix-map
  (equal (keys (mfix map)) (keys map)))

Theorem: keys-mequiv-congruence-on-map

(defthm keys-mequiv-congruence-on-map
  (implies (mequiv map map-equiv)
           (equal (keys map) (keys map-equiv)))
  :rule-classes :congruence)