		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))