strip-cars

other

(in-package "ACL2")

local

(local (include-book "kestrel/lists-light/revappend" :dir :system))

in-theory

(in-theory (disable strip-cars))

consp-of-strip-carstheorem

(defthm consp-of-strip-cars
  (equal (consp (strip-cars x)) (consp x))
  :hints (("Goal" :in-theory (enable strip-cars))))

len-of-strip-carstheorem

(defthm len-of-strip-cars
  (equal (len (strip-cars x)) (len x))
  :hints (("Goal" :in-theory (enable strip-cars))))

strip-cars-of-constheorem

(defthm strip-cars-of-cons
  (equal (strip-cars (cons a x))
    (cons (car a) (strip-cars x)))
  :hints (("Goal" :in-theory (enable strip-cars))))

strip-cars-of-aconstheorem

(defthm strip-cars-of-acons
  (equal (strip-cars (acons key datum alist))
    (cons key (strip-cars alist)))
  :hints (("Goal" :in-theory (enable strip-cars))))

car-of-strip-carstheorem

(defthm car-of-strip-cars
  (equal (car (strip-cars x)) (car (car x)))
  :hints (("Goal" :in-theory (enable strip-cars))))

cadr-of-strip-carstheorem

(defthm cadr-of-strip-cars
  (equal (cadr (strip-cars x)) (car (cadr x)))
  :hints (("Goal" :in-theory (enable strip-cars))))

nth-of-strip-carstheorem

(defthm nth-of-strip-cars
  (equal (nth n (strip-cars x)) (car (nth n x)))
  :hints (("Goal" :in-theory (enable nth strip-cars))))

strip-cars-of-appendtheorem

(defthm strip-cars-of-append
  (equal (strip-cars (append x y))
    (append (strip-cars x) (strip-cars y)))
  :hints (("Goal" :in-theory (enable strip-cars))))

strip-cars-when-not-consp-cheaptheorem

(defthm strip-cars-when-not-consp-cheap
  (implies (not (consp x)) (equal (strip-cars x) nil))
  :rule-classes ((:rewrite :backchain-limit-lst (0)))
  :hints (("Goal" :in-theory (enable strip-cars))))

strip-cars-of-cdrtheorem

(defthmd strip-cars-of-cdr
  (equal (strip-cars (cdr x)) (cdr (strip-cars x)))
  :hints (("Goal" :in-theory (enable strip-cars))))

other

(theory-invariant (incompatible (:rewrite strip-cars-of-cdr)
    (:definition strip-cars)))

member-equal-of-strip-cars-ifftheorem

(defthmd member-equal-of-strip-cars-iff
  (implies (or (alistp alist) key)
    (iff (member-equal key (strip-cars alist))
      (assoc-equal key alist)))
  :hints (("Goal" :in-theory (enable assoc-equal member-equal strip-cars))))

strip-cars-of-pairlis$theorem

(defthm strip-cars-of-pairlis$
  (equal (strip-cars (pairlis$ x y)) (true-list-fix x))
  :hints (("Goal" :in-theory (enable strip-cars))))

strip-cars-of-revappendtheorem

(defthm strip-cars-of-revappend
  (equal (strip-cars (revappend x y))
    (revappend (strip-cars x) (strip-cars y)))
  :hints (("Goal" :in-theory (enable strip-cars
       revappend
       append-of-revappend-of-nil-arg1))))

strip-cars-of-reversetheorem

(defthm strip-cars-of-reverse
  (equal (strip-cars (reverse x)) (reverse (strip-cars x)))
  :hints (("Goal" :in-theory (enable reverse))))

strip-cars-ifftheorem

(defthm strip-cars-iff
  (iff (strip-cars alist) (consp alist))
  :hints (("Goal" :in-theory (enable strip-cars))))

<=-of-acl2-count-of-strip-cars-lineartheorem

(defthm <=-of-acl2-count-of-strip-cars-linear
  (<= (acl2-count (strip-cars x)) (acl2-count x))
  :rule-classes :linear :hints (("Goal" :in-theory (enable strip-cars))))

Included Books