Convert a character to upper-case.
(upcase-char x) → char
(upcase-char x) converts lower-case characters into their upper-case equivalents, and returns other characters unchanged.
ACL2 has a built-in alternative to this function, common-lisp::char-upcase,
but it is irritating to use because it has standard-char-p guards. In
(defun upcase-char$inline (x) (declare (type character x)) (let ((acl2::__function__ 'upcase-char)) (declare (ignorable acl2::__function__)) (b* (((the (unsigned-byte 8) code) (char-code x))) (if (and (<= (little-a) code) (<= code (little-z))) (code-char (the (unsigned-byte 8) (- code (case-delta)))) (mbe :logic (char-fix x) :exec x)))))
(defthm characterp-of-upcase-char (b* ((char (upcase-char$inline x))) (characterp char)) :rule-classes :type-prescription)
(defthm chareqv-implies-equal-upcase-char-1 (implies (chareqv x x-equiv) (equal (upcase-char x) (upcase-char x-equiv))) :rule-classes (:congruence))
(defthm upcase-char-does-nothing-unless-down-alpha-p (implies (not (down-alpha-p x)) (equal (upcase-char x) (char-fix x))))
(defthm upcase-char-of-upcase-char (equal (upcase-char (upcase-char x)) (upcase-char x)))
(defthm char-upcase-is-upcase-char (equal (common-lisp::char-upcase x) (upcase-char (double-rewrite x))))
(defthm not-down-alpha-p-of-upcase-char (not (down-alpha-p (upcase-char x))))