		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)