		Search-engine friendly clone of the ACL2 documentation.

Cases

Upcase-charlist

Convert every character in a list to upper case.

Signature
(upcase-charlist x) → *
Arguments: x — Guard (character-listp x).

ACL2 has a built-in alternative to this function, string-upcase1, which however can also convert characters that are not standard characters. (Historical note: Before May 2024, the guard for acl2::string-upcase1 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: upcase-charlist

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

Theorem: upcase-charlist-when-atom

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

Theorem: upcase-charlist-of-cons

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

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

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

Theorem: character-listp-upcase-charlist

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

Theorem: consp-of-upcase-charlist

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

Theorem: upcase-charlist-under-iff

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

Theorem: len-of-upcase-charlist

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

Theorem: upcase-charlist-aux-is-upcase-charlist

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

Theorem: upcase-charlist-does-nothing-unless-charlist-has-some-down-alpha-p

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

Theorem: string-upcase1-is-upcase-charlist

(defthm string-upcase1-is-upcase-charlist
  (implies (standard-char-listp x)
           (equal (acl2::string-upcase1 x)
                  (upcase-charlist (double-rewrite x)))))

Theorem: not-charlist-has-some-down-alpha-p-of-upcase-charlist

(defthm not-charlist-has-some-down-alpha-p-of-upcase-charlist
  (not (charlist-has-some-down-alpha-p (upcase-charlist x))))

Subtopics

Charlist-has-some-down-alpha-p
Upcase-charlist-aux