• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
    • Std/lists
    • Std/alists
    • Obags
    • Std/util
    • Std/strings
      • Pretty-printing
      • Printtree
      • Base64
      • Charset-p
      • Strtok!
      • Cases
        • Icharlisteqv
        • Upcase-charlist
        • Downcase-charlist
          • Charlist-has-some-up-alpha-p
          • Downcase-charlist-aux
        • Upcase-string
        • Istreqv
        • Downcase-char
        • Upcase-char
        • Ichareqv
        • Downcase-string
        • Upcase-first-charlist
        • Downcase-first-charlist
        • Downcase-first
        • Upcase-first
        • Down-alpha-p
        • Up-alpha-p
        • Upcase-char-str
        • Downcase-char-str
        • Upcase-string-list
        • Downcase-string-list
      • Concatenation
      • Html-encoding
      • Character-kinds
      • Substrings
      • Strtok
      • Equivalences
      • Url-encoding
      • Lines
      • Explode-implode-equalities
      • Ordering
      • Numbers
      • Pad-trim
      • Coercion
      • Std/strings/digit-to-char
      • Substitution
      • Symbols
    • Std/io
    • Std/osets
    • Std/basic
    • Std/system
    • Std/typed-lists
    • Std/bitsets
    • Std/testing
    • Std/typed-alists
    • Std/stobjs
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Cases

Downcase-charlist

Convert every character in a list to lower case.

Signature

(downcase-charlist x) → *

Arguments

x — Guard (character-listp x).

ACL2 has a built-in alternative to this function, string-downcase1, which however can also convert characters that are not standard characters. (Historical note: Before May 2024, the guard for acl2::string-downcase1 required standard characters yet also converted only standard characters; this provided motivation for the development of this function.)

For sometimes-better performance, we avoid consing and simply return x unchanged when it has no characters that need to be converted. Of course, deciding whether some conversion is necessary will marginally slow this function down when some conversion is necessary, but we think the gain of not consing outweighs this. At any rate, this optimization does not affect the logical definition.

Definitions and Theorems

Function: downcase-charlist

(defun downcase-charlist (x)
  (declare (xargs :guard (character-listp x)))
  (let ((acl2::__function__ 'downcase-charlist))
    (declare (ignorable acl2::__function__))
    (mbe :logic
         (if (atom x)
             nil
           (cons (downcase-char (car x))
                 (downcase-charlist (cdr x))))
         :exec
         (if (charlist-has-some-up-alpha-p x)
             (reverse (downcase-charlist-aux x nil))
           x))))

Theorem: downcase-charlist-when-atom

(defthm downcase-charlist-when-atom
  (implies (atom x)
           (equal (downcase-charlist x) nil)))

Theorem: downcase-charlist-of-cons

(defthm downcase-charlist-of-cons
  (equal (downcase-charlist (cons a x))
         (cons (downcase-char a)
               (downcase-charlist x))))

Theorem: icharlisteqv-implies-equal-downcase-charlist-1

(defthm icharlisteqv-implies-equal-downcase-charlist-1
  (implies (icharlisteqv x x-equiv)
           (equal (downcase-charlist x)
                  (downcase-charlist x-equiv)))
  :rule-classes (:congruence))

Theorem: character-listp-downcase-charlist

(defthm character-listp-downcase-charlist
  (character-listp (downcase-charlist x)))

Theorem: consp-of-downcase-charlist

(defthm consp-of-downcase-charlist
  (equal (consp (downcase-charlist x))
         (consp x)))

Theorem: downcase-charlist-under-iff

(defthm downcase-charlist-under-iff
  (iff (downcase-charlist x) (consp x)))

Theorem: len-of-downcase-charlist

(defthm len-of-downcase-charlist
  (equal (len (downcase-charlist x))
         (len x)))

Theorem: downcase-charlist-aux-is-downcase-charlist

(defthm downcase-charlist-aux-is-downcase-charlist
  (equal (downcase-charlist-aux x acc)
         (revappend (downcase-charlist x) acc)))

Theorem: downcase-charlist-does-nothing-unless-charlist-has-some-up-alpha-p

(defthm
 downcase-charlist-does-nothing-unless-charlist-has-some-up-alpha-p
 (implies (and (not (charlist-has-some-up-alpha-p x))
               (character-listp x))
          (equal (downcase-charlist x) x)))

Theorem: string-downcase1-redef

(defthm string-downcase1-redef
  (implies (standard-char-listp x)
           (equal (acl2::string-downcase1 x)
                  (downcase-charlist (double-rewrite x)))))

Subtopics

Charlist-has-some-up-alpha-p

Downcase-charlist-aux