Std/system/good-atom-listp
Theorems about good-atom-listp.
The good-atom-listp-of-cons theorem is useful
to verify the guards of calls of packn or packn-pos
on lists of good atoms, as these functions are often used.
We order the disjuncts in the right side of this rewrite rule
roughly according to the supposed relative frequency
of the different types of good atoms:
it seems that symbols would be the most common,
followed by numbers (e.g. for indices),
then strings (which can be often avoided, using symbols instead),
then characters (which may be just written as symbols or strings).
Note that we expect the nil case to be taken care of by
the executable counterpart of good-atom-listp.
Definitions and Theorems
Theorem: good-atom-listp-of-cons
(defthm good-atom-listp-of-cons
(equal (good-atom-listp (cons x y))
(and (or (symbolp x)
(acl2-numberp x)
(stringp x)
(characterp x))
(good-atom-listp y))))
