Abs-hex-digit
Abstract a hex-digit tree to a natural number below 16.
- Signature
(abs-hex-digit tree) → val
- Arguments
- tree — Guard (abnf-tree-with-root-p tree "hex-digit").
- Returns
- val — Type (natp val).
A hex-digit tree is essentially a single
hexadecimal digit Unicode character,
which denotes a natural number below 16.
We abstract this kind of tree to the denoted value.
A hex-digit tree has a single subtree,
accessible via caar.
That subtree is a terminal leaf tree
with a single terminal (natural number)
that is the ASCII/Unicode code of a hexadecimal digit,
which we map to the value it denotes via hex-digit-value.
Definitions and Theorems
Function: abs-hex-digit
(defun abs-hex-digit (tree)
(declare (xargs :guard (abnf-tree-with-root-p tree "hex-digit")))
(let ((__function__ 'abs-hex-digit))
(declare (ignorable __function__))
(b* ((subtree (caar (abnf::tree-nonleaf->branches tree)))
(string (abnf::tree->string subtree))
(hexdig (car string)))
(hex-digit-value hexdig))))
Theorem: natp-of-abs-hex-digit
(defthm natp-of-abs-hex-digit
(b* ((val (abs-hex-digit tree)))
(natp val))
:rule-classes :rewrite)
Theorem: abs-hex-digit-upper-bound
(defthm abs-hex-digit-upper-bound
(b* ((?val (abs-hex-digit tree)))
(<= val 15))
:rule-classes :linear)
