		Search-engine friendly clone of the ACL2 documentation.

Std/alists/strip-cars

Lemmas about strip-cars available in the std/alists library.

Note that strip-cars is a "traditional" alist function: it has an alistp guard and fails to respect the non-alist convention. We generally prefer to work with alist-keys instead.

Even so, we provide many lemmas for working with strip-cars, in case for some reason that's what you want to do.

Definitions and Theorems

Theorem: strip-cars-when-atom

(defthm strip-cars-when-atom
  (implies (atom x)
           (equal (strip-cars x) nil)))

Theorem: strip-cars-of-cons

(defthm strip-cars-of-cons
  (equal (strip-cars (cons a x))
         (cons (car a) (strip-cars x))))

Theorem: len-of-strip-cars

(defthm len-of-strip-cars
  (equal (len (strip-cars x)) (len x)))

Theorem: consp-of-strip-cars

(defthm consp-of-strip-cars
  (equal (consp (strip-cars x))
         (consp x)))

Theorem: car-of-strip-cars

(defthm car-of-strip-cars
  (equal (car (strip-cars x))
         (car (car x))))

Theorem: cdr-of-strip-cars

(defthm cdr-of-strip-cars
  (equal (cdr (strip-cars x))
         (strip-cars (cdr x))))

Theorem: strip-cars-under-iff

(defthm strip-cars-under-iff
  (iff (strip-cars x) (consp x)))

Theorem: strip-cars-of-list-fix

(defthm strip-cars-of-list-fix
  (equal (strip-cars (list-fix x))
         (strip-cars x)))

Theorem: set-equiv-implies-set-equiv-strip-cars-1

(defthm set-equiv-implies-set-equiv-strip-cars-1
  (implies (set-equiv x x-equiv)
           (set-equiv (strip-cars x)
                      (strip-cars x-equiv)))
  :rule-classes (:congruence))

Theorem: strip-cars-of-append

(defthm strip-cars-of-append
  (equal (strip-cars (append x y))
         (append (strip-cars x) (strip-cars y))))

Theorem: strip-cars-of-rev

(defthm strip-cars-of-rev
  (equal (strip-cars (rev x))
         (rev (strip-cars x))))

Theorem: strip-cars-of-revappend

(defthm strip-cars-of-revappend
  (equal (strip-cars (revappend x y))
         (revappend (strip-cars x)
                    (strip-cars y))))

Theorem: strip-cars-of-repeat

(defthm strip-cars-of-repeat
  (equal (strip-cars (repeat n x))
         (repeat n (car x))))

Theorem: strip-cars-of-take

(defthm strip-cars-of-take
  (equal (strip-cars (take n x))
         (take n (strip-cars x))))

Theorem: strip-cars-of-nthcdr

(defthm strip-cars-of-nthcdr
  (equal (strip-cars (nthcdr n x))
         (nthcdr n (strip-cars x))))

Theorem: strip-cars-of-last

(defthm strip-cars-of-last
  (equal (strip-cars (last x))
         (last (strip-cars x))))

Theorem: strip-cars-of-butlast

(defthm strip-cars-of-butlast
  (equal (strip-cars (butlast x n))
         (butlast (strip-cars x) n)))

Theorem: strip-cars-of-pairlis$

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