oct-digit-char-listp

(in-package "STR")

(include-book "std/strings/octal" :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))

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

(controlled-configuration :hooks nil)

(deflist oct-digit-char-listp
  (x)
  :parents (octal)
  :short "Recognize lists of octal digit characters."
  :long (topstring (p "Unlike @(tsee oct-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 oct-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 oct-digit-char-list*p)
     has a backchain limit that doesn't work with some proofs."))
  (oct-digit-char-p x)
  :true-listp t
  :elementp-of-nil nil
  ///
  (defthm oct-digit-char-list*p-when-oct-digit-char-listp
    (implies (oct-digit-char-listp x)
      (oct-digit-char-list*p x))
    :hints (("Goal" :induct t
       :in-theory (enable oct-digit-char-list*p))))
  (defthmd character-listp-when-oct-digit-char-listp
    (implies (oct-digit-char-listp x)
      (character-listp x))))

(defsection oct-digit-char-listp-results
  :parents (oct-digit-char-listp)
  :short "Theorems about results of @(see std/strings) functions
          that return lists of octal digit characters."
  :long (topstring (p "Those @(see std/strings) are accompanied by
     theorems that they return @(tsee oct-digit-char-list*p),
     but they in fact return true lists,
     so here we add theorems that they return @(tsee oct-digit-char-listp)."))
  (defrule oct-digit-char-listp-of-basic-nat-to-oct-chars
    (oct-digit-char-listp (basic-nat-to-oct-chars nat))
    :induct t
    :enable (basic-nat-to-oct-chars oct-digit-char-listp
      digit-to-char
      ifix)
    :prep-books ((include-book "ihs/logops-lemmas" :dir :system) (include-book "arithmetic-3/top" :dir :system)))
  (defrule oct-digit-char-listp-of-nat-to-oct-chars-aux
    (implies (oct-digit-char-listp acc)
      (oct-digit-char-listp (nat-to-oct-chars-aux nat acc)))
    :enable nat-to-oct-chars-aux)
  (defrule oct-digit-char-listp-of-nat-to-oct-chars
    (oct-digit-char-listp (nat-to-oct-chars nat))
    :enable nat-to-oct-chars))