Recognizer for slong-integer.
(slong-integerp x) → yes/no
Function:
(defun slong-integerp (x) (declare (xargs :guard t)) (mbe :logic (signed-byte-p (long-bits) x) :exec (and (integerp x) (<= (- (expt 2 (1- (long-bits)))) x) (< x (expt 2 (1- (long-bits)))))))
Theorem:
(defthm booleanp-of-slong-integerp (b* ((yes/no (slong-integerp x))) (booleanp yes/no)) :rule-classes :rewrite)
Theorem:
(defthm slong-integerp-forward-signed-byte-p (implies (slong-integerp x) (signed-byte-p (long-bits) x)) :rule-classes :forward-chaining)
Theorem:
(defthm signed-byte-p-rewrite-slong-integerp (equal (signed-byte-p (long-bits) x) (slong-integerp x)))
Theorem:
(defthm integerp-when-slong-integerp (implies (slong-integerp x) (integerp x)) :rule-classes :compound-recognizer)