		Search-engine friendly clone of the ACL2 documentation.

Decimal-digits-grammar-validation

Dec-digit-tree

Tree for a decimal digit.

Signature
(dec-digit-tree digit) → tree
Arguments: digit — Guard (dec-digitp digit).
Returns: tree — Type (abnf-tree-with-root-p tree "digit").

This is used in grammar-dec-digitp-when-dec-digitp.

If the digit is 0, the resulting tree has just a leaf subtree. Otherwise, it has a non-zero-digit subtree with a leaf subtree.

Definitions and Theorems

Function: dec-digit-tree

(defun dec-digit-tree (digit)
 (declare (xargs :guard (dec-digitp digit)))
 (let ((__function__ 'dec-digit-tree))
  (declare (ignorable __function__))
  (b* ((digit (dec-digit-fix digit)))
   (if (equal digit (char-code #\0))
       (abnf::tree-nonleaf
            (abnf::rulename "digit")
            (list (list (abnf::tree-leafterm (list digit)))))
    (abnf::tree-nonleaf
     (abnf::rulename "digit")
     (list
      (list
       (abnf::tree-nonleaf
            (abnf::rulename "non-zero-digit")
            (list (list (abnf::tree-leafterm (list digit))))))))))))

Theorem: return-type-of-dec-digit-tree

(defthm return-type-of-dec-digit-tree
  (b* ((tree (dec-digit-tree digit)))
    (abnf-tree-with-root-p tree "digit"))
  :rule-classes :rewrite)

Theorem: tree->string-of-dec-digit-tree

(defthm tree->string-of-dec-digit-tree
  (equal (abnf::tree->string (dec-digit-tree digit))
         (list (dec-digit-fix digit))))

Theorem: dec-digit-tree-of-dec-digit-fix-digit

(defthm dec-digit-tree-of-dec-digit-fix-digit
  (equal (dec-digit-tree (dec-digit-fix digit))
         (dec-digit-tree digit)))

Theorem: dec-digit-tree-dec-digit-equiv-congruence-on-digit

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