downcase - ACL2 Book

other

(in-package "ACL2")

char-downcase-genfunction

(defund char-downcase-gen
  (char)
  (declare (xargs :guard (characterp char)))
  (if (standard-char-p char)
    (char-downcase char)
    char))

chars-downcase-genfunction

(defund chars-downcase-gen
  (chars acc)
  (declare (xargs :guard (and (character-listp chars) (character-listp acc))))
  (if (endp chars)
    (reverse acc)
    (chars-downcase-gen (rest chars)
      (cons (char-downcase-gen (first chars)) acc))))

character-listp-of-chars-downcase-gentheorem

(defthm character-listp-of-chars-downcase-gen
  (implies (and (character-listp chars) (character-listp acc))
    (character-listp (chars-downcase-gen chars acc)))
  :hints (("Goal" :in-theory (enable chars-downcase-gen))))

string-downcase-genfunction

(defund string-downcase-gen
  (str)
  (declare (xargs :guard (stringp str)))
  (coerce (chars-downcase-gen (coerce str 'list) nil) 'string))

stringp-of-string-downcase-gentheorem

(defthm stringp-of-string-downcase-gen
  (stringp (string-downcase-gen str)))