last

(in-package "ACL2")

(defsection std/lists/last
  :parents (std/lists last)
  :short "Lemmas about @(see last) available in the @(see std/lists) library."
  (defthm last-when-atom
    (implies (atom x) (equal (last x) x)))
  (defthm last-when-atom-of-cdr
    (implies (atom (cdr x)) (equal (last x) x)))
  (defthm last-of-cons
    (equal (last (cons a x))
      (if (consp x)
        (last x)
        (cons a x))))
  (defthm consp-of-last (equal (consp (last l)) (consp l)))
  (defthm true-listp-of-last
    (equal (true-listp (last l)) (true-listp l)))
  (defthm last-of-list-fix
    (equal (last (list-fix x)) (list-fix (last x))))
  (defthm len-of-last
    (equal (len (last l))
      (if (consp l)
        1
        0)))
  (defthm upper-bound-of-len-of-last
    (< (len (last x)) 2)
    :rule-classes :linear)
  (defthm member-of-car-of-last
    (iff (member (car (last x)) x)
      (if (consp x)
        t
        nil)))
  (defsection subsetp-of-last
    (local (defthm l0
        (implies (subsetp-equal a x) (subsetp-equal a (cons b x)))))
    (defthm subsetp-of-last (subsetp (last x) x)))
  (defthm last-of-append
    (equal (last (append x y))
      (if (consp y)
        (last y)
        (append (last x) y))))
  (defthm last-of-rev
    (equal (last (rev x))
      (if (consp x)
        (list (car x))
        nil)))
  (defthm last-of-revappend
    (equal (last (revappend x y))
      (cond ((consp y) (last y))
        ((consp x) (cons (car x) y))
        (t y))))
  (def-listp-rule element-list-p-of-last
    (implies (element-list-p (double-rewrite x))
      (element-list-p (last x)))))