		Search-engine friendly clone of the ACL2 documentation.

Octal-digits

Oct-digit-value

Numeric value of a Java octal digit.

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

Definitions and Theorems

Function: oct-digit-value

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

Theorem: natp-of-oct-digit-value

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

Theorem: oct-digit-value-upper-bound

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

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

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

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

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