		Search-engine friendly clone of the ACL2 documentation.

Syntax-abstraction

Abs-hexadecimal-digit-to-nat

Abstract a hexadecimal-digit to a natural number.

Signature
(abs-hexadecimal-digit-to-nat tree) → nat
Arguments: tree — Guard (abnf::treep tree).
Returns: nat — Type (nat-resultp nat).

Definitions and Theorems

Function: abs-hexadecimal-digit-to-nat

(defun abs-hexadecimal-digit-to-nat (tree)
 (declare (xargs :guard (abnf::treep tree)))
 (let ((__function__ 'abs-hexadecimal-digit-to-nat))
  (declare (ignorable __function__))
  (b* (((okf tree)
        (abnf::check-tree-nonleaf-1-1 tree "hexadecimal-digit"))
       (nat (abs-decimal-digit-to-nat tree))
       ((when (not (reserrp nat))) nat)
       ((okf nats)
        (abnf::check-tree-leafterm tree)))
   (cond
    ((abnf::nats-match-insensitive-chars-p nats (list #\a))
     10)
    ((abnf::nats-match-insensitive-chars-p nats (list #\b))
     11)
    ((abnf::nats-match-insensitive-chars-p nats (list #\c))
     12)
    ((abnf::nats-match-insensitive-chars-p nats (list #\d))
     13)
    ((abnf::nats-match-insensitive-chars-p nats (list #\e))
     14)
    ((abnf::nats-match-insensitive-chars-p nats (list #\f))
     15)
    (t
     (reserrf
        (list :found-subtree (abnf::tree-info-for-error tree))))))))

Theorem: nat-resultp-of-abs-hexadecimal-digit-to-nat

(defthm nat-resultp-of-abs-hexadecimal-digit-to-nat
  (b* ((nat (abs-hexadecimal-digit-to-nat tree)))
    (nat-resultp nat))
  :rule-classes :rewrite)

Theorem: natp-of-hexadecimal-to-nat

(defthm natp-of-hexadecimal-to-nat
  (b* ((acl2::?nat (abs-hexadecimal-digit-to-nat tree)))
    (implies (not (reserrp nat))
             (natp nat)))
  :rule-classes :forward-chaining)

Theorem: abs-hexadecimal-digit-to-nat-bound

(defthm abs-hexadecimal-digit-to-nat-bound
  (b* ((acl2::?nat (abs-hexadecimal-digit-to-nat tree)))
    (implies (not (reserrp nat))
             (< nat 16)))
  :rule-classes :linear)

Theorem: abs-hexadecimal-digit-to-nat-of-tree-fix-tree

(defthm abs-hexadecimal-digit-to-nat-of-tree-fix-tree
  (equal (abs-hexadecimal-digit-to-nat (abnf::tree-fix tree))
         (abs-hexadecimal-digit-to-nat tree)))

Theorem: abs-hexadecimal-digit-to-nat-tree-equiv-congruence-on-tree

(defthm abs-hexadecimal-digit-to-nat-tree-equiv-congruence-on-tree
  (implies (abnf::tree-equiv tree tree-equiv)
           (equal (abs-hexadecimal-digit-to-nat tree)
                  (abs-hexadecimal-digit-to-nat tree-equiv)))
  :rule-classes :congruence)