		Search-engine friendly clone of the ACL2 documentation.

Syntax-abstraction

Abstract-digit

A DIGIT parse tree is abstracted to its decimal digit.

Signature
(abstract-digit tree) → digit
Arguments: tree — Guard (treep tree).
Returns: digit — Type (integer-range-p 0 10 digit).

Definitions and Theorems

Function: abstract-digit

(defun abstract-digit (tree)
  (declare (xargs :guard (treep tree)))
  (b* (((fun (fail))
        (prog2$ (abstract-fail) 0))
       ((unless (tree-case tree :nonleaf))
        (fail))
       (treess (tree-nonleaf->branches tree))
       ((unless (consp treess)) (fail))
       (trees (car treess))
       ((unless (consp trees)) (fail))
       (subtree (car trees))
       (nat (abstract-terminal subtree))
       ((unless (and (<= (char-code #\0) nat)
                     (<= nat (char-code #\9))))
        (fail)))
    (- nat (char-code #\0))))

Theorem: return-type-of-abstract-digit

(defthm return-type-of-abstract-digit
  (b* ((digit (abstract-digit tree)))
    (integer-range-p 0 10 digit))
  :rule-classes :rewrite)

Theorem: natp-of-abstract-digit

(defthm natp-of-abstract-digit
  (b* ((digit (abstract-digit tree)))
    (natp digit))
  :rule-classes :type-prescription)

Theorem: abstract-digit-linear

(defthm abstract-digit-linear
  (b* ((digit (abstract-digit tree)))
    (< digit 10))
  :rule-classes :linear)