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.
(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)))
(defthm pat-flatten-is-pat-flatten1 (equal (pat-flatten pat acc) (append (pat-flatten1 pat) acc)))
(defthm true-listp-of-pat-flatten1 (true-listp (pat-flatten1 x)) :rule-classes ((:type-prescription) (:rewrite)))
(defthm pat-flatten1-when-atom (implies (atom pat) (equal (pat-flatten1 pat) (if pat (list pat) nil))))
(defthm pat-flatten1-of-cons (equal (pat-flatten1 (cons x y)) (append (pat-flatten1 x) (pat-flatten1 y))))
(defthm pat-flatten1-nonnil (not (member-equal nil (pat-flatten1 x))))