take - ACL2 Book

other

(in-package "ACL2")

in-theory

(in-theory (disable take))

consp-of-taketheorem

(defthm consp-of-take
  (equal (consp (take n xs)) (not (zp n)))
  :hints (("Goal" :in-theory (enable take))))

car-of-take-strongtheorem

(defthm car-of-take-strong
  (equal (car (take n l))
    (if (zp n)
      nil
      (car l)))
  :hints (("Goal" :expand ((first-n-ac n l nil))
     :in-theory (enable take))))

take-of-constheorem

(defthm take-of-cons
  (equal (take n (cons a x))
    (if (zp n)
      nil
      (cons a (take (+ -1 n) x))))
  :hints (("Goal" :in-theory (enable take))))

take-of-0theorem

(defthm take-of-0
  (equal (take 0 l) nil)
  :hints (("Goal" :in-theory (enable take))))

take-when-zptheorem

(defthmd take-when-zp
  (implies (zp n) (equal (take n l) nil))
  :hints (("Goal" :in-theory (enable take))))

take-of-1theorem

(defthm take-of-1
  (equal (take 1 x) (list (car x)))
  :hints (("Goal" :in-theory (enable take))))

cdr-of-taketheorem

(defthm cdr-of-take
  (equal (cdr (take n l)) (take (+ -1 n) (cdr l)))
  :hints (("Goal" :expand (first-n-ac n l nil)
     :in-theory (enable take))))

len-of-taketheorem

(defthm len-of-take
  (equal (len (take n xs)) (nfix n))
  :hints (("Goal" :in-theory (enable take))))

nth-of-take-2theorem

(defthm nth-of-take-2
  (implies (and (natp n) (natp m))
    (equal (nth n (take m lst))
      (if (< n m)
        (nth n lst)
        nil)))
  :hints (("Goal" :in-theory (enable take nth))))

nth-of-take-2-gentheorem

(defthm nth-of-take-2-gen
  (equal (nth n (take m lst))
    (if (natp n)
      (if (natp m)
        (if (< n m)
          (nth n lst)
          nil)
        nil)
      (if (zp m)
        nil
        (car lst))))
  :hints (("Goal" :use nth-of-take-2
     :expand (take m lst)
     :in-theory (disable nth-of-take-2))))

nth-of-take-too-hightheorem

(defthm nth-of-take-too-high
  (implies (and (<= m n) (natp n) (< 0 m))
    (equal (nth n (take m data)) nil)))

nthcdr-of-taketheorem

(defthm nthcdr-of-take
  (equal (nthcdr i (take j x))
    (take (- (nfix j) (nfix i)) (nthcdr i x)))
  :hints (("Goal" :in-theory (enable take nthcdr))))

take-of-nthcdrtheorem

(defthmd take-of-nthcdr
  (implies (and (integerp i) (<= 0 i) (integerp k))
    (equal (take k (nthcdr i x)) (nthcdr i (take (+ i k) x))))
  :hints (("Goal" :in-theory (e/d (take) (nthcdr-of-take))
     :use (:instance nthcdr-of-take (j (+ i k))))))

other

(theory-invariant (incompatible (:rewrite nthcdr-of-take)
    (:rewrite take-of-nthcdr)))

take-does-nothingtheorem

(defthm take-does-nothing
  (implies (equal n (len lst))
    (equal (take n lst) (true-list-fix lst)))
  :hints (("Goal" :in-theory (enable take))))

take-does-nothing-simpletheorem

(defthmd take-does-nothing-simple
  (implies (and (equal n (len l)) (true-listp l))
    (equal (take n l) l))
  :hints (("Goal" :in-theory (enable take))))

take-ifftheorem

(defthm take-iff
  (iff (take n lst) (and (natp n) (< 0 n)))
  :hints (("Goal" :in-theory (enable take))))

take-of-true-list-fixtheorem

(defthm take-of-true-list-fix
  (equal (take n (true-list-fix lst)) (take n lst))
  :hints (("Goal" :in-theory (enable take))))

take-of-take-when-<=theorem

(defthm take-of-take-when-<=
  (implies (and (<= n m) (integerp n) (natp m))
    (equal (take n (take m lst)) (take n lst)))
  :hints (("Goal" :in-theory (enable take))))

take-of-cdrtheorem

(defthmd take-of-cdr
  (equal (take n (cdr lst)) (cdr (take (+ 1 n) lst)))
  :hints (("Goal" :in-theory (enable take))))

cdr-take-plus-1theorem

(defthmd cdr-take-plus-1
  (equal (cdr (take (+ 1 n) vals)) (take n (cdr vals)))
  :hints (("Goal" :in-theory (enable take))))

other

(theory-invariant (incompatible (:rewrite take-of-cdr)
    (:rewrite cdr-take-plus-1)))

other

(theory-invariant (incompatible (:rewrite take-of-cdr) (:rewrite cdr-of-take)))

local

(local (defthm subsetp-equal-of-cons-arg2
    (implies (and (syntaxp (not (and (quotep a) (quotep y))))
        (subsetp-equal x y))
      (subsetp-equal x (cons a y)))
    :hints (("Goal" :in-theory (enable subsetp-equal)))))

