|
|
|---|
|
|
|
|---|
Recognize unsigned 4-bit bytes.
(nibblep 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, and the term `nibble' refers to half of such a byte, i.e. a sequence of 4 bits, represented by natural numbers below 16; this predicate caters to this common terminology.
Function:
(defun nibblep (x) (declare (xargs :guard t)) (mbe :logic (unsigned-byte-p 4 x) :exec (and (integerp x) (<= 0 x) (< x 16))))
Theorem:
(defthm booleanp-of-nibblep (b* ((yes/no (nibblep x))) (booleanp yes/no)) :rule-classes :rewrite)
Theorem:
(defthm nibblep-compound-recognizer (implies (nibblep x) (and (integerp x) (<= 0 x))) :rule-classes :compound-recognizer)