hex-digit-char-listp

(in-package "STR")

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

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

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

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

(include-book "std/basic/controlled-configuration" :dir :system)

(controlled-configuration :hooks nil)

(deflist hex-digit-char-listp
  (x)
  :parents (hex)
  :short "Recognize lists of hexadecimal digit characters."
  :long (topstring (p "Unlike @(tsee hex-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 hex-digit-char-list*p),
     we provide a bridge theorem between the two recognizers,
     which we can use to satisfy the guards of those functions.")
    (p "We also provide a (disabled) theorem to backchain without limit
     from @(tsee character-listp) to this recognizer,
     because the one for @(tsee hex-digit-char-list*p)
     has a backchain limit that doesn't work with some proofs."))
  (hex-digit-char-p x)
  :true-listp t
  :elementp-of-nil nil
  ///
  (defthm hex-digit-char-list*p-when-hex-digit-char-listp
    (implies (hex-digit-char-listp x)
      (hex-digit-char-list*p x))
    :hints (("Goal" :induct t
       :in-theory (enable hex-digit-char-list*p))))
  (defthmd character-listp-when-hex-digit-char-listp
    (implies (hex-digit-char-listp x)
      (character-listp x))))

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