butlast

other

(in-package "ACL2")

local

(local (include-book "take"))

in-theory

(in-theory (disable butlast))

consp-of-butlasttheorem

(defthm consp-of-butlast
  (equal (consp (butlast lst n)) (< (nfix n) (len lst)))
  :hints (("Goal" :in-theory (enable butlast))))

car-of-butlasttheorem

(defthm car-of-butlast
  (equal (car (butlast lst n))
    (if (< (nfix n) (len lst))
      (car lst)
      nil))
  :hints (("Goal" :in-theory (enable butlast))))

butlast-of-constheorem

(defthm butlast-of-cons
  (equal (butlast (cons a lst) n)
    (if (<= (nfix n) (len lst))
      (cons a (butlast lst n))
      nil))
  :hints (("Goal" :in-theory (enable butlast))))

cdr-of-butlasttheorem

(defthm cdr-of-butlast
  (equal (cdr (butlast lst n)) (butlast (cdr lst) n))
  :hints (("Goal" :expand (len (cdr lst)) :in-theory (enable butlast))))

butlast-of-niltheorem

(defthm butlast-of-nil
  (equal (butlast nil n) nil)
  :hints (("Goal" :in-theory (enable butlast))))

Included Books