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