• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Debugging
  • Projects
  • Std
    • Std/lists
      • Std/lists/abstract
      • Rev
      • Defsort
      • List-fix
      • Std/lists/nth
      • Hons-remove-duplicates
      • Std/lists/update-nth
      • Set-equiv
      • Duplicity
      • Prefixp
      • Std/lists/take
      • Std/lists/intersection$
      • Nats-equiv
      • Repeat
      • Index-of
      • All-equalp
      • Sublistp
      • Std/lists/nthcdr
      • Listpos
      • List-equiv
      • Final-cdr
      • Std/lists/append
      • Std/lists/remove
      • Subseq-list
      • Rcons
      • Std/lists/revappend
      • Std/lists/remove-duplicates-equal
      • Std/lists/reverse
      • Std/lists/last
      • Std/lists/resize-list
      • Flatten
      • Suffixp
      • Std/lists/butlast
      • Std/lists/set-difference
      • Std/lists/len
      • Std/lists/intersectp
      • Std/lists/true-listp
      • Intersectp-witness
      • Subsetp-witness
      • Std/lists/remove1-equal
      • Rest-n
      • First-n
      • Std/lists/union
      • Append-without-guard
      • Std/lists/subsetp
      • Std/lists/member
    • Std/alists
    • Obags
    • Std/util
    • Std/strings
    • Std/io
    • Std/osets
    • Std/basic
    • Std/system
    • Std/typed-lists
    • Std/bitsets
    • Std/testing
    • Std/typed-alists
    • Std/stobjs
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Std/lists
• Butlast

Std/lists/butlast

Lemmas about butlast available in the std/lists library.

Definitions and Theorems

The usual definition of butlast is in terms of take. But it's often more convenient to reason about butlast directly. In that case, its recursive redefinition may be what you want:

Theorem: butlast-redefinition

(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)))))

Function: butlast-induction

(defun butlast-induction (x n)
  (if (>= (nfix n) (len x))
      nil
    (cons (car x)
          (butlast-induction (cdr x) n))))

Theorem: use-butlast-induction

(defthm use-butlast-induction
  t
  :rule-classes ((:induction :pattern (butlast x n)
                             :scheme (butlast-induction x n))))

For use with std::deflist:

Theorem: element-list-p-of-butlast

(defthm element-list-p-of-butlast
  (implies (element-list-p (double-rewrite x))
           (element-list-p (butlast x n)))
  :rule-classes :rewrite)