		Search-engine friendly clone of the ACL2 documentation.

Decimal-digits

Dec-digit-value

Numeric value of a Java decimal digit.

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

Definitions and Theorems

Function: dec-digit-value

(defun dec-digit-value (x)
  (declare (xargs :guard (dec-digitp x)))
  (let ((__function__ 'dec-digit-value))
    (declare (ignorable __function__))
    (b* ((x (mbe :logic (dec-digit-fix x) :exec x)))
      (- x (char-code #\0)))))

Theorem: natp-of-dec-digit-value

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

Theorem: dec-digit-value-upper-bound

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

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

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

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

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