		Search-engine friendly clone of the ACL2 documentation.

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)