append

other

(in-package "ACL2")

local

(local (include-book "cons"))

local

(local (include-book "take"))

local

(local (include-book "nthcdr"))

local

(local (include-book "true-list-fix"))

in-theory

(in-theory (disable append))

car-of-appendtheorem

(defthm car-of-append
  (equal (car (append x y))
    (if (consp x)
      (car x)
      (car y)))
  :hints (("Goal" :in-theory (enable append))))

cdr-of-appendtheorem

(defthm cdr-of-append
  (equal (cdr (append x y))
    (if (consp x)
      (append (cdr x) y)
      (cdr y)))
  :hints (("Goal" :in-theory (enable append))))

len-of-appendtheorem

(defthm len-of-append
  (equal (len (append x y)) (+ (len x) (len y)))
  :hints (("Goal" :in-theory (enable append))))

append-of-nil-arg1theorem

(defthm append-of-nil-arg1
  (equal (append nil y) y)
  :hints (("Goal" :in-theory (enable append))))

append-when-not-consp-arg1theorem

(defthmd append-when-not-consp-arg1
  (implies (not (consp x)) (equal (append x y) y))
  :hints (("Goal" :in-theory (enable append))))

append-when-not-consp-arg1-cheaptheorem

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

append-of-nil-arg2theorem

(defthm append-of-nil-arg2
  (equal (append x nil) (true-list-fix x))
  :hints (("Goal" :in-theory (enable append))))

true-listp-of-appendtheorem

(defthm true-listp-of-append
  (equal (true-listp (append x y)) (true-listp y))
  :hints (("Goal" :in-theory (enable append))))

append-associativetheorem

(defthm append-associative
  (equal (append (append x y) z) (append x y z))
  :hints (("Goal" :in-theory (enable append))))

consp-of-appendtheorem

(defthm consp-of-append
  (equal (consp (append x y)) (or (consp x) (consp y)))
  :hints (("Goal" :in-theory (enable append))))

append-of-cons-arg1theorem

(defthm append-of-cons-arg1
  (equal (append (cons a x) y) (cons a (append x y)))
  :hints (("Goal" :in-theory (enable append))))

true-list-fix-of-appendtheorem

(defthm true-list-fix-of-append
  (equal (true-list-fix (append x y))
    (append x (true-list-fix y)))
  :hints (("Goal" :in-theory (enable append))))

append-ifftheorem

(defthm append-iff
  (iff (append x y) (or (consp x) y))
  :hints (("Goal" :in-theory (enable append))))

local

(local (defthmd not-equal-when-lens-not-equal
    (implies (not (equal (len x) (len y))) (not (equal x y)))))

equal-of-append-same-arg1-when-true-listptheorem

(defthm equal-of-append-same-arg1-when-true-listp
  (implies (true-listp x)
    (equal (equal x (append x y)) (equal y nil)))
  :hints (("Goal" :in-theory (enable append))))

equal-of-append-same-arg2theorem

(defthm equal-of-append-same-arg2
  (equal (equal y (append x y)) (not (consp x)))
  :hints (("Goal" :expand (append x y)
     :in-theory (enable not-equal-when-lens-not-equal))))

equal-of-append-and-append-same-arg1theorem

(defthm equal-of-append-and-append-same-arg1
  (equal (equal (append x y) (append x z)) (equal y z))
  :hints (("Goal" :in-theory (enable append))))

nthcdr-of-len-and-appendtheorem

(defthm nthcdr-of-len-and-append
  (equal (nthcdr (len x) (append x y)) y)
  :hints (("Goal" :in-theory (enable append nthcdr))))

take-of-len-and-appendtheorem

(defthm take-of-len-and-append
  (equal (take (len x) (append x y)) (true-list-fix x))
  :hints (("Goal" :in-theory (enable append))))

append-of-true-list-fix-arg1theorem

(defthm append-of-true-list-fix-arg1
  (equal (append (true-list-fix x) y) (append x y))
  :hints (("Goal" :in-theory (enable true-list-fix))))

equal-of-appendtheorem

(defthmd equal-of-append
  (equal (equal x (append y z))
    (and (<= (len y) (len x))
      (equal (take (len y) x) (true-list-fix y))
      (equal (nthcdr (len y) x) z)))
  :hints (("Goal" :use ((:instance append-of-true-list-fix-arg1
        (x y)
        (y (nthcdr (len y) x))))
     :in-theory (disable append-of-true-list-fix-arg1))))

equal-of-append-and-append-when-equal-of-len-and-lentheorem

(defthm equal-of-append-and-append-when-equal-of-len-and-len
  (implies (equal (len x1) (len x2))
    (equal (equal (append x1 y1) (append x2 y2))
      (and (equal (true-list-fix x1) (true-list-fix x2))
        (equal y1 y2))))
  :hints (("Goal" :in-theory (enable equal-of-append))))

last-of-appendtheorem

(defthm last-of-append
  (equal (last (append x y))
    (if (consp y)
      (last y)
      (append (last x) y)))
  :hints (("Goal" :in-theory (enable last append))))

equal-of-append-and-append-same-arg2theorem

(defthm equal-of-append-and-append-same-arg2
  (equal (equal (append x1 y) (append x2 y))
    (equal (true-list-fix x1) (true-list-fix x2)))
  :hints (("Goal" :in-theory (enable equal-of-append
       equal-of-true-list-fix-and-true-list-fix-forward))))

<=-of-acl2-count-of-append-lineartheorem

(defthm <=-of-acl2-count-of-append-linear
  (<= (acl2-count (append x y))
    (+ (acl2-count x) (acl2-count y)))
  :rule-classes :linear :hints (("Goal" :in-theory (enable append))))

acl2-count-of-append-of-constheorem

(defthm acl2-count-of-append-of-cons
  (equal (acl2-count (append (cons x y) z))
    (acl2-count (cons x (append y z)))))

acl2-count-of-append-of-cons-lineartheorem

(defthm acl2-count-of-append-of-cons-linear
  (equal (acl2-count (append (cons x y) z))
    (acl2-count (cons x (append y z))))
  :rule-classes :linear)

Included Books