butlast

(in-package "ACL2")

(defsection std/lists/butlast
  :parents (std/lists butlast)
  :short "Lemmas about @(see butlast) available in the @(see std/lists)
  library."
  "<p>The usual definition of @('butlast') is in terms of @(see take).  But
  it's often more convenient to reason about @('butlast') directly.  In that
  case, its recursive redefinition may be what you want:</p>"
  (defthm butlast-redefinition
    (equal (butlast x n)
      (if (>= (nfix n) (len x))
        nil
        (cons (car x) (butlast (cdr x) n))))
    :rule-classes ((:definition :clique (butlast)
       :controller-alist ((butlast t t)))))
  (defun butlast-induction
    (x n)
    (if (>= (nfix n) (len x))
      nil
      (cons (car x) (butlast-induction (cdr x) n))))
  (defthm use-butlast-induction
    t
    :rule-classes ((:induction :pattern (butlast x n)
       :scheme (butlast-induction x n))))
  "<p>For use with @(see std::deflist):</p>"
  (def-listp-rule element-list-p-of-butlast
    (implies (element-list-p (double-rewrite x))
      (element-list-p (butlast x n)))))