		Search-engine friendly clone of the ACL2 documentation.

Decimal-integer-literals

Decdig/uscore-list-wfp

Check if a decimal numeral is well-formed.

Signature
(decdig/uscore-list-wfp dus) → yes/no
Arguments: dus — Guard (decdig/uscore-listp dus).
Returns: yes/no — Type (booleanp yes/no).

A decimal-numeral in the grammar is a list of decimal digits and underscores subject to the following constraints, derived from the grammar:

It must start with a digit, not an underscore.
It must end with a digit, not an underscore. (Note that first and last digit may be the same, if the decimal numeral is just 0.)
If the starting digit is 0, then it must be the only digit (which implies that there cannot be any underscores.

Definitions and Theorems

Function: decdig/uscore-list-wfp

(defun decdig/uscore-list-wfp (dus)
  (declare (xargs :guard (decdig/uscore-listp dus)))
  (let ((__function__ 'decdig/uscore-list-wfp))
    (declare (ignorable __function__))
    (and (consp dus)
         (decdig/uscore-case (car dus) :digit)
         (decdig/uscore-case (car (last dus))
                             :digit)
         (implies (equal (decdig/uscore-fix (car dus))
                         (decdig/uscore-digit (char-code #\0)))
                  (= (len dus) 1)))))

Theorem: booleanp-of-decdig/uscore-list-wfp

(defthm booleanp-of-decdig/uscore-list-wfp
  (b* ((yes/no (decdig/uscore-list-wfp dus)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: decdig/uscore-list-wfp-of-decdig/uscore-list-fix-dus

(defthm decdig/uscore-list-wfp-of-decdig/uscore-list-fix-dus
  (equal (decdig/uscore-list-wfp (decdig/uscore-list-fix dus))
         (decdig/uscore-list-wfp dus)))

Theorem: decdig/uscore-list-wfp-decdig/uscore-list-equiv-congruence-on-dus

(defthm
  decdig/uscore-list-wfp-decdig/uscore-list-equiv-congruence-on-dus
  (implies (decdig/uscore-list-equiv dus dus-equiv)
           (equal (decdig/uscore-list-wfp dus)
                  (decdig/uscore-list-wfp dus-equiv)))
  :rule-classes :congruence)