		Search-engine friendly clone of the ACL2 documentation.

Std/lists/take

Lemmas about take available in the std/lists library.

Definitions and Theorems

Theorem: consp-of-take

(defthm consp-of-take
  (equal (consp (take n xs))
         (not (zp n))))

Theorem: take-under-iff

(defthm take-under-iff
  (iff (take n xs) (not (zp n))))

Theorem: len-of-take

(defthm len-of-take
  (equal (len (take n xs)) (nfix n)))

Theorem: take-of-cons

(defthm take-of-cons
  (equal (take n (cons a x))
         (if (zp n)
             nil
           (cons a (take (1- n) x)))))

Theorem: take-of-append

(defthm take-of-append
  (equal (take n (append x y))
         (if (< (nfix n) (len x))
             (take n x)
           (append x (take (- n (len x)) y)))))

Theorem: take-of-zero

(defthm take-of-zero
  (equal (take 0 x) nil))

Theorem: take-of-1

(defthm take-of-1
  (equal (take 1 x) (list (car x))))

Theorem: car-of-take

(defthm car-of-take
  (implies (<= 1 (nfix n))
           (equal (car (take n x)) (car x))))

Theorem: second-of-take

(defthm second-of-take
  (implies (<= 2 (nfix n))
           (equal (second (take n x)) (second x))))

Theorem: third-of-take

(defthm third-of-take
  (implies (<= 3 (nfix n))
           (equal (third (take n x)) (third x))))

Theorem: fourth-of-take

(defthm fourth-of-take
  (implies (<= 4 (nfix n))
           (equal (fourth (take n x)) (fourth x))))

Theorem: take-of-len-free

(defthm take-of-len-free
  (implies (equal len (len x))
           (equal (take len x) (list-fix x))))

Theorem: equal-of-take-and-list-fix

(defthm equal-of-take-and-list-fix
  (equal (equal (take n x) (list-fix x))
         (equal (len x) (nfix n))))

Theorem: take-of-len

(defthm take-of-len
  (equal (take (len x) x) (list-fix x)))

Theorem: subsetp-of-take

(defthm subsetp-of-take
  (iff (subsetp (take n x) x)
       (or (<= (nfix n) (len x))
           (member-equal nil x))))

Theorem: take-fewer-of-take-more

(defthm take-fewer-of-take-more
  (implies (<= (nfix a) (nfix b))
           (equal (take a (take b x)) (take a x))))

Theorem: take-of-take-same

(defthm take-of-take-same
  (equal (take a (take a x)) (take a x)))

Theorem: no-duplicatesp-of-take

(defthm no-duplicatesp-of-take
  (implies (and (no-duplicatesp-equal l)
                (<= (nfix n) (len l)))
           (no-duplicatesp-equal (take n l))))

Theorem: take-as-append-and-nth

(defthm take-as-append-and-nth
  (equal (take n l)
         (if (zp n)
             nil
           (append (take (- n 1) l)
                   (list (nth (- n 1) l)))))
  :rule-classes ((:definition :install-body nil)))

Theorem: list-equiv-implies-equal-take-2

(defthm list-equiv-implies-equal-take-2
  (implies (list-equiv x x-equiv)
           (equal (take n x) (take n x-equiv)))
  :rule-classes (:congruence))

Theorem: list-equiv-implies-equal-butlast-1

(defthm list-equiv-implies-equal-butlast-1
  (implies (list-equiv lst lst-equiv)
           (equal (butlast lst n)
                  (butlast lst-equiv n)))
  :rule-classes (:congruence))

Theorem: element-list-p-of-take

(defthm element-list-p-of-take
  (implies (element-list-p (double-rewrite x))
           (iff (element-list-p (take n x))
                (or (element-p nil)
                    (<= (nfix n) (len x)))))
  :rule-classes :rewrite)

Theorem: elementlist-projection-of-take-nil-preserving

(defthm elementlist-projection-of-take-nil-preserving
  (implies (equal nil (element-xformer nil))
           (equal (elementlist-projection (take n x))
                  (take n (elementlist-projection x))))
  :rule-classes :rewrite)

Theorem: elementlist-projection-of-take

(defthm elementlist-projection-of-take
  (implies (<= (nfix n) (len x))
           (equal (elementlist-projection (take n x))
                  (take n (elementlist-projection x))))
  :rule-classes :rewrite)

Subtopics

Take-of-take-split: Aggressive case splitting rule to reduce (take a (take b x)).
Take-of-too-many: Rewrite (take n x) when n is more than (len x).