acl2-count - ACL2 Book

other

(in-package "ACL2")

acl2-count-of-cartheorem

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

acl2-count-of-cdrtheorem

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

acl2-count-of-sumtheorem

(defthm acl2-count-of-sum
  (and (implies (consp x)
      (< (+ (acl2-count (car x)) (acl2-count (cdr x)))
        (acl2-count x)))
    (<= (+ (acl2-count (car x)) (acl2-count (cdr x)))
      (acl2-count x)))
  :hints (("Goal" :in-theory (enable acl2-count)))
  :rule-classes :linear)

acl2-count-of-consp-positivetheorem

(defthm acl2-count-of-consp-positive
  (implies (consp x) (< 0 (acl2-count x)))
  :rule-classes (:type-prescription :linear))

acl2-count-of-cons-greatertheorem

(defthm acl2-count-of-cons-greater
  (> (acl2-count (cons a b))
    (+ (acl2-count a) (acl2-count b)))
  :rule-classes :linear)