make-character-list

(in-package "STR")

(include-book "char-fix")

(local (include-book "std/lists/append" :dir :system))

(in-theory (disable make-character-list))

(defsection std/strings/make-character-list
  :parents (coercion make-character-list)
  :short "Lemmas about @(see make-character-list) in the @(see std/strings)
library."
  :long "<p>This function is normally not anything you would ever want to use.
It is notable mainly for the role it plays in the completion axiom for @(see
coerce).</p>"
  (local (in-theory (enable make-character-list)))
  (defthm make-character-list-when-atom
    (implies (atom x)
      (equal (make-character-list x) nil)))
  (defthm make-character-list-of-cons
    (equal (make-character-list (cons a x))
      (cons (char-fix a)
        (make-character-list x))))
  (defthm consp-of-make-character-list
    (equal (consp (make-character-list x))
      (consp x)))
  (defthm make-character-list-under-iff
    (iff (make-character-list x) (consp x)))
  (defthm len-of-make-character-list
    (equal (len (make-character-list x))
      (len x)))
  (defthm make-character-list-when-character-listp
    (implies (character-listp x)
      (equal (make-character-list x) x)))
  (defthm character-listp-of-make-character-list
    (character-listp (make-character-list x)))
  (defthm make-character-list-of-append
    (equal (make-character-list (append x y))
      (append (make-character-list x)
        (make-character-list y))))
  (defthm make-character-list-of-revappend
    (equal (make-character-list (revappend x y))
      (revappend (make-character-list x)
        (make-character-list y)))))