dec-digit-char-listp

(in-package "STR")

(include-book "std/strings/decimal" :dir :system)

(include-book "std/util/deflist" :dir :system)

(include-book "std/util/defrule" :dir :system)

(include-book "xdoc/constructors" :dir :system)

(local (include-book "arithmetic-3/top" :dir :system))

(local (include-book "kestrel/built-ins/disable" :dir :system))

(local (disable-most-builtin-logic-defuns))

(local (disable-builtin-rewrite-rules-for-defaults))

(set-induction-depth-limit 0)

(deflist dec-digit-char-listp
  (x)
  :parents (decimal)
  :short "Recognize lists of decimal digit characters."
  :long (topstring (p "Unlike @(tsee dec-digit-char-list*p),
     this requires true list (i.e. @('nil')-terminated.")
    (p "Since there are functions in @(see std/strings)
     that operate on @(tsee dec-digit-char-list*p),
     we provide a bridge theorem between the two recognizers,
     which we can use to satisfy the guards of those functions."))
  (dec-digit-char-p x)
  :true-listp t
  :elementp-of-nil nil
  ///
  (defthm dec-digit-char-list*p-when-dec-digit-char-listp
    (implies (dec-digit-char-listp x)
      (dec-digit-char-list*p x))
    :hints (("Goal" :induct t
       :in-theory (enable dec-digit-char-list*p)))))

(defsection dec-digit-char-listp-results
  :parents (dec-digit-char-listp)
  :short "Theorems about results of @(see std/strings) functions
          that return lists of decimal digit characters."
  :long (topstring (p "Those @(see std/strings) are accompanied by
     theorems that they return @(tsee dec-digit-char-list*p),
     but they in fact return true lists,
     so here we add theorems that they return @(tsee dec-digit-char-listp)."))
  (defrule dec-digit-char-listp-of-basic-nat-to-dec-chars
    (dec-digit-char-listp (basic-nat-to-dec-chars nat))
    :induct t
    :enable (basic-nat-to-dec-chars dec-digit-char-listp
      digit-to-char))
  (defrule dec-digit-char-listp-of-nat-to-dec-chars-aux
    (implies (dec-digit-char-listp acc)
      (dec-digit-char-listp (nat-to-dec-chars-aux nat acc)))
    :enable nat-to-dec-chars-aux)
  (defrule dec-digit-char-listp-of-nat-to-dec-chars
    (dec-digit-char-listp (nat-to-dec-chars nat))
    :enable nat-to-dec-chars))