Determine if a character is a lower-case letter (a-z).
(down-alpha-p x) → bool
ACL2 has a built-in alternative to this function, common-lisp::lower-case-p, but it is irritating to use because it has standard-char-p guards. In contrast,
(defun down-alpha-p$inline (x) (declare (type character x)) (let ((acl2::__function__ 'down-alpha-p)) (declare (ignorable acl2::__function__)) (b* (((the (unsigned-byte 8) code) (char-code x))) (and (<= (little-a) code) (<= code (little-z))))))
(defthm chareqv-implies-equal-down-alpha-p-1 (implies (chareqv x x-equiv) (equal (down-alpha-p x) (down-alpha-p x-equiv))) :rule-classes (:congruence))
(defthm lower-case-p-is-down-alpha-p (equal (common-lisp::lower-case-p x) (down-alpha-p (double-rewrite x))))
(defthm down-alpha-p-when-up-alpha-p (implies (up-alpha-p x) (not (down-alpha-p x))))