Recognize unsigned 8-bit bytes.
(bytep x) → yes/no
ACL2 has a flexible notion of `byte', which may be signed or unsigned, and consist of (almost) any number of bits: see unsigned-byte-p and signed-byte-p. But very often the unqualified term `byte' refers to a sequence of exactly 8 bits, represented by natural numbers below 256: this predicate caters to this common terminology.
(defun bytep (x) (declare (xargs :guard t)) (mbe :logic (unsigned-byte-p 8 x) :exec (and (integerp x) (<= 0 x) (< x 256))))
(defthm booleanp-of-bytep (b* ((yes/no (bytep x))) (booleanp yes/no)) :rule-classes :rewrite)
(defthm bytep-compound-recognizer (implies (bytep x) (and (integerp x) (<= 0 x))) :rule-classes :compound-recognizer)