		Search-engine friendly clone of the ACL2 documentation.

Downcase-string

Convert a string to lower case.

Signature
(downcase-string x) → *

(downcase-string x) converts a string to lower case, effectively by transforming each of its characters with downcase-char.

ACL2 has a built-in alternative to this function, common-lisp::string-downcase, but it is irritating to use because it has standard-char-p guards. In contrast, downcase-string works on strings with arbitrary characters.

See also upcase-string, which has more discussion on how we try to make this fast.

Definitions and Theorems

Function: downcase-string

(defun downcase-string (x)
 (declare (type string x))
 (let ((acl2::__function__ 'downcase-string))
   (declare (ignorable acl2::__function__))
   (mbe :logic
        (implode (downcase-charlist (explode x)))
        :exec
        (let ((xl (length x)))
          (if (not (string-has-some-up-alpha-p x 0 xl))
              x
            (rchars-to-string (downcase-string-aux x 0 xl nil)))))))

Theorem: istreqv-implies-equal-downcase-string-1

(defthm istreqv-implies-equal-downcase-string-1
  (implies (istreqv x x-equiv)
           (equal (downcase-string x)
                  (downcase-string x-equiv)))
  :rule-classes (:congruence))

Theorem: len-of-downcase-string

(defthm len-of-downcase-string
  (equal (len (explode (downcase-string x)))
         (len (explode x))))

Theorem: length-of-downcase-string

(defthm length-of-downcase-string
  (equal (length (downcase-string x))
         (len (explode x))))

Theorem: equal-of-empty-string-with-downcase-string

(defthm equal-of-empty-string-with-downcase-string
  (equal (equal "" (downcase-string x))
         (atom (explode x))))

Theorem: string-downcase-is-downcase-string

(defthm string-downcase-is-downcase-string
  (implies (standard-char-listp (explode x))
           (equal (common-lisp::string-downcase x)
                  (downcase-string (double-rewrite x)))))

Subtopics

String-has-some-up-alpha-p
Downcase-string-aux