Filtering...

flatten

books/std/lists/flatten

Included Books

equiv
other
(in-package "ACL2")
include-book
(include-book "equiv")
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
(add-macro-alias append-without-guard
  binary-append-without-guard)
other
(defxdoc append-without-guard
  :parents (std/lists append)
  :short "Version of @(see append) that has a guard of @('t')"
  :long "See @(see std::strict-list-recognizers) for a discussion of whether
 requring lists to be @('nil')-terminated is right for you.")
other
(defsection flatten
  :parents (std/lists)
  :short "@(call flatten) appends together the elements of @('x')."
  :long "<p>Typically @('x') is a list of lists that you want to
merge together.  For example:</p>

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

<p>This is a "one-level" flatten that does not necessarily produce
an @(see atom-listp).  For instance,</p>

@({
     (flatten '(((a . 1) (b . 2))
                ((x . 3) (y . 4)))
       -->
     ((a . 1) (b . 2) (x . 3) (y . 4))
})"
  (defund flatten
    (x)
    (declare (xargs :guard t))
    (if (consp x)
      (append-without-guard (car x) (flatten (cdr x)))
      nil))
  (local (in-theory (enable flatten)))
  (in-theory (disable (:type-prescription flatten)))
  (defthm true-listp-of-flatten
    (true-listp (flatten x))
    :rule-classes :type-prescription)
  (defthm flatten-when-not-consp
    (implies (not (consp x)) (equal (flatten x) nil)))
  (defthm flatten-of-cons
    (equal (flatten (cons a x)) (append a (flatten x))))
  (defthm flatten-of-list-fix
    (equal (flatten (list-fix x)) (flatten x)))
  (defcong list-equiv
    equal
    (flatten x)
    1
    :hints (("Goal" :in-theory (disable flatten-of-list-fix)
       :use ((:instance flatten-of-list-fix (x x)) (:instance flatten-of-list-fix (x x-equiv))))))
  (defthm flatten-of-append
    (equal (flatten (append x y))
      (append (flatten x) (flatten y)))))