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