		Search-engine friendly clone of the ACL2 documentation.

Std/alists/pairlis$

Lemmas about pairlis$ available in the std/alists library.

(pairlis$ x y) is a perfectly reasonable way to create a proper, nil-terminated alistp which can be used with either "traditional" or "modern" alist functions.

Definitions and Theorems

Theorem: pairlis$-when-atom

(defthm pairlis$-when-atom
        (implies (atom x)
                 (equal (pairlis$ x y) nil)))

Theorem: pairlis$-of-cons

(defthm pairlis$-of-cons
        (equal (pairlis$ (cons a x) y)
               (cons (cons a (car y))
                     (pairlis$ x (cdr y)))))

Theorem: len-of-pairlis$

(defthm len-of-pairlis$
        (equal (len (pairlis$ x y)) (len x)))

Theorem: alistp-of-pairlis$

(defthm alistp-of-pairlis$
        (alistp (pairlis$ x y)))

Theorem: strip-cars-of-pairlis$

(defthm strip-cars-of-pairlis$
        (equal (strip-cars (pairlis$ x y))
               (list-fix x)))

Theorem: strip-cdrs-of-pairlis$

(defthm strip-cdrs-of-pairlis$
        (equal (strip-cdrs (pairlis$ x y))
               (take (len x) y)))

Theorem: pairlis$-of-list-fix-left

(defthm pairlis$-of-list-fix-left
        (equal (pairlis$ (list-fix x) y)
               (pairlis$ x y)))

Theorem: pairlis$-of-list-fix-right

(defthm pairlis$-of-list-fix-right
        (equal (pairlis$ x (list-fix y))
               (pairlis$ x y)))

Theorem: list-equiv-implies-equal-pairlis$-1

(defthm list-equiv-implies-equal-pairlis$-1
        (implies (list-equiv x x-equiv)
                 (equal (pairlis$ x y)
                        (pairlis$ x-equiv y)))
        :rule-classes (:congruence))

Theorem: list-equiv-implies-equal-pairlis$-2

(defthm list-equiv-implies-equal-pairlis$-2
        (implies (list-equiv y y-equiv)
                 (equal (pairlis$ x y)
                        (pairlis$ x y-equiv)))
        :rule-classes (:congruence))