subsetp-equal-of-take-and-taketheorem

(defthm subsetp-equal-of-take-and-take
  (implies (<= n1 n2)
    (equal (subsetp-equal (take n1 lst) (take n2 lst))
      (if (natp n2)
        t
        (zp n1))))
  :hints (("Goal" :in-theory (enable take))))

take-of-appendtheorem

(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))))
  :hints (("Goal" :in-theory (enable take append true-list-fix))))

take-of-update-nththeorem

(defthm take-of-update-nth
  (equal (take n1 (update-nth n2 val x))
    (if (<= (nfix n1) (nfix n2))
      (take n1 x)
      (update-nth n2 val (take n1 x))))
  :hints (("Goal" :in-theory (enable take update-nth))))

local

(local (defthm nthcdr-of-nil
    (equal (nthcdr n nil) nil)
    :hints (("Goal" :in-theory (enable nthcdr)))))

append-of-take-and-nthcdr-2theorem

(defthm append-of-take-and-nthcdr-2
  (equal (append (take n l) (nthcdr n l))
    (if (<= (nfix n) (len l))
      l
      (take n l)))
  :hints (("Goal" :in-theory (enable take nthcdr))))

cadr-of-taketheorem

(defthm cadr-of-take
  (equal (cadr (take n lst))
    (if (not (and (integerp n) (< 1 n)))
      nil
      (cadr lst)))
  :hints (("Goal" :in-theory (enable take))))

take-does-nothing-rewritetheorem

(defthm take-does-nothing-rewrite
  (implies (natp n)
    (equal (equal x (take n x))
      (and (true-listp x) (equal (len x) n)))))

equal-of-take-and-take-sametheorem

(defthm equal-of-take-and-take-same
  (equal (equal (take n1 x) (take n2 x))
    (equal (nfix n1) (nfix n2)))
  :hints (("Goal" :in-theory (enable take))))

take-opener-when-not-zptheorem

(defthmd take-opener-when-not-zp
  (implies (not (zp n))
    (equal (take n lst)
      (cons (nth 0 lst) (take (+ -1 n) (cdr lst)))))
  :hints (("Goal" :in-theory (enable take))))

take-of-+-of-1theorem

(defthmd take-of-+-of-1
  (implies (and (syntaxp (not (quotep n))) (natp n))
    (equal (take (+ 1 n) x) (cons (car x) (take n (cdr x)))))
  :hints (("Goal" :in-theory (enable take append))))

take-of-+-of-1-alttheorem

(defthmd take-of-+-of-1-alt
  (implies (and (syntaxp (not (quotep n))) (< n (len x)) (natp n))
    (equal (take (+ 1 n) x)
      (append (take n x) (list (nth n x)))))
  :hints (("Goal" :in-theory (enable take append))))

update-nth-take-last-elementtheorem

(defthm update-nth-take-last-element
  (implies (and (< n (len lst)) (integerp n))
    (equal (update-nth n val (take (+ 1 n) lst))
      (append (take n lst) (list val))))
  :hints (("Goal" :in-theory (enable take))))

<-of-acl2-count-of-taketheorem

(defthm <-of-acl2-count-of-take
  (implies (true-listp l)
    (equal (< (acl2-count l) (acl2-count (take n l)))
      (and (< (len l) n) (natp n))))
  :hints (("Goal" :in-theory (enable take)) ("subgoal *1/1" :cases ((< (+ 1 (len (cdr l))) n)))))

<=-of-acl2-count-of-take-lineartheorem

(defthm <=-of-acl2-count-of-take-linear
  (implies (<= n (len l))
    (<= (acl2-count (take n l)) (acl2-count l)))
  :rule-classes ((:linear :trigger-terms ((acl2-count (take n l)))))
  :hints (("Goal" :in-theory (enable take))))

<-of-acl2-count-of-take-lineartheorem

(defthm <-of-acl2-count-of-take-linear
  (implies (< (nfix n) (len l))
    (< (acl2-count (take n l)) (acl2-count l)))
  :rule-classes ((:linear :trigger-terms ((acl2-count (take n l)))))
  :hints (("Goal" :in-theory (enable take))))

nth-when-equal-of-take-and-constanttheorem

(defthm nth-when-equal-of-take-and-constant
  (implies (and (equal k (take m x))
      (syntaxp (and (quotep k) (not (quotep x))))
      (< n m)
      (natp n)
      (natp m))
    (equal (nth n x) (nth n k))))

take-opener-alttheorem

(defthmd take-opener-alt
  (implies (posp n)
    (equal (take n x)
      (append (take (+ -1 n) x) (list (nth (+ -1 n) x)))))
  :hints (("Goal" :in-theory (enable take))))

take-when-most-knowntheorem

(defthmd take-when-most-known
  (implies (and (equal (take (+ -1 n) x) free) (posp n))
    (equal (take n x) (append free (list (nth (+ -1 n) x)))))
  :hints (("Goal" :in-theory (enable take-opener-alt))))