Filtering...

rcons

books/std/lists/rcons

Included Books

equiv rev append inductions
other
(in-package "ACL2")
include-book
(include-book "equiv")
include-book
(include-book "rev")
include-book
(include-book "append")
local
(local (include-book "std/basic/inductions" :dir :system))
binary-append-without-guardfunction
(defun binary-append-without-guard
  (x y)
  (declare (xargs :guard t))
  (mbe :logic (append x y)
    :exec (if (consp x)
      (cons (car x) (binary-append-without-guard (cdr x) y))
      y)))
append-without-guardmacro
(defmacro append-without-guard
  (x y &rest rst)
  (xxxjoin 'binary-append-without-guard (list* x y rst)))
other
(defsection rcons
  :parents (std/lists)
  :short "Cons onto the back of a list."
  :long "<p>@(call rcons) is like @(see cons), except that instead of putting
@('a') onto front of the list @('x'), it puts it at the end.  To borrow ML
notation, we compute @('x@[a]') instead of @('a::x').  This is obviously quite
inefficient: we have to copy the whole list just to add one element!</p>"
  (defund rcons
    (a x)
    (declare (xargs :guard t))
    (append-without-guard x (list a)))
  (in-theory (disable (:type-prescription rcons)))
  (local (in-theory (enable rcons)))
  (defthm type-of-rcons
    (and (consp (rcons a x)) (true-listp (rcons a x)))
    :rule-classes :type-prescription)
  (defthm rcons-of-list-fix
    (equal (rcons a (list-fix x)) (rcons a x)))
  (defcong list-equiv equal (rcons a x) 2)
  (local (defthm l0
      (equal (list-equiv (cons a x) y)
        (and (consp y) (equal (car y) a) (list-equiv x (cdr y))))))
  (defthm list-equiv-of-rcons-and-rcons
    (equal (list-equiv (rcons a x) (rcons a y))
      (list-equiv x y))
    :hints (("Goal" :induct (cdr-cdr-induct x y))))
  (defthm len-of-rcons
    (equal (len (rcons a x)) (+ 1 (len x))))
  (defthm rev-of-rcons
    (equal (rev (rcons a x)) (cons a (rev x))))
  (defthm append-of-rcons
    (equal (append (rcons a x) y) (append x (cons a y))))
  (defthm rcons-of-append
    (equal (rcons a (append x y)) (append x (rcons a y))))
  (defthm revappend-of-rcons
    (equal (revappend (rcons a x) y) (cons a (revappend x y))))
  (def-listp-rule element-list-p-of-rcons
    (iff (element-list-p (rcons a x))
      (and (element-p a) (element-list-p (list-fix x))))
    :hints (("goal" :cases ((element-list-final-cdr-p t))))))