		Search-engine friendly clone of the ACL2 documentation.

Std/lists

Flatten

(flatten x) appends together the elements of x.

Typically x is a list of lists that you want to merge together. For example:

(flatten '((a b c) (1 2 3) (x y z)))
  -->
(a b c 1 2 3 x y z)

This is a "one-level" flatten that does not necessarily produce an atom-listp. For instance,

(flatten '(((a . 1) (b . 2))
           ((x . 3) (y . 4)))
  -->
((a . 1) (b . 2) (x . 3) (y . 4))

Definitions and Theorems

Function: flatten

(defun flatten (x)
       (declare (xargs :guard t))
       (if (consp x)
           (append-without-guard (car x)
                                 (flatten (cdr x)))
           nil))

Theorem: true-listp-of-flatten

(defthm true-listp-of-flatten
        (true-listp (flatten x))
        :rule-classes :type-prescription)

Theorem: flatten-when-not-consp

(defthm flatten-when-not-consp
        (implies (not (consp x))
                 (equal (flatten x) nil)))

Theorem: flatten-of-cons

(defthm flatten-of-cons
        (equal (flatten (cons a x))
               (append a (flatten x))))

Theorem: flatten-of-list-fix

(defthm flatten-of-list-fix
        (equal (flatten (list-fix x))
               (flatten x)))

Theorem: list-equiv-implies-equal-flatten-1

(defthm list-equiv-implies-equal-flatten-1
        (implies (list-equiv x x-equiv)
                 (equal (flatten x) (flatten x-equiv)))
        :rule-classes (:congruence))

Theorem: flatten-of-append

(defthm flatten-of-append
        (equal (flatten (append x y))
               (append (flatten x) (flatten y))))