len - ACL2 Book

other

(in-package "ACL2")

in-theory

(in-theory (disable len))

len-of-constheorem

(defthm len-of-cons
  (equal (len (cons a x)) (+ 1 (len x)))
  :hints (("Goal" :in-theory (enable len))))

len-when-not-consp-cheaptheorem

(defthm len-when-not-consp-cheap
  (implies (not (consp x)) (equal (len x) 0))
  :rule-classes ((:rewrite :backchain-limit-lst (0)))
  :hints (("Goal" :in-theory (enable len))))

consp-when-len-greatertheorem

(defthm consp-when-len-greater
  (implies (and (< n (len x)) (natp n)) (consp x)))

equal-of-len-and-0theorem

(defthm equal-of-len-and-0
  (equal (equal 0 (len x)) (not (consp x)))
  :hints (("Goal" :in-theory (enable len))))

len-of-cdr-lineartheorem

(defthm len-of-cdr-linear
  (<= (len (cdr x)) (len x))
  :rule-classes :linear)

len-of-cdr-linear-strongtheorem

(defthm len-of-cdr-linear-strong
  (implies (consp x) (= (len (cdr x)) (+ -1 (len x))))
  :rule-classes :linear)

len-positive-when-consp-linear-cheaptheorem

(defthm len-positive-when-consp-linear-cheap
  (implies (consp x) (< 0 (len x)))
  :rule-classes ((:linear :backchain-limit-lst (0)))
  :hints (("Goal" :in-theory (enable len))))

consp-forward-to-len-boundtheorem

(defthm consp-forward-to-len-bound
  (implies (consp x) (< 0 (len x)))
  :rule-classes :forward-chaining)

<-of-0-and-len-forward-to-consptheorem

(defthm <-of-0-and-len-forward-to-consp
  (implies (< 0 (len x)) (consp x))
  :rule-classes :forward-chaining)

not-consp-of-cdr-forward-to-len-boundtheorem

(defthm not-consp-of-cdr-forward-to-len-bound
  (implies (not (consp (cdr x))) (<= (len x) 1))
  :rule-classes :forward-chaining)

len-of-cdrtheorem

(defthm len-of-cdr
  (equal (len (cdr x))
    (if (equal 0 (len x))
      0
      (+ -1 (len x)))))

other

(theory-invariant (incompatible (:rewrite len-of-cdr) (:definition len)))

consp-of-cdrtheorem

(defthmd consp-of-cdr
  (equal (consp (cdr x)) (< 1 (len x)))
  :hints (("Goal" :in-theory (e/d (len) (len-of-cdr)))))

<-of-1-and-len-when-true-listptheorem

(defthmd <-of-1-and-len-when-true-listp
  (implies (true-listp x) (iff (< 1 (len x)) (cdr x)))
  :hints (("Goal" :in-theory (e/d (len) (len-of-cdr)))))

consp-to-len-boundtheorem

(defthmd consp-to-len-bound
  (equal (consp x) (< 0 (len x)))
  :hints (("Goal" :in-theory (e/d (len) (len-of-cdr)))))

<-of-0-and-lentheorem

(defthmd <-of-0-and-len
  (equal (< 0 (len x)) (consp x))
  :hints (("Goal" :in-theory (e/d (len) (len-of-cdr)))))

consp-of-cdr-when-len-knowntheorem

(defthm consp-of-cdr-when-len-known
  (implies (and (equal (len x) k) (syntaxp (quotep k)))
    (equal (consp (cdr x)) (< 1 k)))
  :hints (("Goal" :in-theory (enable consp-of-cdr))))

consp-from-lentheorem

(defthmd consp-from-len (implies (< 0 (len x)) (consp x)))

consp-from-len-cheaptheorem

(defthm consp-from-len-cheap
  (implies (< 0 (len x)) (consp x))
  :rule-classes ((:rewrite :backchain-limit-lst (1))))

<-of-len-and-2-casestheorem

(defthmd <-of-len-and-2-cases
  (equal (< (len x) 2) (or (not (consp x)) (equal 1 (len x)))))

equal-of-len-and-1theorem

(defthmd equal-of-len-and-1
  (implies (true-listp x)
    (equal (equal 1 (len x)) (equal x (list (car x))))))

len-of-cddr-when-equal-of-lentheorem

(defthm len-of-cddr-when-equal-of-len
  (implies (and (equal (len x) k) (syntaxp (quotep k)) (<= 2 k))
    (equal (len (cddr x)) (+ -2 k))))

consp-when-len-equal-constanttheorem

(defthm consp-when-len-equal-constant
  (implies (and (equal (len x) free) (syntaxp (quotep free)))
    (equal (consp x) (< 0 free)))
  :hints (("Goal" :in-theory (e/d (len) (len-of-cdr)))))