pairlis - ACL2 Book

Included Books

other

(in-package "ACL2")

include-book

(include-book "xdoc/top" :dir :system)

include-book

(include-book "../lists/list-defuns")

local

(local (include-book "../lists/take"))

local

(local (in-theory (enable pairlis$)))

local

(local (defthm commutativity-2-of-+
    (equal (+ x (+ y z)) (+ y (+ x z)))))

local

(local (defthm fold-consts-in-+
    (implies (and (syntaxp (quotep x)) (syntaxp (quotep y)))
      (equal (+ x (+ y z)) (+ (+ x y) z)))))

local

(local (defthm distributivity-of-minus-over-+
    (equal (- (+ x y)) (+ (- x) (- y)))))

other

(defsection std/alists/pairlis$
  :parents (std/alists pairlis$)
  :short "Lemmas about @(see pairlis$) available in the @(see std/alists)
library."
  :long "<p>@('(pairlis$ x y)') is a perfectly reasonable way to create a
proper, @('nil')-terminated @(see alistp) which can be used with either
"traditional" or "modern" alist functions.</p>"
  (defthm pairlis$-when-atom
    (implies (atom x) (equal (pairlis$ x y) nil)))
  (defthm pairlis$-of-cons
    (equal (pairlis$ (cons a x) y)
      (cons (cons a (car y)) (pairlis$ x (cdr y)))))
  (defthm len-of-pairlis$
    (equal (len (pairlis$ x y)) (len x)))
  (defthm alistp-of-pairlis$ (alistp (pairlis$ x y)))
  (defthm strip-cars-of-pairlis$
    (equal (strip-cars (pairlis$ x y)) (list-fix x)))
  (local (defthm l0
      (equal (strip-cdrs (pairlis$ x2 nil)) (repeat (len x2) nil))
      :hints (("goal" :in-theory (enable repeat)))))
  (defthm strip-cdrs-of-pairlis$
    (equal (strip-cdrs (pairlis$ x y)) (take (len x) y)))
  (defthm pairlis$-of-list-fix-left
    (equal (pairlis$ (list-fix x) y) (pairlis$ x y)))
  (defthm pairlis$-of-list-fix-right
    (equal (pairlis$ x (list-fix y)) (pairlis$ x y)))
  (defcong list-equiv equal (pairlis$ x y) 1)
  (defcong list-equiv equal (pairlis$ x y) 2))