• 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

From-lists

Build an omap from a list of keys and a list of corresponding values.

Signature

(from-lists keys vals) → map

Arguments

keys — Guard (true-listp keys).

vals — Guard (true-listp vals).

Returns

map — Type (mapp map).

If there are duplicate keys in the first list, the leftmost key, and the corresponding value, will be in the resulting omap.

Definitions and Theorems

Function: from-lists

(defun from-lists (keys vals)
  (declare (xargs :guard (and (true-listp keys)
                              (true-listp vals))))
  (declare (xargs :guard (= (len keys) (len vals))))
  (let ((__function__ 'from-lists))
    (declare (ignorable __function__))
    (cond ((endp keys) nil)
          (t (update (car keys)
                     (car vals)
                     (from-lists (cdr keys) (cdr vals)))))))

Theorem: mapp-of-from-lists

(defthm mapp-of-from-lists
  (b* ((map (from-lists keys vals)))
    (mapp map))
  :rule-classes :rewrite)

Theorem: list-lookup-of-from-lists-of-append-first

(defthm list-lookup-of-from-lists-of-append-first
  (implies (and (equal (len keys1) (len vals1))
                (no-duplicatesp-equal keys1))
           (equal (list-lookup keys1
                               (from-lists (append keys1 keys2)
                                           (append vals1 vals2)))
                  (true-list-fix vals1))))

Theorem: list-lookup-of-from-lists-of-append-second

(defthm list-lookup-of-from-lists-of-append-second
  (implies (and (equal (len keys1) (len vals1))
                (not (intersectp-equal keys keys1)))
           (equal (list-lookup keys
                               (from-lists (append keys1 keys2)
                                           (append vals1 vals2)))
                  (list-lookup keys (from-lists keys2 vals2)))))

Theorem: from-lists-of-list-fix-keys

(defthm from-lists-of-list-fix-keys
  (equal (from-lists (list-fix keys) vals)
         (from-lists keys vals)))

Theorem: from-lists-list-equiv-congruence-on-keys

(defthm from-lists-list-equiv-congruence-on-keys
  (implies (list-equiv keys keys-equiv)
           (equal (from-lists keys vals)
                  (from-lists keys-equiv vals)))
  :rule-classes :congruence)

Theorem: from-lists-of-list-fix-vals

(defthm from-lists-of-list-fix-vals
  (equal (from-lists keys (list-fix vals))
         (from-lists keys vals)))

Theorem: from-lists-list-equiv-congruence-on-vals

(defthm from-lists-list-equiv-congruence-on-vals
  (implies (list-equiv vals vals-equiv)
           (equal (from-lists keys vals)
                  (from-lists keys vals-equiv)))
  :rule-classes :congruence)