		Search-engine friendly clone of the ACL2 documentation.

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, but it is irritating to use because it has standard-char-p guards. In contrast, downcase-charlist works on arbitrary characters.

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
        (equal (acl2::string-downcase1 x)
               (downcase-charlist (double-rewrite x))))

Subtopics

Charlist-has-some-up-alpha-p
Downcase-charlist-aux