		Search-engine friendly clone of the ACL2 documentation.

Std/lists

Rcons

Cons onto the back of a list.

(rcons a x) is like 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!

Definitions and Theorems

Function: rcons

(defun rcons (a x)
  (declare (xargs :guard t))
  (append-without-guard x (list a)))

Theorem: type-of-rcons

(defthm type-of-rcons
  (and (consp (rcons a x))
       (true-listp (rcons a x)))
  :rule-classes :type-prescription)

Theorem: rcons-of-list-fix

(defthm rcons-of-list-fix
  (equal (rcons a (list-fix x))
         (rcons a x)))

Theorem: list-equiv-implies-equal-rcons-2

(defthm list-equiv-implies-equal-rcons-2
  (implies (list-equiv x x-equiv)
           (equal (rcons a x) (rcons a x-equiv)))
  :rule-classes (:congruence))

Theorem: list-equiv-of-rcons-and-rcons

(defthm list-equiv-of-rcons-and-rcons
  (equal (list-equiv (rcons a x) (rcons a y))
         (list-equiv x y)))

Theorem: len-of-rcons

(defthm len-of-rcons
  (equal (len (rcons a x)) (+ 1 (len x))))

Theorem: rev-of-rcons

(defthm rev-of-rcons
  (equal (rev (rcons a x))
         (cons a (rev x))))

Theorem: append-of-rcons

(defthm append-of-rcons
  (equal (append (rcons a x) y)
         (append x (cons a y))))

Theorem: rcons-of-append

(defthm rcons-of-append
  (equal (rcons a (append x y))
         (append x (rcons a y))))

Theorem: revappend-of-rcons

(defthm revappend-of-rcons
  (equal (revappend (rcons a x) y)
         (cons a (revappend x y))))

Theorem: element-list-p-of-rcons

(defthm element-list-p-of-rcons
  (iff (element-list-p (rcons a x))
       (and (element-p a)
            (element-list-p (list-fix x))))
  :rule-classes :rewrite)