append

(in-package "ACL2")

(defsection std/lists/append
  :parents (std/lists append)
  :short "Lemmas about @(see append) available in the @(see std/lists)
library."
  (local (defthm len-when-consp
      (implies (consp x) (< 0 (len x)))
      :rule-classes ((:linear) (:rewrite))))
  (defthm append-when-not-consp
    (implies (not (consp x)) (equal (append x y) y)))
  (defthm append-of-cons
    (equal (append (cons a x) y) (cons a (append x y))))
  (defthm true-listp-of-append
    (equal (true-listp (append x y)) (true-listp y)))
  (defthm consp-of-append
    (equal (consp (append x y)) (or (consp x) (consp y))))
  (defthm append-under-iff
    (iff (append x y) (or (consp x) y)))
  (defthm len-of-append
    (equal (len (append x y)) (+ (len x) (len y))))
  (defthm equal-when-append-same
    (equal (equal (append x y1) (append x y2)) (equal y1 y2)))
  (local (defthm append-nonempty-list
      (implies (consp x) (not (equal (append x y) y)))
      :hints (("Goal" :use ((:instance len (x (append x y))) (:instance len (x y)))))))
  (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" :induct (cdr-cdr-induct x1 x2))))
  (defthm append-of-nil (equal (append x nil) (list-fix x)))
  (in-theory (disable append-to-nil))
  (defthm list-fix-of-append
    (equal (list-fix (append x y)) (append x (list-fix y))))
  (defthm car-of-append
    (equal (car (append x y))
      (if (consp x)
        (car x)
        (car y))))
  (defthmd car-of-append-when-consp
    (implies (consp x) (equal (car (append x y)) (car x))))
  (theory-invariant (incompatible (:rewrite car-of-append-when-consp)
      (:rewrite car-of-append))
    :key car-of-append-consp-invariant
    :error t)
  (defthmd cdr-of-append
    (equal (cdr (append x y))
      (if (consp x)
        (append (cdr x) y)
        (cdr y))))
  (defthm cdr-of-append-when-consp
    (implies (consp x)
      (equal (cdr (append x y)) (append (cdr x) y))))
  (theory-invariant (incompatible (:rewrite cdr-of-append-when-consp)
      (:rewrite cdr-of-append))
    :key cdr-of-append-consp-invariant
    :error t)
  (defthm associativity-of-append
    (equal (append (append a b) c) (append a (append b c))))
  (defcong element-list-equiv
    element-list-equiv
    (append a b)
    1)
  (table listfix-rules
    'element-list-equiv-implies-element-list-equiv-append-1
    t)
  (defcong element-list-equiv
    element-list-equiv
    (append a b)
    2)
  (table listfix-rules
    'element-list-equiv-implies-element-list-equiv-append-2
    t)
  (def-listp-rule element-list-p-of-append-true-list
    (equal (element-list-p (append a b))
      (and (element-list-p (list-fix a)) (element-list-p b)))
    :requirement true-listp
    :name element-list-p-of-append))