		Search-engine friendly clone of the ACL2 documentation.

Patterns

Pat-flatten1

Flatten a pattern into a list of atoms (without an accumulator).

(pat-flatten1 pat) is just a simpler flattening function that does the same thing as pat-flatten but without an accumulator. It is generally convenient to reason about.

Definitions and Theorems

Function: pat-flatten1

(defun pat-flatten1 (pat)
       (declare (xargs :guard t))
       (mbe :logic (if pat
                       (if (atom pat)
                           (list pat)
                           (append (pat-flatten1 (car pat))
                                   (pat-flatten1 (cdr pat))))
                       nil)
            :exec (pat-flatten pat nil)))

Theorem: pat-flatten-is-pat-flatten1

(defthm pat-flatten-is-pat-flatten1
        (equal (pat-flatten pat acc)
               (append (pat-flatten1 pat) acc)))

Theorem: true-listp-of-pat-flatten1

(defthm true-listp-of-pat-flatten1
        (true-listp (pat-flatten1 x))
        :rule-classes ((:type-prescription) (:rewrite)))

Theorem: pat-flatten1-when-atom

(defthm pat-flatten1-when-atom
        (implies (atom pat)
                 (equal (pat-flatten1 pat)
                        (if pat (list pat) nil))))

Theorem: pat-flatten1-of-cons

(defthm pat-flatten1-of-cons
        (equal (pat-flatten1 (cons x y))
               (append (pat-flatten1 x)
                       (pat-flatten1 y))))

Theorem: pat-flatten1-nonnil

(defthm pat-flatten1-nonnil
        (not (member-equal nil (pat-flatten1 x))))