• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
    • Std/lists
    • Std/alists
    • Obags
    • Std/util
    • Std/strings
    • Std/osets
      • Omaps
        • Defomap
        • Update
        • Mapp
        • Assoc
        • Update*
        • Size
        • Keys
        • From-lists
        • Update-induction-on-maps
        • Compatiblep
        • Tail
        • Head
        • Restrict
        • Submap
        • Map
        • Rlookup
        • Emptyp
        • Rlookup*
        • Lookup*
        • Delete*
        • Values
        • In*
        • Lookup
        • Delete
        • Mfix
        • Head-val
        • Head-key
        • Omap-induction2
        • Omap-order-rules
      • All-by-membership
      • Defset
      • In
      • Primitives
      • Subset
      • Mergesort
      • Intersect
      • Union
      • Pick-a-point-subset-strategy
      • Delete
      • Double-containment
      • Difference
      • Cardinality
      • Set
      • Intersectp
    • 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: 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)))))