acl2-count - ACL2 Book

other

(in-package "ACL2")

<=-of-acl2-count-of-car-and-acl2-count-sametheorem

(defthm <=-of-acl2-count-of-car-and-acl2-count-same
  (<= (acl2-count (car x)) (acl2-count x)))

<=-of-acl2-count-of-car-and-acl2-count-same-lineartheorem

(defthm <=-of-acl2-count-of-car-and-acl2-count-same-linear
  (<= (acl2-count (car x)) (acl2-count x))
  :rule-classes ((:linear :trigger-terms ((acl2-count (car x))))))

<=-of-acl2-count-of-cdr-and-acl2-count-sametheorem

(defthm <=-of-acl2-count-of-cdr-and-acl2-count-same
  (<= (acl2-count (cdr x)) (acl2-count x)))

<=-of-acl2-count-of-cdr-and-acl2-count-same-lineartheorem

(defthm <=-of-acl2-count-of-cdr-and-acl2-count-same-linear
  (<= (acl2-count (cdr x)) (acl2-count x))
  :rule-classes ((:linear :trigger-terms ((acl2-count (cdr x))))))

acl2-count-car-chainingtheorem

(defthm acl2-count-car-chaining
  (implies (<= (acl2-count y) (acl2-count x))
    (<= (acl2-count (car y)) (acl2-count x)))
  :hints (("Goal" :in-theory (disable acl2-count))))

acl2-count-cdr-chainingtheorem

(defthm acl2-count-cdr-chaining
  (implies (<= (acl2-count y) (acl2-count x))
    (<= (acl2-count (cdr y)) (acl2-count x)))
  :hints (("Goal" :in-theory (disable acl2-count))))

<-of-0-and-acl2-count-when-consp-lineartheorem

(defthmd <-of-0-and-acl2-count-when-consp-linear
  (implies (consp x) (< 0 (acl2-count x)))
  :rule-classes :linear :hints (("Goal" :in-theory (enable acl2-count))))

acl2-count-of-constheorem

(defthm acl2-count-of-cons
  (equal (acl2-count (cons x y))
    (+ 1 (acl2-count x) (acl2-count y))))

<=-of-acl2-count-of-nthcdrtheorem

(defthmd <=-of-acl2-count-of-nthcdr
  (<= (acl2-count (nthcdr n lst)) (acl2-count lst))
  :hints (("Goal" :induct (nthcdr n lst) :in-theory (enable nthcdr))))

<=-of-acl2-count-of-nthcdr-lineartheorem

(defthm <=-of-acl2-count-of-nthcdr-linear
  (<= (acl2-count (nthcdr n lst)) (acl2-count lst))
  :rule-classes ((:linear :trigger-terms ((acl2-count (nthcdr n lst)))))
  :hints (("Goal" :by <=-of-acl2-count-of-nthcdr)))

<-of-acl2-count-of-nthcdrtheorem

(defthm <-of-acl2-count-of-nthcdr
  (implies (consp lst)
    (equal (< (acl2-count (nthcdr n lst)) (acl2-count lst))
      (and (< 0 n) (integerp n))))
  :hints (("Goal" :induct (nthcdr n lst) :in-theory (enable nthcdr)) ("subgoal *1/1" :cases ((< 0 n)))
    ("subgoal *1/2" :cases ((< 0 n)))))

<-of-acl2-count-of-nthcdr-lineartheorem

(defthm <-of-acl2-count-of-nthcdr-linear
  (implies (and (posp n) (consp lst))
    (< (acl2-count (nthcdr n lst)) (acl2-count lst)))
  :rule-classes ((:linear :trigger-terms ((acl2-count (nthcdr n lst))))))

<=-of-acl2-count-of-nththeorem

(defthm <=-of-acl2-count-of-nth
  (<= (acl2-count (nth n lst)) (acl2-count lst))
  :rule-classes (:rewrite (:linear :trigger-terms ((acl2-count (nth n lst)))))
  :hints (("Goal" :induct (nth n lst) :in-theory (enable nth))))

<-of-acl2-count-of-one-lesstheorem

(defthm <-of-acl2-count-of-one-less
  (implies (posp x) (< (acl2-count (+ -1 x)) (acl2-count x)))
  :hints (("Goal" :in-theory (enable acl2-count))))

acl2-count-hacktheorem

(defthmd acl2-count-hack
  (implies (<= (acl2-count x) y) (< (acl2-count x) (+ 1 y))))