		Search-engine friendly clone of the ACL2 documentation.

Hexadecimal-digits

Hex-digit-value

Numeric value of a Java hexadecimal digit.

Signature
(hex-digit-value x) → val
Arguments: x — Guard (hex-digitp x).
Returns: val — Type (natp val).

Definitions and Theorems

Function: hex-digit-value

(defun hex-digit-value (x)
  (declare (xargs :guard (hex-digitp x)))
  (let ((__function__ 'hex-digit-value))
    (declare (ignorable __function__))
    (b* ((x (mbe :logic (hex-digit-fix x) :exec x)))
      (cond ((and (<= (char-code #\0) x)
                  (<= x (char-code #\9)))
             (- x (char-code #\0)))
            ((and (<= (char-code #\A) x)
                  (<= x (char-code #\F)))
             (+ 10 (- x (char-code #\A))))
            ((and (<= (char-code #\a) x)
                  (<= x (char-code #\f)))
             (+ 10 (- x (char-code #\a))))
            (t (impossible))))))

Theorem: natp-of-hex-digit-value

(defthm natp-of-hex-digit-value
  (b* ((val (hex-digit-value x)))
    (natp val))
  :rule-classes (:rewrite :type-prescription))

Theorem: hex-digit-value-upper-bound

(defthm hex-digit-value-upper-bound
  (b* ((?val (hex-digit-value x)))
    (<= val 15))
  :rule-classes :linear)

Theorem: hex-digit-value-of-hex-digit-fix-x

(defthm hex-digit-value-of-hex-digit-fix-x
  (equal (hex-digit-value (hex-digit-fix x))
         (hex-digit-value x)))

Theorem: hex-digit-value-hex-digit-equiv-congruence-on-x

(defthm hex-digit-value-hex-digit-equiv-congruence-on-x
  (implies (hex-digit-equiv x x-equiv)
           (equal (hex-digit-value x)
                  (hex-digit-value x-equiv)))
  :rule-classes :congruence)