Convert a string to lower case.
(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,
See also upcase-string, which has more discussion on how we try to make this fast.
(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)))))))
(defthm istreqv-implies-equal-downcase-string-1 (implies (istreqv x x-equiv) (equal (downcase-string x) (downcase-string x-equiv))) :rule-classes (:congruence))
(defthm len-of-downcase-string (equal (len (explode (downcase-string x))) (len (explode x))))
(defthm length-of-downcase-string (equal (length (downcase-string x)) (len (explode x))))
(defthm equal-of-empty-string-with-downcase-string (equal (equal "" (downcase-string x)) (atom (explode x))))
(defthm string-downcase-is-downcase-string (equal (common-lisp::string-downcase x) (downcase-string (double-rewrite x))))