cons-size

other

(in-package "ACL2")

include-book

(include-book "std/lists/top" :dir :system)

include-book

(include-book "std/alists/top" :dir :system)

include-book

(include-book "std/strings/top" :dir :system)

include-book

(include-book "acl2s/defdata/records" :dir :system)

cons-sizefunction

(defun cons-size
  (x)
  (declare (xargs :guard t))
  (if (consp x)
    (+ 1 (cons-size (car x)) (cons-size (cdr x)))
    0))

tree-sizemacro

(defmacro tree-size (x) `(cons-size ,X))

cons-size-typetheorem

(defthm cons-size-type
  (natp (cons-size x))
  :rule-classes ((:type-prescription) (:forward-chaining :trigger-terms ((cons-size x)))))

acons-cons-size-lemmatheorem

(defthm acons-cons-size-lemma
  (= (cons-size (acons x1 x2 x3))
    (+ 2 (cons-size x1) (cons-size x2) (cons-size x3)))
  :rule-classes ((:linear) (:rewrite)))

split-list-1-cons-sizetheorem

(defthm split-list-1-cons-size
  (implies (consp x)
    (< (cons-size (mv-nth 1 (split-list-1 x del)))
      (cons-size x)))
  :hints (("Goal" :in-theory (enable split-list-1)))
  :rule-classes :linear)

head-cons-sizetheorem

(defthm head-cons-size
  (implies (not (emptyp x))
    (< (cons-size (head x)) (cons-size x)))
  :hints (("Goal" :in-theory (enable emptyp head)))
  :rule-classes :linear)

tail-cons-sizetheorem

(defthm tail-cons-size
  (implies (not (emptyp x))
    (< (cons-size (tail x)) (cons-size x)))
  :hints (("Goal" :in-theory (enable emptyp tail)))
  :rule-classes :linear)

cons-size-appendtheorem

(defthm cons-size-append
  (= (cons-size (append x y)) (+ (cons-size x) (cons-size y)))
  :rule-classes ((:linear) (:rewrite)))

rev-cons-size-lemmatheorem

(defthm rev-cons-size-lemma
  (= (cons-size (rev x)) (cons-size x))
  :hints (("Goal" :in-theory (enable rev)))
  :rule-classes ((:linear) (:rewrite)))

cons-size-evens-strongtheorem

(defthm cons-size-evens-strong
  (implies (and (consp x) (consp (cdr x)))
    (< (cons-size (evens x)) (cons-size x)))
  :rule-classes :linear)

cons-size-evens-weaktheorem

(defthm cons-size-evens-weak
  (<= (cons-size (evens x)) (cons-size x))
  :hints (("Goal" :induct (evens x)))
  :rule-classes :linear)

cons-size-of-remove-assoc-equal-upper-boundtheorem

(defthm cons-size-of-remove-assoc-equal-upper-bound
  (<= (cons-size (remove-assoc-equal a x)) (cons-size x))
  :hints (("Goal" :in-theory (enable remove-assoc-equal)))
  :rule-classes :linear)

cons-size-when-membertheorem

(defthm cons-size-when-member
  (implies (member-equal a x) (< (cons-size a) (cons-size x)))
  :hints (("Goal" :in-theory (enable member-equal)))
  :rule-classes :linear)

cons-size-of-remove-duplicatestheorem

(defthm cons-size-of-remove-duplicates
  (<= (cons-size (remove-duplicates-equal x)) (cons-size x))
  :rule-classes :linear)

cons-size-of-hons-remove-duplicatestheorem

(defthm cons-size-of-hons-remove-duplicates
  (<= (cons-size (hons-remove-duplicates x)) (cons-size x))
  :hints (("Goal" :in-theory (enable hons-remove-duplicates)))
  :rule-classes :linear)

cons-size-of-nthcdr-lineartheorem

(defthm cons-size-of-nthcdr-linear
  (implies (and (not (zp n)) (consp x))
    (< (cons-size (nthcdr n x)) (cons-size x)))
  :hints (("Goal" :in-theory (enable nthcdr)))
  :rule-classes :linear)

cons-size-of-nthcdr-linear-weaktheorem

(defthm cons-size-of-nthcdr-linear-weak
  (<= (cons-size (nthcdr n x)) (cons-size x))
  :hints (("Goal" :in-theory (enable nthcdr)))
  :rule-classes :linear)

cons-size-of-nth-linear-weaktheorem

(defthm cons-size-of-nth-linear-weak
  (<= (cons-size (nth i x)) (cons-size x))
  :rule-classes :linear)

cons-size-of-nth-lineartheorem

(defthm cons-size-of-nth-linear
  (implies (consp x) (< (cons-size (nth i x)) (cons-size x)))
  :rule-classes :linear)

cons-size-of-prod-cons1theorem

(defthm cons-size-of-prod-cons1
  (<= (cons-size y)
    (cons-size (prod-cons x y)))
  :rule-classes :linear)

cons-size-of-prod-cons2theorem

(defthm cons-size-of-prod-cons2
  (<= (cons-size x)
    (cons-size (prod-cons x y)))
  :rule-classes :linear)

records-cons-size-linear-arith-<=theorem

(defthm records-cons-size-linear-arith-<=
  (<= (cons-size (mget k r)) (cons-size r))
  :hints (("goal" :in-theory (enable mget
       recordp
       no-nil-val-alistp
       ordered-unique-key-alistp)))
  :rule-classes :linear)

records-cons-size-linear-arith-<theorem

(defthm records-cons-size-linear-arith-<
  (implies (mget k r)
    (< (cons-size (mget k r)) (cons-size r)))
  :hints (("goal" :in-theory (enable mget
       recordp
       no-nil-val-alistp
       ordered-unique-key-alistp)))
  :rule-classes :linear)

records-cons-sizetheorem

(defthm records-cons-size
  (implies (consp r) (< (cons-size (mget k r)) (cons-size r)))
  :hints (("goal" :in-theory (enable mget
       recordp
       no-nil-val-alistp
       ordered-unique-key-alistp)))
  :rule-classes :linear)

len-<=-cons-sizetheorem

(defthm len-<=-cons-size
  (<= (len x) (cons-size x))
  :rule-classes :linear)

cons-size-<=-acl2-counttheorem

(defthm cons-size-<=-acl2-count
  (<= (cons-size x) (acl2-count x))
  :rule-classes :linear)

acl2-sizefunction

(defun acl2-size
  (x)
  (declare (xargs :guard t
      :measure (if (and (not (rationalp x)) (complex/complex-rationalp x))
        1
        (* 2 (cons-size x)))))
  (if (consp x)
    (+ 1 (acl2-size (car x)) (acl2-size (cdr x)))
    (if (rationalp x)
      (if (integerp x)
        (integer-abs x)
        (+ (integer-abs (numerator x)) (denominator x)))
      (if (complex/complex-rationalp x)
        (+ 1 (acl2-size (realpart x)) (acl2-size (imagpart x)))
        (if (stringp x)
          (length x)
          0)))))

Included Books