/usr/share/acl2-6.3/books/str/case-conversion.cert

(IN-PACKAGE "ACL2")
"ACL2 Version 6.3"
:BEGIN-PORTCULLIS-CMDS
(INCLUDE-BOOK "cutil/portcullis" :DIR :SYSTEM)
:END-PORTCULLIS-CMDS
:EXPANSION-ALIST
((6 RECORD-EXPANSION (DEFSECTION STR::UPCASE-CHARLIST :PARENTS (STR::CASES) :SHORT "Convert every character in a list to upper case." :LONG "<p>@(call upcase-charlist) maps @(see upcase-char) across a character
list.</p>

<p>ACL2 has a built-in alternative to this function, @('string-upcase1'), but
it is irritating to use because it has @(see standard-char-p) guards.  In
contrast, @('upcase-charlist') works on arbitrary characters.</p>

<p>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.</p>" (DEFUND STR::CHARLIST-HAS-SOME-DOWN-ALPHA-P (X) (DECLARE (XARGS :GUARD (CHARACTER-LISTP X))) (IF (ATOM X) NIL (OR (STR::DOWN-ALPHA-P (CAR X)) (STR::CHARLIST-HAS-SOME-DOWN-ALPHA-P (CDR X))))) (DEFUND STR::UPCASE-CHARLIST-AUX (X STR::ACC) (DECLARE (XARGS :GUARD (AND (CHARACTER-LISTP X) (CHARACTER-LISTP STR::ACC)))) (IF (ATOM X) STR::ACC (STR::UPCASE-CHARLIST-AUX (CDR X) (CONS (STR::UPCASE-CHAR (CAR X)) STR::ACC)))) (DEFUND STR::UPCASE-CHARLIST (X) (DECLARE (XARGS :GUARD (CHARACTER-LISTP X) :VERIFY-GUARDS NIL)) (MBE :LOGIC (IF (ATOM X) NIL (CONS (STR::UPCASE-CHAR (CAR X)) (STR::UPCASE-CHARLIST (CDR X)))) :EXEC (IF (STR::CHARLIST-HAS-SOME-DOWN-ALPHA-P X) (REVERSE (STR::UPCASE-CHARLIST-AUX X NIL)) X))) (LOCAL (IN-THEORY (ENABLE STR::UPCASE-CHARLIST STR::UPCASE-CHARLIST-AUX STR::CHARLIST-HAS-SOME-DOWN-ALPHA-P))) (DEFTHM STR::UPCASE-CHARLIST-WHEN-ATOM (IMPLIES (ATOM X) (EQUAL (STR::UPCASE-CHARLIST X) NIL))) (DEFTHM STR::UPCASE-CHARLIST-OF-CONS (EQUAL (STR::UPCASE-CHARLIST (CONS A X)) (CONS (STR::UPCASE-CHAR A) (STR::UPCASE-CHARLIST X)))) (DEFCONG STR::ICHARLISTEQV EQUAL (STR::UPCASE-CHARLIST X) 1 :HINTS (("Goal" :IN-THEORY (ENABLE STR::ICHARLISTEQV)))) (DEFTHM STR::CHARACTER-LISTP-UPCASE-CHARLIST (CHARACTER-LISTP (STR::UPCASE-CHARLIST X))) (DEFTHM STR::CONSP-OF-UPCASE-CHARLIST (EQUAL (CONSP (STR::UPCASE-CHARLIST X)) (CONSP X))) (DEFTHM STR::UPCASE-CHARLIST-UNDER-IFF (IFF (STR::UPCASE-CHARLIST X) (CONSP X)) :HINTS (("Goal" :IN-THEORY (ENABLE STR::UPCASE-CHARLIST)))) (DEFTHM STR::LEN-OF-UPCASE-CHARLIST (EQUAL (LEN (STR::UPCASE-CHARLIST X)) (LEN X))) (DEFTHM STR::UPCASE-CHARLIST-AUX-IS-UPCASE-CHARLIST (EQUAL (STR::UPCASE-CHARLIST-AUX X STR::ACC) (REVAPPEND (STR::UPCASE-CHARLIST X) STR::ACC))) (DEFTHM STR::UPCASE-CHARLIST-DOES-NOTHING-UNLESS-CHARLIST-HAS-SOME-DOWN-ALPHA-P (IMPLIES (AND (NOT (STR::CHARLIST-HAS-SOME-DOWN-ALPHA-P X)) (CHARACTER-LISTP X)) (EQUAL (STR::UPCASE-CHARLIST X) X))) (VERIFY-GUARDS STR::UPCASE-CHARLIST) (DEFTHM STR::STRING-UPCASE1-IS-UPCASE-CHARLIST (EQUAL (STRING-UPCASE1 X) (STR::UPCASE-CHARLIST (DOUBLE-REWRITE X))))) (WITH-OUTPUT :STACK :PUSH :OFF :ALL :ON ERROR (PROGN (TABLE INTRO-TABLE :MARK (QUOTE STR::UPCASE-CHARLIST)) (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (DEFUND STR::CHARLIST-HAS-SOME-DOWN-ALPHA-P (X) (DECLARE (XARGS :GUARD (CHARACTER-LISTP X))) (IF (ATOM X) NIL (OR (STR::DOWN-ALPHA-P (CAR X)) (STR::CHARLIST-HAS-SOME-DOWN-ALPHA-P (CDR X))))) (DEFUND STR::UPCASE-CHARLIST-AUX (X STR::ACC) (DECLARE (XARGS :GUARD (AND (CHARACTER-LISTP X) (CHARACTER-LISTP STR::ACC)))) (IF (ATOM X) STR::ACC (STR::UPCASE-CHARLIST-AUX (CDR X) (CONS (STR::UPCASE-CHAR (CAR X)) STR::ACC)))) (DEFUND STR::UPCASE-CHARLIST (X) (DECLARE (XARGS :GUARD (CHARACTER-LISTP X) :VERIFY-GUARDS NIL)) (MBE :LOGIC (IF (ATOM X) NIL (CONS (STR::UPCASE-CHAR (CAR X)) (STR::UPCASE-CHARLIST (CDR X)))) :EXEC (IF (STR::CHARLIST-HAS-SOME-DOWN-ALPHA-P X) (REVERSE (STR::UPCASE-CHARLIST-AUX X NIL)) X))) (LOCAL (IN-THEORY (ENABLE STR::UPCASE-CHARLIST STR::UPCASE-CHARLIST-AUX STR::CHARLIST-HAS-SOME-DOWN-ALPHA-P))) (DEFTHM STR::UPCASE-CHARLIST-WHEN-ATOM (IMPLIES (ATOM X) (EQUAL (STR::UPCASE-CHARLIST X) NIL))) (DEFTHM STR::UPCASE-CHARLIST-OF-CONS (EQUAL (STR::UPCASE-CHARLIST (CONS A X)) (CONS (STR::UPCASE-CHAR A) (STR::UPCASE-CHARLIST X)))) (DEFCONG STR::ICHARLISTEQV EQUAL (STR::UPCASE-CHARLIST X) 1 :HINTS (("Goal" :IN-THEORY (ENABLE STR::ICHARLISTEQV)))) (DEFTHM STR::CHARACTER-LISTP-UPCASE-CHARLIST (CHARACTER-LISTP (STR::UPCASE-CHARLIST X))) (DEFTHM STR::CONSP-OF-UPCASE-CHARLIST (EQUAL (CONSP (STR::UPCASE-CHARLIST X)) (CONSP X))) (DEFTHM STR::UPCASE-CHARLIST-UNDER-IFF (IFF (STR::UPCASE-CHARLIST X) (CONSP X)) :HINTS (("Goal" :IN-THEORY (ENABLE STR::UPCASE-CHARLIST)))) (DEFTHM STR::LEN-OF-UPCASE-CHARLIST (EQUAL (LEN (STR::UPCASE-CHARLIST X)) (LEN X))) (DEFTHM STR::UPCASE-CHARLIST-AUX-IS-UPCASE-CHARLIST (EQUAL (STR::UPCASE-CHARLIST-AUX X STR::ACC) (REVAPPEND (STR::UPCASE-CHARLIST X) STR::ACC))) (DEFTHM STR::UPCASE-CHARLIST-DOES-NOTHING-UNLESS-CHARLIST-HAS-SOME-DOWN-ALPHA-P (IMPLIES (AND (NOT (STR::CHARLIST-HAS-SOME-DOWN-ALPHA-P X)) (CHARACTER-LISTP X)) (EQUAL (STR::UPCASE-CHARLIST X) X))) (VERIFY-GUARDS STR::UPCASE-CHARLIST) (DEFTHM STR::STRING-UPCASE1-IS-UPCASE-CHARLIST (EQUAL (STRING-UPCASE1 X) (STR::UPCASE-CHARLIST (DOUBLE-REWRITE X)))))) (RECORD-EXPANSION (MAKE-EVENT (LET* ((XDOC::NAME (QUOTE STR::UPCASE-CHARLIST)) (XDOC::PARENTS (QUOTE (STR::CASES))) (XDOC::SHORT (QUOTE "Convert every character in a list to upper case.")) (XDOC::EXTENSION (QUOTE NIL)) (XDOC::WRLD (W STATE)) (XDOC::TRIPS (REVERSED-WORLD-SINCE-EVENT XDOC::WRLD (QUOTE (TABLE INTRO-TABLE :MARK (QUOTE STR::UPCASE-CHARLIST))) NIL)) (XDOC::INFO (REVERSE (NEW-FORMULA-INFO XDOC::TRIPS XDOC::WRLD NIL))) (XDOC::AUTODOC (XDOC::FORMULA-INFO-TO-DEFS (NOT XDOC::EXTENSION) XDOC::INFO)) (XDOC::LONG (CONCATENATE (QUOTE STRING) (QUOTE "<p>@(call upcase-charlist) maps @(see upcase-char) across a character
list.</p>

<p>ACL2 has a built-in alternative to this function, @('string-upcase1'), but
it is irritating to use because it has @(see standard-char-p) guards.  In
contrast, @('upcase-charlist') works on arbitrary characters.</p>

<p>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.</p>") (COERCE (LIST #\Newline #\Newline) (QUOTE STRING)) XDOC::AUTODOC))) (IF XDOC::EXTENSION (CONS (QUOTE XDOC-EXTEND) (CONS XDOC::EXTENSION (CONS XDOC::LONG (QUOTE NIL)))) (CONS (QUOTE DEFXDOC) (CONS XDOC::NAME (CONS (QUOTE :PARENTS) (CONS XDOC::PARENTS (CONS (QUOTE :SHORT) (CONS XDOC::SHORT (CONS (QUOTE :LONG) (CONS XDOC::LONG (QUOTE NIL)))))))))))) (WITH-OUTPUT :OFF (EVENT SUMMARY) (PROGN (TABLE XDOC (QUOTE DOC) (CONS (QUOTE ((:NAME . STR::UPCASE-CHARLIST) (:BASE-PKG . STR::ACL2-PKG-WITNESS) (:PARENTS STR::CASES) (:SHORT . "Convert every character in a list to upper case.") (:LONG . "<p>@(call upcase-charlist) maps @(see upcase-char) across a character
list.</p>

<p>ACL2 has a built-in alternative to this function, @('string-upcase1'), but
it is irritating to use because it has @(see standard-char-p) guards.  In
contrast, @('upcase-charlist') works on arbitrary characters.</p>

<p>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.</p>

<h3>Definitions and Theorems</h3>@(def |STR|::|CHARLIST-HAS-SOME-DOWN-ALPHA-P|)
@(def |STR|::|UPCASE-CHARLIST-AUX|)
@(def |STR|::|UPCASE-CHARLIST|)
@(def |STR|::|UPCASE-CHARLIST-WHEN-ATOM|)
@(def |STR|::|UPCASE-CHARLIST-OF-CONS|)
@(def |STR|::|ICHARLISTEQV-IMPLIES-EQUAL-UPCASE-CHARLIST-1|)
@(def |STR|::|CHARACTER-LISTP-UPCASE-CHARLIST|)
@(def |STR|::|CONSP-OF-UPCASE-CHARLIST|)
@(def |STR|::|UPCASE-CHARLIST-UNDER-IFF|)
@(def |STR|::|LEN-OF-UPCASE-CHARLIST|)
@(def |STR|::|UPCASE-CHARLIST-AUX-IS-UPCASE-CHARLIST|)
@(def |STR|::|UPCASE-CHARLIST-DOES-NOTHING-UNLESS-CHARLIST-HAS-SOME-DOWN-ALPHA-P|)
@(def |STR|::|STRING-UPCASE1-IS-UPCASE-CHARLIST|)") (:FROM . "[books]/str/case-conversion.lisp"))) (XDOC::GET-XDOC-TABLE WORLD))) (VALUE-TRIPLE (QUOTE (DEFXDOC STR::UPCASE-CHARLIST)))))) (VALUE-TRIPLE (QUOTE STR::UPCASE-CHARLIST))))) (7 RECORD-EXPANSION (DEFSECTION STR::DOWNCASE-CHARLIST :PARENTS (STR::CASES) :SHORT "Convert every character in a list to lower case." :LONG "<p>@(call downcase-charlist) maps @(see downcase-char) across a
character list.</p>

<p>ACL2 has a built-in alternative to this function, @('string-downcase1'), but
it is irritating to use because it has @(see standard-char-p) guards.  In
contrast, @('downcase-charlist') works on arbitrary characters.</p>

<p>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.</p>" (DEFUND STR::CHARLIST-HAS-SOME-UP-ALPHA-P (X) (DECLARE (XARGS :GUARD (CHARACTER-LISTP X))) (IF (ATOM X) NIL (OR (STR::UP-ALPHA-P (CAR X)) (STR::CHARLIST-HAS-SOME-UP-ALPHA-P (CDR X))))) (DEFUND STR::DOWNCASE-CHARLIST-AUX (X STR::ACC) (DECLARE (XARGS :GUARD (AND (CHARACTER-LISTP X) (CHARACTER-LISTP STR::ACC)))) (IF (ATOM X) STR::ACC (STR::DOWNCASE-CHARLIST-AUX (CDR X) (CONS (STR::DOWNCASE-CHAR (CAR X)) STR::ACC)))) (DEFUND STR::DOWNCASE-CHARLIST (X) (DECLARE (XARGS :GUARD (CHARACTER-LISTP X) :VERIFY-GUARDS NIL)) (MBE :LOGIC (IF (ATOM X) NIL (CONS (STR::DOWNCASE-CHAR (CAR X)) (STR::DOWNCASE-CHARLIST (CDR X)))) :EXEC (IF (STR::CHARLIST-HAS-SOME-UP-ALPHA-P X) (REVERSE (STR::DOWNCASE-CHARLIST-AUX X NIL)) X))) (LOCAL (IN-THEORY (ENABLE STR::DOWNCASE-CHARLIST STR::DOWNCASE-CHARLIST-AUX STR::CHARLIST-HAS-SOME-UP-ALPHA-P))) (DEFTHM STR::DOWNCASE-CHARLIST-WHEN-ATOM (IMPLIES (ATOM X) (EQUAL (STR::DOWNCASE-CHARLIST X) NIL))) (DEFTHM STR::DOWNCASE-CHARLIST-OF-CONS (EQUAL (STR::DOWNCASE-CHARLIST (CONS A X)) (CONS (STR::DOWNCASE-CHAR A) (STR::DOWNCASE-CHARLIST X)))) (DEFCONG STR::ICHARLISTEQV EQUAL (STR::DOWNCASE-CHARLIST X) 1 :HINTS (("Goal" :IN-THEORY (ENABLE STR::ICHARLISTEQV)))) (DEFTHM STR::CHARACTER-LISTP-DOWNCASE-CHARLIST (CHARACTER-LISTP (STR::DOWNCASE-CHARLIST X))) (DEFTHM STR::CONSP-OF-DOWNCASE-CHARLIST (EQUAL (CONSP (STR::DOWNCASE-CHARLIST X)) (CONSP X))) (DEFTHM STR::DOWNCASE-CHARLIST-UNDER-IFF (IFF (STR::DOWNCASE-CHARLIST X) (CONSP X)) :HINTS (("Goal" :IN-THEORY (ENABLE STR::DOWNCASE-CHARLIST)))) (DEFTHM STR::LEN-OF-DOWNCASE-CHARLIST (EQUAL (LEN (STR::DOWNCASE-CHARLIST X)) (LEN X))) (DEFTHM STR::DOWNCASE-CHARLIST-AUX-IS-DOWNCASE-CHARLIST (EQUAL (STR::DOWNCASE-CHARLIST-AUX X STR::ACC) (REVAPPEND (STR::DOWNCASE-CHARLIST X) STR::ACC))) (DEFTHM STR::DOWNCASE-CHARLIST-DOES-NOTHING-UNLESS-CHARLIST-HAS-SOME-UP-ALPHA-P (IMPLIES (AND (NOT (STR::CHARLIST-HAS-SOME-UP-ALPHA-P X)) (CHARACTER-LISTP X)) (EQUAL (STR::DOWNCASE-CHARLIST X) X))) (VERIFY-GUARDS STR::DOWNCASE-CHARLIST) (DEFTHM STR::STRING-DOWNCASE1-REDEF (EQUAL (STRING-DOWNCASE1 X) (STR::DOWNCASE-CHARLIST (DOUBLE-REWRITE X))))) (WITH-OUTPUT :STACK :PUSH :OFF :ALL :ON ERROR (PROGN (TABLE INTRO-TABLE :MARK (QUOTE STR::DOWNCASE-CHARLIST)) (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (DEFUND STR::CHARLIST-HAS-SOME-UP-ALPHA-P (X) (DECLARE (XARGS :GUARD (CHARACTER-LISTP X))) (IF (ATOM X) NIL (OR (STR::UP-ALPHA-P (CAR X)) (STR::CHARLIST-HAS-SOME-UP-ALPHA-P (CDR X))))) (DEFUND STR::DOWNCASE-CHARLIST-AUX (X STR::ACC) (DECLARE (XARGS :GUARD (AND (CHARACTER-LISTP X) (CHARACTER-LISTP STR::ACC)))) (IF (ATOM X) STR::ACC (STR::DOWNCASE-CHARLIST-AUX (CDR X) (CONS (STR::DOWNCASE-CHAR (CAR X)) STR::ACC)))) (DEFUND STR::DOWNCASE-CHARLIST (X) (DECLARE (XARGS :GUARD (CHARACTER-LISTP X) :VERIFY-GUARDS NIL)) (MBE :LOGIC (IF (ATOM X) NIL (CONS (STR::DOWNCASE-CHAR (CAR X)) (STR::DOWNCASE-CHARLIST (CDR X)))) :EXEC (IF (STR::CHARLIST-HAS-SOME-UP-ALPHA-P X) (REVERSE (STR::DOWNCASE-CHARLIST-AUX X NIL)) X))) (LOCAL (IN-THEORY (ENABLE STR::DOWNCASE-CHARLIST STR::DOWNCASE-CHARLIST-AUX STR::CHARLIST-HAS-SOME-UP-ALPHA-P))) (DEFTHM STR::DOWNCASE-CHARLIST-WHEN-ATOM (IMPLIES (ATOM X) (EQUAL (STR::DOWNCASE-CHARLIST X) NIL))) (DEFTHM STR::DOWNCASE-CHARLIST-OF-CONS (EQUAL (STR::DOWNCASE-CHARLIST (CONS A X)) (CONS (STR::DOWNCASE-CHAR A) (STR::DOWNCASE-CHARLIST X)))) (DEFCONG STR::ICHARLISTEQV EQUAL (STR::DOWNCASE-CHARLIST X) 1 :HINTS (("Goal" :IN-THEORY (ENABLE STR::ICHARLISTEQV)))) (DEFTHM STR::CHARACTER-LISTP-DOWNCASE-CHARLIST (CHARACTER-LISTP (STR::DOWNCASE-CHARLIST X))) (DEFTHM STR::CONSP-OF-DOWNCASE-CHARLIST (EQUAL (CONSP (STR::DOWNCASE-CHARLIST X)) (CONSP X))) (DEFTHM STR::DOWNCASE-CHARLIST-UNDER-IFF (IFF (STR::DOWNCASE-CHARLIST X) (CONSP X)) :HINTS (("Goal" :IN-THEORY (ENABLE STR::DOWNCASE-CHARLIST)))) (DEFTHM STR::LEN-OF-DOWNCASE-CHARLIST (EQUAL (LEN (STR::DOWNCASE-CHARLIST X)) (LEN X))) (DEFTHM STR::DOWNCASE-CHARLIST-AUX-IS-DOWNCASE-CHARLIST (EQUAL (STR::DOWNCASE-CHARLIST-AUX X STR::ACC) (REVAPPEND (STR::DOWNCASE-CHARLIST X) STR::ACC))) (DEFTHM STR::DOWNCASE-CHARLIST-DOES-NOTHING-UNLESS-CHARLIST-HAS-SOME-UP-ALPHA-P (IMPLIES (AND (NOT (STR::CHARLIST-HAS-SOME-UP-ALPHA-P X)) (CHARACTER-LISTP X)) (EQUAL (STR::DOWNCASE-CHARLIST X) X))) (VERIFY-GUARDS STR::DOWNCASE-CHARLIST) (DEFTHM STR::STRING-DOWNCASE1-REDEF (EQUAL (STRING-DOWNCASE1 X) (STR::DOWNCASE-CHARLIST (DOUBLE-REWRITE X)))))) (RECORD-EXPANSION (MAKE-EVENT (LET* ((XDOC::NAME (QUOTE STR::DOWNCASE-CHARLIST)) (XDOC::PARENTS (QUOTE (STR::CASES))) (XDOC::SHORT (QUOTE "Convert every character in a list to lower case.")) (XDOC::EXTENSION (QUOTE NIL)) (XDOC::WRLD (W STATE)) (XDOC::TRIPS (REVERSED-WORLD-SINCE-EVENT XDOC::WRLD (QUOTE (TABLE INTRO-TABLE :MARK (QUOTE STR::DOWNCASE-CHARLIST))) NIL)) (XDOC::INFO (REVERSE (NEW-FORMULA-INFO XDOC::TRIPS XDOC::WRLD NIL))) (XDOC::AUTODOC (XDOC::FORMULA-INFO-TO-DEFS (NOT XDOC::EXTENSION) XDOC::INFO)) (XDOC::LONG (CONCATENATE (QUOTE STRING) (QUOTE "<p>@(call downcase-charlist) maps @(see downcase-char) across a
character list.</p>

<p>ACL2 has a built-in alternative to this function, @('string-downcase1'), but
it is irritating to use because it has @(see standard-char-p) guards.  In
contrast, @('downcase-charlist') works on arbitrary characters.</p>

<p>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.</p>") (COERCE (LIST #\Newline #\Newline) (QUOTE STRING)) XDOC::AUTODOC))) (IF XDOC::EXTENSION (CONS (QUOTE XDOC-EXTEND) (CONS XDOC::EXTENSION (CONS XDOC::LONG (QUOTE NIL)))) (CONS (QUOTE DEFXDOC) (CONS XDOC::NAME (CONS (QUOTE :PARENTS) (CONS XDOC::PARENTS (CONS (QUOTE :SHORT) (CONS XDOC::SHORT (CONS (QUOTE :LONG) (CONS XDOC::LONG (QUOTE NIL)))))))))))) (WITH-OUTPUT :OFF (EVENT SUMMARY) (PROGN (TABLE XDOC (QUOTE DOC) (CONS (QUOTE ((:NAME . STR::DOWNCASE-CHARLIST) (:BASE-PKG . STR::ACL2-PKG-WITNESS) (:PARENTS STR::CASES) (:SHORT . "Convert every character in a list to lower case.") (:LONG . "<p>@(call downcase-charlist) maps @(see downcase-char) across a
character list.</p>

<p>ACL2 has a built-in alternative to this function, @('string-downcase1'), but
it is irritating to use because it has @(see standard-char-p) guards.  In
contrast, @('downcase-charlist') works on arbitrary characters.</p>

<p>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.</p>

<h3>Definitions and Theorems</h3>@(def |STR|::|CHARLIST-HAS-SOME-UP-ALPHA-P|)
@(def |STR|::|DOWNCASE-CHARLIST-AUX|)
@(def |STR|::|DOWNCASE-CHARLIST|)
@(def |STR|::|DOWNCASE-CHARLIST-WHEN-ATOM|)
@(def |STR|::|DOWNCASE-CHARLIST-OF-CONS|)
@(def |STR|::|ICHARLISTEQV-IMPLIES-EQUAL-DOWNCASE-CHARLIST-1|)
@(def |STR|::|CHARACTER-LISTP-DOWNCASE-CHARLIST|)
@(def |STR|::|CONSP-OF-DOWNCASE-CHARLIST|)
@(def |STR|::|DOWNCASE-CHARLIST-UNDER-IFF|)
@(def |STR|::|LEN-OF-DOWNCASE-CHARLIST|)
@(def |STR|::|DOWNCASE-CHARLIST-AUX-IS-DOWNCASE-CHARLIST|)
@(def |STR|::|DOWNCASE-CHARLIST-DOES-NOTHING-UNLESS-CHARLIST-HAS-SOME-UP-ALPHA-P|)
@(def |STR|::|STRING-DOWNCASE1-REDEF|)") (:FROM . "[books]/str/case-conversion.lisp"))) (XDOC::GET-XDOC-TABLE WORLD))) (VALUE-TRIPLE (QUOTE (DEFXDOC STR::DOWNCASE-CHARLIST)))))) (VALUE-TRIPLE (QUOTE STR::DOWNCASE-CHARLIST))))) (8 RECORD-EXPANSION (DEFSECTION STR::UPCASE-STRING :PARENTS (STR::CASES STRING-UPCASE) :SHORT "Convert a string to upper case." :LONG "<p>@(call upcase-string) converts a string to upper case, effectively
by transforming each of its characters with @(see upcase-char).</p>

<p>ACL2 has a built-in alternative to this function, @(see
acl2::string-upcase), but it is irritating to use because it has @(see
standard-char-p) guards.  In contrast, @('upcase-string') works on strings with
arbitrary characters.</p>

<p>We try to make this fast.  For 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.</p>

<p>Despite trying to make this fast, the builtin @('string-upcase') can really
outperform us since it doesn't have to build the intermediate list, etc.  It's
really a shame that @('string-upcase') has such a terrible guard.  Well, at
least we're better when no work needs to be done:</p>

@({
    (time (loop for i fixnum from 1 to 1000000 do
            (str::upcase-string \"Hello, World!\")))  ;; 1.2 seconds, 336 MB
    (time (loop for i fixnum from 1 to 1000000 do
            (string-upcase \"Hello, World!\")))       ;; .26 seconds, 64 MB

    (time (loop for i fixnum from 1 to 1000000 do
            (str::upcase-string \"HELLO, WORLD!\")))  ;; .15 seconds, 0 MB
    (time (loop for i fixnum from 1 to 1000000 do
            (string-upcase \"HELLO, WORLD!\")))       ;; .23 seconds, 64 MB
})" (DEFUND STR::STRING-HAS-SOME-DOWN-ALPHA-P (X N STR::XL) (DECLARE (TYPE STRING X) (TYPE INTEGER N) (TYPE INTEGER STR::XL) (XARGS :GUARD (AND (STRINGP X) (NATP N) (NATP STR::XL) (= STR::XL (LENGTH X)) (<= N STR::XL)) :MEASURE (NFIX (- (NFIX STR::XL) (NFIX N))))) (IF (MBE :LOGIC (ZP (- (NFIX STR::XL) (NFIX N))) :EXEC (INT= N STR::XL)) NIL (OR (STR::DOWN-ALPHA-P (CHAR X N)) (STR::STRING-HAS-SOME-DOWN-ALPHA-P X (+ 1 (LNFIX N)) STR::XL)))) (DEFUND STR::UPCASE-STRING-AUX (X N STR::XL STR::ACC) (DECLARE (TYPE STRING X) (TYPE INTEGER N) (TYPE INTEGER STR::XL) (XARGS :GUARD (AND (STRINGP X) (NATP N) (NATP STR::XL) (= STR::XL (LENGTH X)) (<= N STR::XL)) :MEASURE (NFIX (- (NFIX STR::XL) (NFIX N))))) (IF (MBE :LOGIC (ZP (- (NFIX STR::XL) (NFIX N))) :EXEC (INT= N STR::XL)) STR::ACC (LET* ((CHAR (CHAR X N)) (STR::UPCHAR (STR::UPCASE-CHAR CHAR))) (STR::UPCASE-STRING-AUX X (+ 1 (LNFIX N)) STR::XL (CONS STR::UPCHAR STR::ACC))))) (DEFUND STR::UPCASE-STRING (X) (DECLARE (TYPE STRING X) (XARGS :VERIFY-GUARDS NIL)) (MBE :LOGIC (IMPLODE (STR::UPCASE-CHARLIST (EXPLODE X))) :EXEC (LET ((STR::XL (LENGTH X))) (IF (NOT (STR::STRING-HAS-SOME-DOWN-ALPHA-P X 0 STR::XL)) X (STR::RCHARS-TO-STRING (STR::UPCASE-STRING-AUX X 0 STR::XL NIL)))))) (LOCAL (IN-THEORY (ENABLE STR::UPCASE-STRING))) (DEFTHM STR::STRING-HAS-SOME-DOWN-ALPHA-P-REDEF (IMPLIES (AND (STRINGP X) (NATP N) (NATP STR::XL) (= STR::XL (LENGTH X)) (<= N STR::XL)) (EQUAL (STR::STRING-HAS-SOME-DOWN-ALPHA-P X N STR::XL) (STR::CHARLIST-HAS-SOME-DOWN-ALPHA-P (NTHCDR N (EXPLODE X))))) :HINTS (("Goal" :IN-THEORY (ENABLE STR::STRING-HAS-SOME-DOWN-ALPHA-P STR::CHARLIST-HAS-SOME-DOWN-ALPHA-P)))) (DEFTHM STR::UPCASE-STRING-AUX-REDEF (IMPLIES (AND (STRINGP X) (NATP N) (NATP STR::XL) (= STR::XL (LENGTH X)) (<= N STR::XL)) (EQUAL (STR::UPCASE-STRING-AUX X N STR::XL STR::ACC) (REVAPPEND (STR::UPCASE-CHARLIST (NTHCDR N (EXPLODE X))) STR::ACC))) :HINTS (("Goal" :IN-THEORY (ENABLE STR::UPCASE-STRING-AUX STR::UPCASE-CHARLIST)))) (VERIFY-GUARDS STR::UPCASE-STRING) (DEFCONG STR::ISTREQV EQUAL (STR::UPCASE-STRING X) 1) (DEFTHM STR::LEN-OF-UPCASE-STRING (EQUAL (LEN (EXPLODE (STR::UPCASE-STRING X))) (LEN (EXPLODE X)))) (DEFTHM STR::LENGTH-OF-UPCASE-STRING (EQUAL (LENGTH (STR::UPCASE-STRING X)) (LEN (EXPLODE X)))) (DEFTHM STR::EQUAL-OF-EMPTY-STRING-WITH-UPCASE-STRING (EQUAL (EQUAL "" (STR::UPCASE-STRING X)) (ATOM (EXPLODE X)))) (DEFTHM STR::STRING-UPCASE-IS-UPCASE-STRING (EQUAL (STRING-UPCASE X) (STR::UPCASE-STRING (DOUBLE-REWRITE X))))) (WITH-OUTPUT :STACK :PUSH :OFF :ALL :ON ERROR (PROGN (TABLE INTRO-TABLE :MARK (QUOTE STR::UPCASE-STRING)) (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (DEFUND STR::STRING-HAS-SOME-DOWN-ALPHA-P (X N STR::XL) (DECLARE (TYPE STRING X) (TYPE INTEGER N) (TYPE INTEGER STR::XL) (XARGS :GUARD (AND (STRINGP X) (NATP N) (NATP STR::XL) (= STR::XL (LENGTH X)) (<= N STR::XL)) :MEASURE (NFIX (- (NFIX STR::XL) (NFIX N))))) (IF (MBE :LOGIC (ZP (- (NFIX STR::XL) (NFIX N))) :EXEC (INT= N STR::XL)) NIL (OR (STR::DOWN-ALPHA-P (CHAR X N)) (STR::STRING-HAS-SOME-DOWN-ALPHA-P X (+ 1 (LNFIX N)) STR::XL)))) (DEFUND STR::UPCASE-STRING-AUX (X N STR::XL STR::ACC) (DECLARE (TYPE STRING X) (TYPE INTEGER N) (TYPE INTEGER STR::XL) (XARGS :GUARD (AND (STRINGP X) (NATP N) (NATP STR::XL) (= STR::XL (LENGTH X)) (<= N STR::XL)) :MEASURE (NFIX (- (NFIX STR::XL) (NFIX N))))) (IF (MBE :LOGIC (ZP (- (NFIX STR::XL) (NFIX N))) :EXEC (INT= N STR::XL)) STR::ACC (LET* ((CHAR (CHAR X N)) (STR::UPCHAR (STR::UPCASE-CHAR CHAR))) (STR::UPCASE-STRING-AUX X (+ 1 (LNFIX N)) STR::XL (CONS STR::UPCHAR STR::ACC))))) (DEFUND STR::UPCASE-STRING (X) (DECLARE (TYPE STRING X) (XARGS :VERIFY-GUARDS NIL)) (MBE :LOGIC (IMPLODE (STR::UPCASE-CHARLIST (EXPLODE X))) :EXEC (LET ((STR::XL (LENGTH X))) (IF (NOT (STR::STRING-HAS-SOME-DOWN-ALPHA-P X 0 STR::XL)) X (STR::RCHARS-TO-STRING (STR::UPCASE-STRING-AUX X 0 STR::XL NIL)))))) (LOCAL (IN-THEORY (ENABLE STR::UPCASE-STRING))) (DEFTHM STR::STRING-HAS-SOME-DOWN-ALPHA-P-REDEF (IMPLIES (AND (STRINGP X) (NATP N) (NATP STR::XL) (= STR::XL (LENGTH X)) (<= N STR::XL)) (EQUAL (STR::STRING-HAS-SOME-DOWN-ALPHA-P X N STR::XL) (STR::CHARLIST-HAS-SOME-DOWN-ALPHA-P (NTHCDR N (EXPLODE X))))) :HINTS (("Goal" :IN-THEORY (ENABLE STR::STRING-HAS-SOME-DOWN-ALPHA-P STR::CHARLIST-HAS-SOME-DOWN-ALPHA-P)))) (DEFTHM STR::UPCASE-STRING-AUX-REDEF (IMPLIES (AND (STRINGP X) (NATP N) (NATP STR::XL) (= STR::XL (LENGTH X)) (<= N STR::XL)) (EQUAL (STR::UPCASE-STRING-AUX X N STR::XL STR::ACC) (REVAPPEND (STR::UPCASE-CHARLIST (NTHCDR N (EXPLODE X))) STR::ACC))) :HINTS (("Goal" :IN-THEORY (ENABLE STR::UPCASE-STRING-AUX STR::UPCASE-CHARLIST)))) (VERIFY-GUARDS STR::UPCASE-STRING) (DEFCONG STR::ISTREQV EQUAL (STR::UPCASE-STRING X) 1) (DEFTHM STR::LEN-OF-UPCASE-STRING (EQUAL (LEN (EXPLODE (STR::UPCASE-STRING X))) (LEN (EXPLODE X)))) (DEFTHM STR::LENGTH-OF-UPCASE-STRING (EQUAL (LENGTH (STR::UPCASE-STRING X)) (LEN (EXPLODE X)))) (DEFTHM STR::EQUAL-OF-EMPTY-STRING-WITH-UPCASE-STRING (EQUAL (EQUAL "" (STR::UPCASE-STRING X)) (ATOM (EXPLODE X)))) (DEFTHM STR::STRING-UPCASE-IS-UPCASE-STRING (EQUAL (STRING-UPCASE X) (STR::UPCASE-STRING (DOUBLE-REWRITE X)))))) (RECORD-EXPANSION (MAKE-EVENT (LET* ((XDOC::NAME (QUOTE STR::UPCASE-STRING)) (XDOC::PARENTS (QUOTE (STR::CASES STRING-UPCASE))) (XDOC::SHORT (QUOTE "Convert a string to upper case.")) (XDOC::EXTENSION (QUOTE NIL)) (XDOC::WRLD (W STATE)) (XDOC::TRIPS (REVERSED-WORLD-SINCE-EVENT XDOC::WRLD (QUOTE (TABLE INTRO-TABLE :MARK (QUOTE STR::UPCASE-STRING))) NIL)) (XDOC::INFO (REVERSE (NEW-FORMULA-INFO XDOC::TRIPS XDOC::WRLD NIL))) (XDOC::AUTODOC (XDOC::FORMULA-INFO-TO-DEFS (NOT XDOC::EXTENSION) XDOC::INFO)) (XDOC::LONG (CONCATENATE (QUOTE STRING) (QUOTE "<p>@(call upcase-string) converts a string to upper case, effectively
by transforming each of its characters with @(see upcase-char).</p>

<p>ACL2 has a built-in alternative to this function, @(see
acl2::string-upcase), but it is irritating to use because it has @(see
standard-char-p) guards.  In contrast, @('upcase-string') works on strings with
arbitrary characters.</p>

<p>We try to make this fast.  For 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.</p>

<p>Despite trying to make this fast, the builtin @('string-upcase') can really
outperform us since it doesn't have to build the intermediate list, etc.  It's
really a shame that @('string-upcase') has such a terrible guard.  Well, at
least we're better when no work needs to be done:</p>

@({
    (time (loop for i fixnum from 1 to 1000000 do
            (str::upcase-string \"Hello, World!\")))  ;; 1.2 seconds, 336 MB
    (time (loop for i fixnum from 1 to 1000000 do
            (string-upcase \"Hello, World!\")))       ;; .26 seconds, 64 MB

    (time (loop for i fixnum from 1 to 1000000 do
            (str::upcase-string \"HELLO, WORLD!\")))  ;; .15 seconds, 0 MB
    (time (loop for i fixnum from 1 to 1000000 do
            (string-upcase \"HELLO, WORLD!\")))       ;; .23 seconds, 64 MB
})") (COERCE (LIST #\Newline #\Newline) (QUOTE STRING)) XDOC::AUTODOC))) (IF XDOC::EXTENSION (CONS (QUOTE XDOC-EXTEND) (CONS XDOC::EXTENSION (CONS XDOC::LONG (QUOTE NIL)))) (CONS (QUOTE DEFXDOC) (CONS XDOC::NAME (CONS (QUOTE :PARENTS) (CONS XDOC::PARENTS (CONS (QUOTE :SHORT) (CONS XDOC::SHORT (CONS (QUOTE :LONG) (CONS XDOC::LONG (QUOTE NIL)))))))))))) (WITH-OUTPUT :OFF (EVENT SUMMARY) (PROGN (TABLE XDOC (QUOTE DOC) (CONS (QUOTE ((:NAME . STR::UPCASE-STRING) (:BASE-PKG . STR::ACL2-PKG-WITNESS) (:PARENTS STR::CASES STRING-UPCASE) (:SHORT . "Convert a string to upper case.") (:LONG . "<p>@(call upcase-string) converts a string to upper case, effectively
by transforming each of its characters with @(see upcase-char).</p>

<p>ACL2 has a built-in alternative to this function, @(see
acl2::string-upcase), but it is irritating to use because it has @(see
standard-char-p) guards.  In contrast, @('upcase-string') works on strings with
arbitrary characters.</p>

<p>We try to make this fast.  For 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.</p>

<p>Despite trying to make this fast, the builtin @('string-upcase') can really
outperform us since it doesn't have to build the intermediate list, etc.  It's
really a shame that @('string-upcase') has such a terrible guard.  Well, at
least we're better when no work needs to be done:</p>

@({
    (time (loop for i fixnum from 1 to 1000000 do
            (str::upcase-string \"Hello, World!\")))  ;; 1.2 seconds, 336 MB
    (time (loop for i fixnum from 1 to 1000000 do
            (string-upcase \"Hello, World!\")))       ;; .26 seconds, 64 MB

    (time (loop for i fixnum from 1 to 1000000 do
            (str::upcase-string \"HELLO, WORLD!\")))  ;; .15 seconds, 0 MB
    (time (loop for i fixnum from 1 to 1000000 do
            (string-upcase \"HELLO, WORLD!\")))       ;; .23 seconds, 64 MB
})

<h3>Definitions and Theorems</h3>@(def |STR|::|STRING-HAS-SOME-DOWN-ALPHA-P|)
@(def |STR|::|UPCASE-STRING-AUX|)
@(def |STR|::|UPCASE-STRING|)
@(def |STR|::|STRING-HAS-SOME-DOWN-ALPHA-P-REDEF|)
@(def |STR|::|UPCASE-STRING-AUX-REDEF|)
@(def |STR|::|ISTREQV-IMPLIES-EQUAL-UPCASE-STRING-1|)
@(def |STR|::|LEN-OF-UPCASE-STRING|)
@(def |STR|::|LENGTH-OF-UPCASE-STRING|)
@(def |STR|::|EQUAL-OF-EMPTY-STRING-WITH-UPCASE-STRING|)
@(def |STR|::|STRING-UPCASE-IS-UPCASE-STRING|)") (:FROM . "[books]/str/case-conversion.lisp"))) (XDOC::GET-XDOC-TABLE WORLD))) (VALUE-TRIPLE (QUOTE (DEFXDOC STR::UPCASE-STRING)))))) (VALUE-TRIPLE (QUOTE STR::UPCASE-STRING))))) (9 RECORD-EXPANSION (DEFSECTION STR::DOWNCASE-STRING :PARENTS (STR::CASES STRING-DOWNCASE) :SHORT "Convert a string to lower case." :LONG "<p>@(call downcase-string) converts a string to lower case,
effectively by transforming each of its characters with @(see
downcase-char).</p>

<p>ACL2 has a built-in alternative to this function, @(see
acl2::string-downcase), but it is irritating to use because it has @(see
standard-char-p) guards.  In contrast, @('downcase-string') works on strings
with arbitrary characters.</p>

<p>See also @(see upcase-string), which has more discussion on how we try to
make this fast.</p>" (DEFUND STR::STRING-HAS-SOME-UP-ALPHA-P (X N STR::XL) (DECLARE (TYPE STRING X) (TYPE INTEGER N) (TYPE INTEGER STR::XL) (XARGS :GUARD (AND (STRINGP X) (NATP N) (NATP STR::XL) (= STR::XL (LENGTH X)) (<= N STR::XL)) :MEASURE (NFIX (- (NFIX STR::XL) (NFIX N))))) (IF (MBE :LOGIC (ZP (- (NFIX STR::XL) (NFIX N))) :EXEC (INT= N STR::XL)) NIL (OR (STR::UP-ALPHA-P (CHAR X N)) (STR::STRING-HAS-SOME-UP-ALPHA-P X (+ 1 (LNFIX N)) STR::XL)))) (DEFUND STR::DOWNCASE-STRING-AUX (X N STR::XL STR::ACC) (DECLARE (TYPE STRING X) (TYPE INTEGER N) (TYPE INTEGER STR::XL) (XARGS :GUARD (AND (STRINGP X) (NATP N) (NATP STR::XL) (= STR::XL (LENGTH X)) (<= N STR::XL)) :MEASURE (NFIX (- (NFIX STR::XL) (NFIX N))))) (IF (MBE :LOGIC (ZP (- (NFIX STR::XL) (NFIX N))) :EXEC (INT= N STR::XL)) STR::ACC (LET* ((CHAR (CHAR X N)) (STR::DOWNCHAR (STR::DOWNCASE-CHAR CHAR))) (STR::DOWNCASE-STRING-AUX X (+ 1 (LNFIX N)) STR::XL (CONS STR::DOWNCHAR STR::ACC))))) (DEFUND STR::DOWNCASE-STRING (X) (DECLARE (TYPE STRING X) (XARGS :VERIFY-GUARDS NIL)) (MBE :LOGIC (IMPLODE (STR::DOWNCASE-CHARLIST (EXPLODE X))) :EXEC (LET ((STR::XL (LENGTH X))) (IF (NOT (STR::STRING-HAS-SOME-UP-ALPHA-P X 0 STR::XL)) X (STR::RCHARS-TO-STRING (STR::DOWNCASE-STRING-AUX X 0 STR::XL NIL)))))) (LOCAL (IN-THEORY (ENABLE STR::DOWNCASE-STRING))) (DEFTHM STR::STRING-HAS-SOME-UP-ALPHA-P-REDEF (IMPLIES (AND (STRINGP X) (NATP N) (NATP STR::XL) (= STR::XL (LENGTH X)) (<= N STR::XL)) (EQUAL (STR::STRING-HAS-SOME-UP-ALPHA-P X N STR::XL) (STR::CHARLIST-HAS-SOME-UP-ALPHA-P (NTHCDR N (EXPLODE X))))) :HINTS (("Goal" :IN-THEORY (ENABLE STR::STRING-HAS-SOME-UP-ALPHA-P STR::CHARLIST-HAS-SOME-UP-ALPHA-P)))) (DEFTHM STR::DOWNCASE-STRING-AUX-REDEF (IMPLIES (AND (STRINGP X) (NATP N) (NATP STR::XL) (= STR::XL (LENGTH X)) (<= N STR::XL)) (EQUAL (STR::DOWNCASE-STRING-AUX X N STR::XL STR::ACC) (REVAPPEND (STR::DOWNCASE-CHARLIST (NTHCDR N (EXPLODE X))) STR::ACC))) :HINTS (("Goal" :IN-THEORY (ENABLE STR::DOWNCASE-STRING-AUX STR::DOWNCASE-CHARLIST)))) (VERIFY-GUARDS STR::DOWNCASE-STRING) (DEFCONG STR::ISTREQV EQUAL (STR::DOWNCASE-STRING X) 1) (DEFTHM STR::LEN-OF-DOWNCASE-STRING (EQUAL (LEN (EXPLODE (STR::DOWNCASE-STRING X))) (LEN (EXPLODE X)))) (DEFTHM STR::LENGTH-OF-DOWNCASE-STRING (EQUAL (LENGTH (STR::DOWNCASE-STRING X)) (LEN (EXPLODE X)))) (DEFTHM STR::EQUAL-OF-EMPTY-STRING-WITH-DOWNCASE-STRING (EQUAL (EQUAL "" (STR::DOWNCASE-STRING X)) (ATOM (EXPLODE X)))) (DEFTHM STR::STRING-DOWNCASE-IS-DOWNCASE-STRING (EQUAL (STRING-DOWNCASE X) (STR::DOWNCASE-STRING (DOUBLE-REWRITE X))))) (WITH-OUTPUT :STACK :PUSH :OFF :ALL :ON ERROR (PROGN (TABLE INTRO-TABLE :MARK (QUOTE STR::DOWNCASE-STRING)) (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (DEFUND STR::STRING-HAS-SOME-UP-ALPHA-P (X N STR::XL) (DECLARE (TYPE STRING X) (TYPE INTEGER N) (TYPE INTEGER STR::XL) (XARGS :GUARD (AND (STRINGP X) (NATP N) (NATP STR::XL) (= STR::XL (LENGTH X)) (<= N STR::XL)) :MEASURE (NFIX (- (NFIX STR::XL) (NFIX N))))) (IF (MBE :LOGIC (ZP (- (NFIX STR::XL) (NFIX N))) :EXEC (INT= N STR::XL)) NIL (OR (STR::UP-ALPHA-P (CHAR X N)) (STR::STRING-HAS-SOME-UP-ALPHA-P X (+ 1 (LNFIX N)) STR::XL)))) (DEFUND STR::DOWNCASE-STRING-AUX (X N STR::XL STR::ACC) (DECLARE (TYPE STRING X) (TYPE INTEGER N) (TYPE INTEGER STR::XL) (XARGS :GUARD (AND (STRINGP X) (NATP N) (NATP STR::XL) (= STR::XL (LENGTH X)) (<= N STR::XL)) :MEASURE (NFIX (- (NFIX STR::XL) (NFIX N))))) (IF (MBE :LOGIC (ZP (- (NFIX STR::XL) (NFIX N))) :EXEC (INT= N STR::XL)) STR::ACC (LET* ((CHAR (CHAR X N)) (STR::DOWNCHAR (STR::DOWNCASE-CHAR CHAR))) (STR::DOWNCASE-STRING-AUX X (+ 1 (LNFIX N)) STR::XL (CONS STR::DOWNCHAR STR::ACC))))) (DEFUND STR::DOWNCASE-STRING (X) (DECLARE (TYPE STRING X) (XARGS :VERIFY-GUARDS NIL)) (MBE :LOGIC (IMPLODE (STR::DOWNCASE-CHARLIST (EXPLODE X))) :EXEC (LET ((STR::XL (LENGTH X))) (IF (NOT (STR::STRING-HAS-SOME-UP-ALPHA-P X 0 STR::XL)) X (STR::RCHARS-TO-STRING (STR::DOWNCASE-STRING-AUX X 0 STR::XL NIL)))))) (LOCAL (IN-THEORY (ENABLE STR::DOWNCASE-STRING))) (DEFTHM STR::STRING-HAS-SOME-UP-ALPHA-P-REDEF (IMPLIES (AND (STRINGP X) (NATP N) (NATP STR::XL) (= STR::XL (LENGTH X)) (<= N STR::XL)) (EQUAL (STR::STRING-HAS-SOME-UP-ALPHA-P X N STR::XL) (STR::CHARLIST-HAS-SOME-UP-ALPHA-P (NTHCDR N (EXPLODE X))))) :HINTS (("Goal" :IN-THEORY (ENABLE STR::STRING-HAS-SOME-UP-ALPHA-P STR::CHARLIST-HAS-SOME-UP-ALPHA-P)))) (DEFTHM STR::DOWNCASE-STRING-AUX-REDEF (IMPLIES (AND (STRINGP X) (NATP N) (NATP STR::XL) (= STR::XL (LENGTH X)) (<= N STR::XL)) (EQUAL (STR::DOWNCASE-STRING-AUX X N STR::XL STR::ACC) (REVAPPEND (STR::DOWNCASE-CHARLIST (NTHCDR N (EXPLODE X))) STR::ACC))) :HINTS (("Goal" :IN-THEORY (ENABLE STR::DOWNCASE-STRING-AUX STR::DOWNCASE-CHARLIST)))) (VERIFY-GUARDS STR::DOWNCASE-STRING) (DEFCONG STR::ISTREQV EQUAL (STR::DOWNCASE-STRING X) 1) (DEFTHM STR::LEN-OF-DOWNCASE-STRING (EQUAL (LEN (EXPLODE (STR::DOWNCASE-STRING X))) (LEN (EXPLODE X)))) (DEFTHM STR::LENGTH-OF-DOWNCASE-STRING (EQUAL (LENGTH (STR::DOWNCASE-STRING X)) (LEN (EXPLODE X)))) (DEFTHM STR::EQUAL-OF-EMPTY-STRING-WITH-DOWNCASE-STRING (EQUAL (EQUAL "" (STR::DOWNCASE-STRING X)) (ATOM (EXPLODE X)))) (DEFTHM STR::STRING-DOWNCASE-IS-DOWNCASE-STRING (EQUAL (STRING-DOWNCASE X) (STR::DOWNCASE-STRING (DOUBLE-REWRITE X)))))) (RECORD-EXPANSION (MAKE-EVENT (LET* ((XDOC::NAME (QUOTE STR::DOWNCASE-STRING)) (XDOC::PARENTS (QUOTE (STR::CASES STRING-DOWNCASE))) (XDOC::SHORT (QUOTE "Convert a string to lower case.")) (XDOC::EXTENSION (QUOTE NIL)) (XDOC::WRLD (W STATE)) (XDOC::TRIPS (REVERSED-WORLD-SINCE-EVENT XDOC::WRLD (QUOTE (TABLE INTRO-TABLE :MARK (QUOTE STR::DOWNCASE-STRING))) NIL)) (XDOC::INFO (REVERSE (NEW-FORMULA-INFO XDOC::TRIPS XDOC::WRLD NIL))) (XDOC::AUTODOC (XDOC::FORMULA-INFO-TO-DEFS (NOT XDOC::EXTENSION) XDOC::INFO)) (XDOC::LONG (CONCATENATE (QUOTE STRING) (QUOTE "<p>@(call downcase-string) converts a string to lower case,
effectively by transforming each of its characters with @(see
downcase-char).</p>

<p>ACL2 has a built-in alternative to this function, @(see
acl2::string-downcase), but it is irritating to use because it has @(see
standard-char-p) guards.  In contrast, @('downcase-string') works on strings
with arbitrary characters.</p>

<p>See also @(see upcase-string), which has more discussion on how we try to
make this fast.</p>") (COERCE (LIST #\Newline #\Newline) (QUOTE STRING)) XDOC::AUTODOC))) (IF XDOC::EXTENSION (CONS (QUOTE XDOC-EXTEND) (CONS XDOC::EXTENSION (CONS XDOC::LONG (QUOTE NIL)))) (CONS (QUOTE DEFXDOC) (CONS XDOC::NAME (CONS (QUOTE :PARENTS) (CONS XDOC::PARENTS (CONS (QUOTE :SHORT) (CONS XDOC::SHORT (CONS (QUOTE :LONG) (CONS XDOC::LONG (QUOTE NIL)))))))))))) (WITH-OUTPUT :OFF (EVENT SUMMARY) (PROGN (TABLE XDOC (QUOTE DOC) (CONS (QUOTE ((:NAME . STR::DOWNCASE-STRING) (:BASE-PKG . STR::ACL2-PKG-WITNESS) (:PARENTS STR::CASES STRING-DOWNCASE) (:SHORT . "Convert a string to lower case.") (:LONG . "<p>@(call downcase-string) converts a string to lower case,
effectively by transforming each of its characters with @(see
downcase-char).</p>

<p>ACL2 has a built-in alternative to this function, @(see
acl2::string-downcase), but it is irritating to use because it has @(see
standard-char-p) guards.  In contrast, @('downcase-string') works on strings
with arbitrary characters.</p>

<p>See also @(see upcase-string), which has more discussion on how we try to
make this fast.</p>

<h3>Definitions and Theorems</h3>@(def |STR|::|STRING-HAS-SOME-UP-ALPHA-P|)
@(def |STR|::|DOWNCASE-STRING-AUX|)
@(def |STR|::|DOWNCASE-STRING|)
@(def |STR|::|STRING-HAS-SOME-UP-ALPHA-P-REDEF|)
@(def |STR|::|DOWNCASE-STRING-AUX-REDEF|)
@(def |STR|::|ISTREQV-IMPLIES-EQUAL-DOWNCASE-STRING-1|)
@(def |STR|::|LEN-OF-DOWNCASE-STRING|)
@(def |STR|::|LENGTH-OF-DOWNCASE-STRING|)
@(def |STR|::|EQUAL-OF-EMPTY-STRING-WITH-DOWNCASE-STRING|)
@(def |STR|::|STRING-DOWNCASE-IS-DOWNCASE-STRING|)") (:FROM . "[books]/str/case-conversion.lisp"))) (XDOC::GET-XDOC-TABLE WORLD))) (VALUE-TRIPLE (QUOTE (DEFXDOC STR::DOWNCASE-STRING)))))) (VALUE-TRIPLE (QUOTE STR::DOWNCASE-STRING))))) (10 RECORD-EXPANSION (DEFSECTION STR::UPCASE-STRING-LIST :PARENTS (STR::CASES) :SHORT "Convert every string in a list to upper case." (DEFUND STR::UPCASE-STRING-LIST-AUX (X STR::ACC) (DECLARE (XARGS :GUARD (AND (STRING-LISTP X) (STRING-LISTP STR::ACC)))) (IF (ATOM X) STR::ACC (STR::UPCASE-STRING-LIST-AUX (CDR X) (CONS (STR::UPCASE-STRING (CAR X)) STR::ACC)))) (DEFUND STR::UPCASE-STRING-LIST (X) (DECLARE (XARGS :GUARD (STRING-LISTP X) :VERIFY-GUARDS NIL)) (MBE :LOGIC (IF (ATOM X) NIL (CONS (STR::UPCASE-STRING (CAR X)) (STR::UPCASE-STRING-LIST (CDR X)))) :EXEC (REVERSE (STR::UPCASE-STRING-LIST-AUX X NIL)))) (LOCAL (IN-THEORY (ENABLE STR::UPCASE-STRING-LIST-AUX STR::UPCASE-STRING-LIST))) (DEFTHM STR::STRING-LISTP-UPCASE-STRING-LIST (STRING-LISTP (STR::UPCASE-STRING-LIST X))) (DEFTHM STR::UPCASE-STRING-LIST-AUX-IS-UPCASE-STRING-LIST (EQUAL (STR::UPCASE-STRING-LIST-AUX X STR::ACC) (REVAPPEND (STR::UPCASE-STRING-LIST X) STR::ACC))) (VERIFY-GUARDS STR::UPCASE-STRING-LIST)) (WITH-OUTPUT :STACK :PUSH :OFF :ALL :ON ERROR (PROGN (TABLE INTRO-TABLE :MARK (QUOTE STR::UPCASE-STRING-LIST)) (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (DEFUND STR::UPCASE-STRING-LIST-AUX (X STR::ACC) (DECLARE (XARGS :GUARD (AND (STRING-LISTP X) (STRING-LISTP STR::ACC)))) (IF (ATOM X) STR::ACC (STR::UPCASE-STRING-LIST-AUX (CDR X) (CONS (STR::UPCASE-STRING (CAR X)) STR::ACC)))) (DEFUND STR::UPCASE-STRING-LIST (X) (DECLARE (XARGS :GUARD (STRING-LISTP X) :VERIFY-GUARDS NIL)) (MBE :LOGIC (IF (ATOM X) NIL (CONS (STR::UPCASE-STRING (CAR X)) (STR::UPCASE-STRING-LIST (CDR X)))) :EXEC (REVERSE (STR::UPCASE-STRING-LIST-AUX X NIL)))) (LOCAL (IN-THEORY (ENABLE STR::UPCASE-STRING-LIST-AUX STR::UPCASE-STRING-LIST))) (DEFTHM STR::STRING-LISTP-UPCASE-STRING-LIST (STRING-LISTP (STR::UPCASE-STRING-LIST X))) (DEFTHM STR::UPCASE-STRING-LIST-AUX-IS-UPCASE-STRING-LIST (EQUAL (STR::UPCASE-STRING-LIST-AUX X STR::ACC) (REVAPPEND (STR::UPCASE-STRING-LIST X) STR::ACC))) (VERIFY-GUARDS STR::UPCASE-STRING-LIST))) (RECORD-EXPANSION (MAKE-EVENT (LET* ((XDOC::NAME (QUOTE STR::UPCASE-STRING-LIST)) (XDOC::PARENTS (QUOTE (STR::CASES))) (XDOC::SHORT (QUOTE "Convert every string in a list to upper case.")) (XDOC::EXTENSION (QUOTE NIL)) (XDOC::WRLD (W STATE)) (XDOC::TRIPS (REVERSED-WORLD-SINCE-EVENT XDOC::WRLD (QUOTE (TABLE INTRO-TABLE :MARK (QUOTE STR::UPCASE-STRING-LIST))) NIL)) (XDOC::INFO (REVERSE (NEW-FORMULA-INFO XDOC::TRIPS XDOC::WRLD NIL))) (XDOC::AUTODOC (XDOC::FORMULA-INFO-TO-DEFS (NOT XDOC::EXTENSION) XDOC::INFO)) (XDOC::LONG (CONCATENATE (QUOTE STRING) (QUOTE "") (COERCE (LIST #\Newline #\Newline) (QUOTE STRING)) XDOC::AUTODOC))) (IF XDOC::EXTENSION (CONS (QUOTE XDOC-EXTEND) (CONS XDOC::EXTENSION (CONS XDOC::LONG (QUOTE NIL)))) (CONS (QUOTE DEFXDOC) (CONS XDOC::NAME (CONS (QUOTE :PARENTS) (CONS XDOC::PARENTS (CONS (QUOTE :SHORT) (CONS XDOC::SHORT (CONS (QUOTE :LONG) (CONS XDOC::LONG (QUOTE NIL)))))))))))) (WITH-OUTPUT :OFF (EVENT SUMMARY) (PROGN (TABLE XDOC (QUOTE DOC) (CONS (QUOTE ((:NAME . STR::UPCASE-STRING-LIST) (:BASE-PKG . STR::ACL2-PKG-WITNESS) (:PARENTS STR::CASES) (:SHORT . "Convert every string in a list to upper case.") (:LONG . "

<h3>Definitions and Theorems</h3>@(def |STR|::|UPCASE-STRING-LIST-AUX|)
@(def |STR|::|UPCASE-STRING-LIST|)
@(def |STR|::|STRING-LISTP-UPCASE-STRING-LIST|)
@(def |STR|::|UPCASE-STRING-LIST-AUX-IS-UPCASE-STRING-LIST|)") (:FROM . "[books]/str/case-conversion.lisp"))) (XDOC::GET-XDOC-TABLE WORLD))) (VALUE-TRIPLE (QUOTE (DEFXDOC STR::UPCASE-STRING-LIST)))))) (VALUE-TRIPLE (QUOTE STR::UPCASE-STRING-LIST))))) (11 RECORD-EXPANSION (DEFSECTION STR::DOWNCASE-STRING-LIST :PARENTS (STR::CASES) :SHORT "Convert every string in a list to lower case." (DEFUND STR::DOWNCASE-STRING-LIST-AUX (X STR::ACC) (DECLARE (XARGS :GUARD (AND (STRING-LISTP X) (STRING-LISTP STR::ACC)))) (IF (ATOM X) STR::ACC (STR::DOWNCASE-STRING-LIST-AUX (CDR X) (CONS (STR::DOWNCASE-STRING (CAR X)) STR::ACC)))) (DEFUND STR::DOWNCASE-STRING-LIST (X) (DECLARE (XARGS :GUARD (STRING-LISTP X) :VERIFY-GUARDS NIL)) (MBE :LOGIC (IF (ATOM X) NIL (CONS (STR::DOWNCASE-STRING (CAR X)) (STR::DOWNCASE-STRING-LIST (CDR X)))) :EXEC (REVERSE (STR::DOWNCASE-STRING-LIST-AUX X NIL)))) (LOCAL (IN-THEORY (ENABLE STR::DOWNCASE-STRING-LIST-AUX STR::DOWNCASE-STRING-LIST))) (DEFTHM STR::STRING-LISTP-DOWNCASE-STRING-LIST (STRING-LISTP (STR::DOWNCASE-STRING-LIST X))) (DEFTHM STR::DOWNCASE-STRING-LIST-AUX-IS-DOWNCASE-STRING-LIST (EQUAL (STR::DOWNCASE-STRING-LIST-AUX X STR::ACC) (REVAPPEND (STR::DOWNCASE-STRING-LIST X) STR::ACC))) (VERIFY-GUARDS STR::DOWNCASE-STRING-LIST)) (WITH-OUTPUT :STACK :PUSH :OFF :ALL :ON ERROR (PROGN (TABLE INTRO-TABLE :MARK (QUOTE STR::DOWNCASE-STRING-LIST)) (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (DEFUND STR::DOWNCASE-STRING-LIST-AUX (X STR::ACC) (DECLARE (XARGS :GUARD (AND (STRING-LISTP X) (STRING-LISTP STR::ACC)))) (IF (ATOM X) STR::ACC (STR::DOWNCASE-STRING-LIST-AUX (CDR X) (CONS (STR::DOWNCASE-STRING (CAR X)) STR::ACC)))) (DEFUND STR::DOWNCASE-STRING-LIST (X) (DECLARE (XARGS :GUARD (STRING-LISTP X) :VERIFY-GUARDS NIL)) (MBE :LOGIC (IF (ATOM X) NIL (CONS (STR::DOWNCASE-STRING (CAR X)) (STR::DOWNCASE-STRING-LIST (CDR X)))) :EXEC (REVERSE (STR::DOWNCASE-STRING-LIST-AUX X NIL)))) (LOCAL (IN-THEORY (ENABLE STR::DOWNCASE-STRING-LIST-AUX STR::DOWNCASE-STRING-LIST))) (DEFTHM STR::STRING-LISTP-DOWNCASE-STRING-LIST (STRING-LISTP (STR::DOWNCASE-STRING-LIST X))) (DEFTHM STR::DOWNCASE-STRING-LIST-AUX-IS-DOWNCASE-STRING-LIST (EQUAL (STR::DOWNCASE-STRING-LIST-AUX X STR::ACC) (REVAPPEND (STR::DOWNCASE-STRING-LIST X) STR::ACC))) (VERIFY-GUARDS STR::DOWNCASE-STRING-LIST))) (RECORD-EXPANSION (MAKE-EVENT (LET* ((XDOC::NAME (QUOTE STR::DOWNCASE-STRING-LIST)) (XDOC::PARENTS (QUOTE (STR::CASES))) (XDOC::SHORT (QUOTE "Convert every string in a list to lower case.")) (XDOC::EXTENSION (QUOTE NIL)) (XDOC::WRLD (W STATE)) (XDOC::TRIPS (REVERSED-WORLD-SINCE-EVENT XDOC::WRLD (QUOTE (TABLE INTRO-TABLE :MARK (QUOTE STR::DOWNCASE-STRING-LIST))) NIL)) (XDOC::INFO (REVERSE (NEW-FORMULA-INFO XDOC::TRIPS XDOC::WRLD NIL))) (XDOC::AUTODOC (XDOC::FORMULA-INFO-TO-DEFS (NOT XDOC::EXTENSION) XDOC::INFO)) (XDOC::LONG (CONCATENATE (QUOTE STRING) (QUOTE "") (COERCE (LIST #\Newline #\Newline) (QUOTE STRING)) XDOC::AUTODOC))) (IF XDOC::EXTENSION (CONS (QUOTE XDOC-EXTEND) (CONS XDOC::EXTENSION (CONS XDOC::LONG (QUOTE NIL)))) (CONS (QUOTE DEFXDOC) (CONS XDOC::NAME (CONS (QUOTE :PARENTS) (CONS XDOC::PARENTS (CONS (QUOTE :SHORT) (CONS XDOC::SHORT (CONS (QUOTE :LONG) (CONS XDOC::LONG (QUOTE NIL)))))))))))) (WITH-OUTPUT :OFF (EVENT SUMMARY) (PROGN (TABLE XDOC (QUOTE DOC) (CONS (QUOTE ((:NAME . STR::DOWNCASE-STRING-LIST) (:BASE-PKG . STR::ACL2-PKG-WITNESS) (:PARENTS STR::CASES) (:SHORT . "Convert every string in a list to lower case.") (:LONG . "

<h3>Definitions and Theorems</h3>@(def |STR|::|DOWNCASE-STRING-LIST-AUX|)
@(def |STR|::|DOWNCASE-STRING-LIST|)
@(def |STR|::|STRING-LISTP-DOWNCASE-STRING-LIST|)
@(def |STR|::|DOWNCASE-STRING-LIST-AUX-IS-DOWNCASE-STRING-LIST|)") (:FROM . "[books]/str/case-conversion.lisp"))) (XDOC::GET-XDOC-TABLE WORLD))) (VALUE-TRIPLE (QUOTE (DEFXDOC STR::DOWNCASE-STRING-LIST)))))) (VALUE-TRIPLE (QUOTE STR::DOWNCASE-STRING-LIST))))) (12 RECORD-EXPANSION (DEFSECTION STR::UPCASE-FIRST-CHARLIST :PARENTS (STR::CASES) :SHORT "Convert the first character of a character list to upper case." (DEFUND STR::UPCASE-FIRST-CHARLIST (X) (DECLARE (XARGS :GUARD (CHARACTER-LISTP X))) (MBE :LOGIC (IF (ATOM X) NIL (CONS (STR::UPCASE-CHAR (CAR X)) (MAKE-CHARACTER-LIST (CDR X)))) :EXEC (COND ((ATOM X) NIL) ((STR::DOWN-ALPHA-P (CAR X)) (CONS (STR::UPCASE-CHAR (CAR X)) (CDR X))) (T X)))) (LOCAL (IN-THEORY (ENABLE STR::UPCASE-FIRST-CHARLIST))) (DEFCONG STR::CHARLISTEQV EQUAL (STR::UPCASE-FIRST-CHARLIST X) 1) (DEFCONG STR::ICHARLISTEQV STR::ICHARLISTEQV (STR::UPCASE-FIRST-CHARLIST X) 1) (DEFTHM STR::UPCASE-FIRST-CHARLIST-WHEN-ATOM (IMPLIES (ATOM X) (EQUAL (STR::UPCASE-FIRST-CHARLIST X) NIL))) (DEFTHM STR::CHARACTER-LISTP-OF-UPCASE-FIRST-CHARLIST (IMPLIES (CHARACTER-LISTP X) (CHARACTER-LISTP (STR::UPCASE-FIRST-CHARLIST X)))) (DEFTHM STR::LEN-OF-UPCASE-FIRST-CHARLIST (EQUAL (LEN (STR::UPCASE-FIRST-CHARLIST X)) (LEN X))) (DEFTHM STR::CONSP-OF-UPCASE-FIRST-CHARLIST (EQUAL (CONSP (STR::UPCASE-FIRST-CHARLIST X)) (CONSP X))) (DEFTHM STR::UPCASE-FIRST-CHARLIST-UNDER-IFF (IFF (STR::UPCASE-FIRST-CHARLIST X) (CONSP X)))) (WITH-OUTPUT :STACK :PUSH :OFF :ALL :ON ERROR (PROGN (TABLE INTRO-TABLE :MARK (QUOTE STR::UPCASE-FIRST-CHARLIST)) (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (DEFUND STR::UPCASE-FIRST-CHARLIST (X) (DECLARE (XARGS :GUARD (CHARACTER-LISTP X))) (MBE :LOGIC (IF (ATOM X) NIL (CONS (STR::UPCASE-CHAR (CAR X)) (MAKE-CHARACTER-LIST (CDR X)))) :EXEC (COND ((ATOM X) NIL) ((STR::DOWN-ALPHA-P (CAR X)) (CONS (STR::UPCASE-CHAR (CAR X)) (CDR X))) (T X)))) (LOCAL (IN-THEORY (ENABLE STR::UPCASE-FIRST-CHARLIST))) (DEFCONG STR::CHARLISTEQV EQUAL (STR::UPCASE-FIRST-CHARLIST X) 1) (DEFCONG STR::ICHARLISTEQV STR::ICHARLISTEQV (STR::UPCASE-FIRST-CHARLIST X) 1) (DEFTHM STR::UPCASE-FIRST-CHARLIST-WHEN-ATOM (IMPLIES (ATOM X) (EQUAL (STR::UPCASE-FIRST-CHARLIST X) NIL))) (DEFTHM STR::CHARACTER-LISTP-OF-UPCASE-FIRST-CHARLIST (IMPLIES (CHARACTER-LISTP X) (CHARACTER-LISTP (STR::UPCASE-FIRST-CHARLIST X)))) (DEFTHM STR::LEN-OF-UPCASE-FIRST-CHARLIST (EQUAL (LEN (STR::UPCASE-FIRST-CHARLIST X)) (LEN X))) (DEFTHM STR::CONSP-OF-UPCASE-FIRST-CHARLIST (EQUAL (CONSP (STR::UPCASE-FIRST-CHARLIST X)) (CONSP X))) (DEFTHM STR::UPCASE-FIRST-CHARLIST-UNDER-IFF (IFF (STR::UPCASE-FIRST-CHARLIST X) (CONSP X))))) (RECORD-EXPANSION (MAKE-EVENT (LET* ((XDOC::NAME (QUOTE STR::UPCASE-FIRST-CHARLIST)) (XDOC::PARENTS (QUOTE (STR::CASES))) (XDOC::SHORT (QUOTE "Convert the first character of a character list to upper case.")) (XDOC::EXTENSION (QUOTE NIL)) (XDOC::WRLD (W STATE)) (XDOC::TRIPS (REVERSED-WORLD-SINCE-EVENT XDOC::WRLD (QUOTE (TABLE INTRO-TABLE :MARK (QUOTE STR::UPCASE-FIRST-CHARLIST))) NIL)) (XDOC::INFO (REVERSE (NEW-FORMULA-INFO XDOC::TRIPS XDOC::WRLD NIL))) (XDOC::AUTODOC (XDOC::FORMULA-INFO-TO-DEFS (NOT XDOC::EXTENSION) XDOC::INFO)) (XDOC::LONG (CONCATENATE (QUOTE STRING) (QUOTE "") (COERCE (LIST #\Newline #\Newline) (QUOTE STRING)) XDOC::AUTODOC))) (IF XDOC::EXTENSION (CONS (QUOTE XDOC-EXTEND) (CONS XDOC::EXTENSION (CONS XDOC::LONG (QUOTE NIL)))) (CONS (QUOTE DEFXDOC) (CONS XDOC::NAME (CONS (QUOTE :PARENTS) (CONS XDOC::PARENTS (CONS (QUOTE :SHORT) (CONS XDOC::SHORT (CONS (QUOTE :LONG) (CONS XDOC::LONG (QUOTE NIL)))))))))))) (WITH-OUTPUT :OFF (EVENT SUMMARY) (PROGN (TABLE XDOC (QUOTE DOC) (CONS (QUOTE ((:NAME . STR::UPCASE-FIRST-CHARLIST) (:BASE-PKG . STR::ACL2-PKG-WITNESS) (:PARENTS STR::CASES) (:SHORT . "Convert the first character of a character list to upper case.") (:LONG . "

<h3>Definitions and Theorems</h3>@(def |STR|::|UPCASE-FIRST-CHARLIST|)
@(def |STR|::|CHARLISTEQV-IMPLIES-EQUAL-UPCASE-FIRST-CHARLIST-1|)
@(def |STR|::|ICHARLISTEQV-IMPLIES-ICHARLISTEQV-UPCASE-FIRST-CHARLIST-1|)
@(def |STR|::|UPCASE-FIRST-CHARLIST-WHEN-ATOM|)
@(def |STR|::|CHARACTER-LISTP-OF-UPCASE-FIRST-CHARLIST|)
@(def |STR|::|LEN-OF-UPCASE-FIRST-CHARLIST|)
@(def |STR|::|CONSP-OF-UPCASE-FIRST-CHARLIST|)
@(def |STR|::|UPCASE-FIRST-CHARLIST-UNDER-IFF|)") (:FROM . "[books]/str/case-conversion.lisp"))) (XDOC::GET-XDOC-TABLE WORLD))) (VALUE-TRIPLE (QUOTE (DEFXDOC STR::UPCASE-FIRST-CHARLIST)))))) (VALUE-TRIPLE (QUOTE STR::UPCASE-FIRST-CHARLIST))))) (13 RECORD-EXPANSION (DEFSECTION STR::UPCASE-FIRST :PARENTS (STR::CASES) :SHORT "Convert the first character of a string to upper case." :LONG "<p>@(call upcase-first) returns a copy of the string @('x') except
that the first character is upcased using @(see upcase-char).  If the string is
empty, we return it unchanged.</p>

<p>For sometimes-better performance, we avoid consing and simply return @('x')
unchanged when its first character is not a lower-case letter.</p>" (DEFUND STR::UPCASE-FIRST (X) (DECLARE (TYPE STRING X) (XARGS :VERIFY-GUARDS NIL)) (MBE :LOGIC (IMPLODE (STR::UPCASE-FIRST-CHARLIST (EXPLODE X))) :EXEC (IF (EQL (LENGTH X) 0) X (LET ((C (CHAR X 0))) (IF (STR::DOWN-ALPHA-P C) (STR::CAT (STR::UPCASE-CHAR-STR C) (SUBSEQ X 1 NIL)) X))))) (LOCAL (IN-THEORY (ENABLE STR::UPCASE-FIRST-CHARLIST STR::UPCASE-FIRST SUBSEQ SUBSEQ-LIST))) (VERIFY-GUARDS STR::UPCASE-FIRST) (DEFTHM STR::STRINGP-OF-UPCASE-FIRST (STRINGP (STR::UPCASE-FIRST X)) :RULE-CLASSES :TYPE-PRESCRIPTION) (DEFCONG STR::STREQV EQUAL (STR::UPCASE-FIRST X) 1) (DEFCONG STR::ISTREQV STR::ISTREQV (STR::UPCASE-FIRST X) 1)) (WITH-OUTPUT :STACK :PUSH :OFF :ALL :ON ERROR (PROGN (TABLE INTRO-TABLE :MARK (QUOTE STR::UPCASE-FIRST)) (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (DEFUND STR::UPCASE-FIRST (X) (DECLARE (TYPE STRING X) (XARGS :VERIFY-GUARDS NIL)) (MBE :LOGIC (IMPLODE (STR::UPCASE-FIRST-CHARLIST (EXPLODE X))) :EXEC (IF (EQL (LENGTH X) 0) X (LET ((C (CHAR X 0))) (IF (STR::DOWN-ALPHA-P C) (STR::CAT (STR::UPCASE-CHAR-STR C) (SUBSEQ X 1 NIL)) X))))) (LOCAL (IN-THEORY (ENABLE STR::UPCASE-FIRST-CHARLIST STR::UPCASE-FIRST SUBSEQ SUBSEQ-LIST))) (VERIFY-GUARDS STR::UPCASE-FIRST) (DEFTHM STR::STRINGP-OF-UPCASE-FIRST (STRINGP (STR::UPCASE-FIRST X)) :RULE-CLASSES :TYPE-PRESCRIPTION) (DEFCONG STR::STREQV EQUAL (STR::UPCASE-FIRST X) 1) (DEFCONG STR::ISTREQV STR::ISTREQV (STR::UPCASE-FIRST X) 1))) (RECORD-EXPANSION (MAKE-EVENT (LET* ((XDOC::NAME (QUOTE STR::UPCASE-FIRST)) (XDOC::PARENTS (QUOTE (STR::CASES))) (XDOC::SHORT (QUOTE "Convert the first character of a string to upper case.")) (XDOC::EXTENSION (QUOTE NIL)) (XDOC::WRLD (W STATE)) (XDOC::TRIPS (REVERSED-WORLD-SINCE-EVENT XDOC::WRLD (QUOTE (TABLE INTRO-TABLE :MARK (QUOTE STR::UPCASE-FIRST))) NIL)) (XDOC::INFO (REVERSE (NEW-FORMULA-INFO XDOC::TRIPS XDOC::WRLD NIL))) (XDOC::AUTODOC (XDOC::FORMULA-INFO-TO-DEFS (NOT XDOC::EXTENSION) XDOC::INFO)) (XDOC::LONG (CONCATENATE (QUOTE STRING) (QUOTE "<p>@(call upcase-first) returns a copy of the string @('x') except
that the first character is upcased using @(see upcase-char).  If the string is
empty, we return it unchanged.</p>

<p>For sometimes-better performance, we avoid consing and simply return @('x')
unchanged when its first character is not a lower-case letter.</p>") (COERCE (LIST #\Newline #\Newline) (QUOTE STRING)) XDOC::AUTODOC))) (IF XDOC::EXTENSION (CONS (QUOTE XDOC-EXTEND) (CONS XDOC::EXTENSION (CONS XDOC::LONG (QUOTE NIL)))) (CONS (QUOTE DEFXDOC) (CONS XDOC::NAME (CONS (QUOTE :PARENTS) (CONS XDOC::PARENTS (CONS (QUOTE :SHORT) (CONS XDOC::SHORT (CONS (QUOTE :LONG) (CONS XDOC::LONG (QUOTE NIL)))))))))))) (WITH-OUTPUT :OFF (EVENT SUMMARY) (PROGN (TABLE XDOC (QUOTE DOC) (CONS (QUOTE ((:NAME . STR::UPCASE-FIRST) (:BASE-PKG . STR::ACL2-PKG-WITNESS) (:PARENTS STR::CASES) (:SHORT . "Convert the first character of a string to upper case.") (:LONG . "<p>@(call upcase-first) returns a copy of the string @('x') except
that the first character is upcased using @(see upcase-char).  If the string is
empty, we return it unchanged.</p>

<p>For sometimes-better performance, we avoid consing and simply return @('x')
unchanged when its first character is not a lower-case letter.</p>

<h3>Definitions and Theorems</h3>@(def |STR|::|UPCASE-FIRST|)
@(def |STR|::|STRINGP-OF-UPCASE-FIRST|)
@(def |STR|::|STREQV-IMPLIES-EQUAL-UPCASE-FIRST-1|)
@(def |STR|::|ISTREQV-IMPLIES-ISTREQV-UPCASE-FIRST-1|)") (:FROM . "[books]/str/case-conversion.lisp"))) (XDOC::GET-XDOC-TABLE WORLD))) (VALUE-TRIPLE (QUOTE (DEFXDOC STR::UPCASE-FIRST)))))) (VALUE-TRIPLE (QUOTE STR::UPCASE-FIRST))))) (14 RECORD-EXPANSION (DEFSECTION STR::DOWNCASE-FIRST-CHARLIST :PARENTS (STR::CASES) :SHORT "Convert the first character of a character list to downper case." (DEFUND STR::DOWNCASE-FIRST-CHARLIST (X) (DECLARE (XARGS :GUARD (CHARACTER-LISTP X))) (MBE :LOGIC (IF (ATOM X) NIL (CONS (STR::DOWNCASE-CHAR (CAR X)) (MAKE-CHARACTER-LIST (CDR X)))) :EXEC (COND ((ATOM X) NIL) ((STR::UP-ALPHA-P (CAR X)) (CONS (STR::DOWNCASE-CHAR (CAR X)) (CDR X))) (T X)))) (LOCAL (IN-THEORY (ENABLE STR::DOWNCASE-FIRST-CHARLIST))) (DEFCONG STR::CHARLISTEQV EQUAL (STR::DOWNCASE-FIRST-CHARLIST X) 1) (DEFCONG STR::ICHARLISTEQV STR::ICHARLISTEQV (STR::DOWNCASE-FIRST-CHARLIST X) 1) (DEFTHM STR::DOWNCASE-FIRST-CHARLIST-WHEN-ATOM (IMPLIES (ATOM X) (EQUAL (STR::DOWNCASE-FIRST-CHARLIST X) NIL))) (DEFTHM STR::CHARACTER-LISTP-OF-DOWNCASE-FIRST-CHARLIST (IMPLIES (CHARACTER-LISTP X) (CHARACTER-LISTP (STR::DOWNCASE-FIRST-CHARLIST X)))) (DEFTHM STR::LEN-OF-DOWNCASE-FIRST-CHARLIST (EQUAL (LEN (STR::DOWNCASE-FIRST-CHARLIST X)) (LEN X))) (DEFTHM STR::CONSP-OF-DOWNCASE-FIRST-CHARLIST (EQUAL (CONSP (STR::DOWNCASE-FIRST-CHARLIST X)) (CONSP X))) (DEFTHM STR::DOWNCASE-FIRST-CHARLIST-UNDER-IFF (IFF (STR::DOWNCASE-FIRST-CHARLIST X) (CONSP X)))) (WITH-OUTPUT :STACK :PUSH :OFF :ALL :ON ERROR (PROGN (TABLE INTRO-TABLE :MARK (QUOTE STR::DOWNCASE-FIRST-CHARLIST)) (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (DEFUND STR::DOWNCASE-FIRST-CHARLIST (X) (DECLARE (XARGS :GUARD (CHARACTER-LISTP X))) (MBE :LOGIC (IF (ATOM X) NIL (CONS (STR::DOWNCASE-CHAR (CAR X)) (MAKE-CHARACTER-LIST (CDR X)))) :EXEC (COND ((ATOM X) NIL) ((STR::UP-ALPHA-P (CAR X)) (CONS (STR::DOWNCASE-CHAR (CAR X)) (CDR X))) (T X)))) (LOCAL (IN-THEORY (ENABLE STR::DOWNCASE-FIRST-CHARLIST))) (DEFCONG STR::CHARLISTEQV EQUAL (STR::DOWNCASE-FIRST-CHARLIST X) 1) (DEFCONG STR::ICHARLISTEQV STR::ICHARLISTEQV (STR::DOWNCASE-FIRST-CHARLIST X) 1) (DEFTHM STR::DOWNCASE-FIRST-CHARLIST-WHEN-ATOM (IMPLIES (ATOM X) (EQUAL (STR::DOWNCASE-FIRST-CHARLIST X) NIL))) (DEFTHM STR::CHARACTER-LISTP-OF-DOWNCASE-FIRST-CHARLIST (IMPLIES (CHARACTER-LISTP X) (CHARACTER-LISTP (STR::DOWNCASE-FIRST-CHARLIST X)))) (DEFTHM STR::LEN-OF-DOWNCASE-FIRST-CHARLIST (EQUAL (LEN (STR::DOWNCASE-FIRST-CHARLIST X)) (LEN X))) (DEFTHM STR::CONSP-OF-DOWNCASE-FIRST-CHARLIST (EQUAL (CONSP (STR::DOWNCASE-FIRST-CHARLIST X)) (CONSP X))) (DEFTHM STR::DOWNCASE-FIRST-CHARLIST-UNDER-IFF (IFF (STR::DOWNCASE-FIRST-CHARLIST X) (CONSP X))))) (RECORD-EXPANSION (MAKE-EVENT (LET* ((XDOC::NAME (QUOTE STR::DOWNCASE-FIRST-CHARLIST)) (XDOC::PARENTS (QUOTE (STR::CASES))) (XDOC::SHORT (QUOTE "Convert the first character of a character list to downper case.")) (XDOC::EXTENSION (QUOTE NIL)) (XDOC::WRLD (W STATE)) (XDOC::TRIPS (REVERSED-WORLD-SINCE-EVENT XDOC::WRLD (QUOTE (TABLE INTRO-TABLE :MARK (QUOTE STR::DOWNCASE-FIRST-CHARLIST))) NIL)) (XDOC::INFO (REVERSE (NEW-FORMULA-INFO XDOC::TRIPS XDOC::WRLD NIL))) (XDOC::AUTODOC (XDOC::FORMULA-INFO-TO-DEFS (NOT XDOC::EXTENSION) XDOC::INFO)) (XDOC::LONG (CONCATENATE (QUOTE STRING) (QUOTE "") (COERCE (LIST #\Newline #\Newline) (QUOTE STRING)) XDOC::AUTODOC))) (IF XDOC::EXTENSION (CONS (QUOTE XDOC-EXTEND) (CONS XDOC::EXTENSION (CONS XDOC::LONG (QUOTE NIL)))) (CONS (QUOTE DEFXDOC) (CONS XDOC::NAME (CONS (QUOTE :PARENTS) (CONS XDOC::PARENTS (CONS (QUOTE :SHORT) (CONS XDOC::SHORT (CONS (QUOTE :LONG) (CONS XDOC::LONG (QUOTE NIL)))))))))))) (WITH-OUTPUT :OFF (EVENT SUMMARY) (PROGN (TABLE XDOC (QUOTE DOC) (CONS (QUOTE ((:NAME . STR::DOWNCASE-FIRST-CHARLIST) (:BASE-PKG . STR::ACL2-PKG-WITNESS) (:PARENTS STR::CASES) (:SHORT . "Convert the first character of a character list to downper case.") (:LONG . "

<h3>Definitions and Theorems</h3>@(def |STR|::|DOWNCASE-FIRST-CHARLIST|)
@(def |STR|::|CHARLISTEQV-IMPLIES-EQUAL-DOWNCASE-FIRST-CHARLIST-1|)
@(def |STR|::|ICHARLISTEQV-IMPLIES-ICHARLISTEQV-DOWNCASE-FIRST-CHARLIST-1|)
@(def |STR|::|DOWNCASE-FIRST-CHARLIST-WHEN-ATOM|)
@(def |STR|::|CHARACTER-LISTP-OF-DOWNCASE-FIRST-CHARLIST|)
@(def |STR|::|LEN-OF-DOWNCASE-FIRST-CHARLIST|)
@(def |STR|::|CONSP-OF-DOWNCASE-FIRST-CHARLIST|)
@(def |STR|::|DOWNCASE-FIRST-CHARLIST-UNDER-IFF|)") (:FROM . "[books]/str/case-conversion.lisp"))) (XDOC::GET-XDOC-TABLE WORLD))) (VALUE-TRIPLE (QUOTE (DEFXDOC STR::DOWNCASE-FIRST-CHARLIST)))))) (VALUE-TRIPLE (QUOTE STR::DOWNCASE-FIRST-CHARLIST))))) (15 RECORD-EXPANSION (DEFSECTION STR::DOWNCASE-FIRST :PARENTS (STR::CASES) :SHORT "Convert the first character of a string to downper case." :LONG "<p>@(call downcase-first) returns a copy of the string @('x') except
that the first character is downcased using @(see downcase-char).  If the
string is empty, we return it unchanged.</p>

<p>For sometimes-better performance, we avoid consing and simply return @('x')
unchanged when its first character is not an upper-case letter.</p>" (DEFUND STR::DOWNCASE-FIRST (X) (DECLARE (TYPE STRING X) (XARGS :VERIFY-GUARDS NIL)) (MBE :LOGIC (IMPLODE (STR::DOWNCASE-FIRST-CHARLIST (EXPLODE X))) :EXEC (IF (EQL (LENGTH X) 0) X (LET ((C (CHAR X 0))) (IF (STR::UP-ALPHA-P C) (STR::CAT (STR::DOWNCASE-CHAR-STR C) (SUBSEQ X 1 NIL)) X))))) (LOCAL (IN-THEORY (ENABLE STR::DOWNCASE-FIRST-CHARLIST STR::DOWNCASE-FIRST SUBSEQ SUBSEQ-LIST))) (VERIFY-GUARDS STR::DOWNCASE-FIRST) (DEFTHM STR::STRINGP-OF-DOWNCASE-FIRST (STRINGP (STR::DOWNCASE-FIRST X)) :RULE-CLASSES :TYPE-PRESCRIPTION) (DEFCONG STR::STREQV EQUAL (STR::DOWNCASE-FIRST X) 1) (DEFCONG STR::ISTREQV STR::ISTREQV (STR::DOWNCASE-FIRST X) 1)) (WITH-OUTPUT :STACK :PUSH :OFF :ALL :ON ERROR (PROGN (TABLE INTRO-TABLE :MARK (QUOTE STR::DOWNCASE-FIRST)) (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (DEFUND STR::DOWNCASE-FIRST (X) (DECLARE (TYPE STRING X) (XARGS :VERIFY-GUARDS NIL)) (MBE :LOGIC (IMPLODE (STR::DOWNCASE-FIRST-CHARLIST (EXPLODE X))) :EXEC (IF (EQL (LENGTH X) 0) X (LET ((C (CHAR X 0))) (IF (STR::UP-ALPHA-P C) (STR::CAT (STR::DOWNCASE-CHAR-STR C) (SUBSEQ X 1 NIL)) X))))) (LOCAL (IN-THEORY (ENABLE STR::DOWNCASE-FIRST-CHARLIST STR::DOWNCASE-FIRST SUBSEQ SUBSEQ-LIST))) (VERIFY-GUARDS STR::DOWNCASE-FIRST) (DEFTHM STR::STRINGP-OF-DOWNCASE-FIRST (STRINGP (STR::DOWNCASE-FIRST X)) :RULE-CLASSES :TYPE-PRESCRIPTION) (DEFCONG STR::STREQV EQUAL (STR::DOWNCASE-FIRST X) 1) (DEFCONG STR::ISTREQV STR::ISTREQV (STR::DOWNCASE-FIRST X) 1))) (RECORD-EXPANSION (MAKE-EVENT (LET* ((XDOC::NAME (QUOTE STR::DOWNCASE-FIRST)) (XDOC::PARENTS (QUOTE (STR::CASES))) (XDOC::SHORT (QUOTE "Convert the first character of a string to downper case.")) (XDOC::EXTENSION (QUOTE NIL)) (XDOC::WRLD (W STATE)) (XDOC::TRIPS (REVERSED-WORLD-SINCE-EVENT XDOC::WRLD (QUOTE (TABLE INTRO-TABLE :MARK (QUOTE STR::DOWNCASE-FIRST))) NIL)) (XDOC::INFO (REVERSE (NEW-FORMULA-INFO XDOC::TRIPS XDOC::WRLD NIL))) (XDOC::AUTODOC (XDOC::FORMULA-INFO-TO-DEFS (NOT XDOC::EXTENSION) XDOC::INFO)) (XDOC::LONG (CONCATENATE (QUOTE STRING) (QUOTE "<p>@(call downcase-first) returns a copy of the string @('x') except
that the first character is downcased using @(see downcase-char).  If the
string is empty, we return it unchanged.</p>

<p>For sometimes-better performance, we avoid consing and simply return @('x')
unchanged when its first character is not an upper-case letter.</p>") (COERCE (LIST #\Newline #\Newline) (QUOTE STRING)) XDOC::AUTODOC))) (IF XDOC::EXTENSION (CONS (QUOTE XDOC-EXTEND) (CONS XDOC::EXTENSION (CONS XDOC::LONG (QUOTE NIL)))) (CONS (QUOTE DEFXDOC) (CONS XDOC::NAME (CONS (QUOTE :PARENTS) (CONS XDOC::PARENTS (CONS (QUOTE :SHORT) (CONS XDOC::SHORT (CONS (QUOTE :LONG) (CONS XDOC::LONG (QUOTE NIL)))))))))))) (WITH-OUTPUT :OFF (EVENT SUMMARY) (PROGN (TABLE XDOC (QUOTE DOC) (CONS (QUOTE ((:NAME . STR::DOWNCASE-FIRST) (:BASE-PKG . STR::ACL2-PKG-WITNESS) (:PARENTS STR::CASES) (:SHORT . "Convert the first character of a string to downper case.") (:LONG . "<p>@(call downcase-first) returns a copy of the string @('x') except
that the first character is downcased using @(see downcase-char).  If the
string is empty, we return it unchanged.</p>

<p>For sometimes-better performance, we avoid consing and simply return @('x')
unchanged when its first character is not an upper-case letter.</p>

<h3>Definitions and Theorems</h3>@(def |STR|::|DOWNCASE-FIRST|)
@(def |STR|::|STRINGP-OF-DOWNCASE-FIRST|)
@(def |STR|::|STREQV-IMPLIES-EQUAL-DOWNCASE-FIRST-1|)
@(def |STR|::|ISTREQV-IMPLIES-ISTREQV-DOWNCASE-FIRST-1|)") (:FROM . "[books]/str/case-conversion.lisp"))) (XDOC::GET-XDOC-TABLE WORLD))) (VALUE-TRIPLE (QUOTE (DEFXDOC STR::DOWNCASE-FIRST)))))) (VALUE-TRIPLE (QUOTE STR::DOWNCASE-FIRST))))))
(("/usr/share/acl2-6.3/books/cutil/portcullis.lisp" "cutil/portcullis" "portcullis" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1188104018) ("/usr/share/acl2-6.3/books/std/osets/portcullis.lisp" "std/osets/portcullis" "portcullis" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1689687557) ("/usr/share/acl2-6.3/books/xdoc/portcullis.lisp" "xdoc/portcullis" "portcullis" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1473208573) ("/usr/share/acl2-6.3/books/str/portcullis.lisp" "str/portcullis" "portcullis" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 2077071243))
(("/usr/share/acl2-6.3/books/str/case-conversion.lisp" "case-conversion" "case-conversion" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 646818128) (LOCAL ("/usr/share/acl2-6.3/books/str/subseq.lisp" "subseq" "subseq" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1507065012)) ("/usr/share/acl2-6.3/books/str/cat.lisp" "cat" "cat" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1576295912) ("/usr/share/acl2-6.3/books/str/ieqv.lisp" "ieqv" "ieqv" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 620245362) ("/usr/share/acl2-6.3/books/std/lists/list-defuns.lisp" "std/lists/list-defuns" "list-defuns" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 321177760) (LOCAL ("/usr/share/acl2-6.3/books/std/lists/sublistp.lisp" "sublistp" "sublistp" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1635583873)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic/top-with-meta.lisp" "arithmetic/top-with-meta" "top-with-meta" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 349005499)) (LOCAL ("/usr/share/acl2-6.3/books/meta/meta.lisp" "meta/meta" "meta" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1434715577)) (LOCAL ("/usr/share/acl2-6.3/books/meta/meta-times-equal.lisp" "meta-times-equal" "meta-times-equal" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 2078846479)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic/equalities.lisp" "arithmetic/equalities" "equalities" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 597034595)) (LOCAL ("/usr/share/acl2-6.3/books/meta/meta-plus-lessp.lisp" "meta-plus-lessp" "meta-plus-lessp" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 932651372)) (LOCAL ("/usr/share/acl2-6.3/books/meta/meta-plus-equal.lisp" "meta-plus-equal" "meta-plus-equal" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1948431900)) (LOCAL ("/usr/share/acl2-6.3/books/meta/term-lemmas.lisp" "term-lemmas" "term-lemmas" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 304413851)) (LOCAL ("/usr/share/acl2-6.3/books/meta/term-defuns.lisp" "term-defuns" "term-defuns" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1038247295)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic/top.lisp" "top" "top" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 956305966)) (LOCAL ("/usr/share/acl2-6.3/books/std/lists/same-lengthp.lisp" "same-lengthp" "same-lengthp" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 2063823673)) (LOCAL ("/usr/share/acl2-6.3/books/std/lists/sets.lisp" "sets" "sets" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 878261262)) (LOCAL ("/usr/share/acl2-6.3/books/std/lists/mfc-utils.lisp" "mfc-utils" "mfc-utils" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1043482843)) (LOCAL ("/usr/share/acl2-6.3/books/std/lists/rcons.lisp" "rcons" "rcons" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 105042482)) (LOCAL ("/usr/share/acl2-6.3/books/std/lists/repeat.lisp" "repeat" "repeat" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 293545519)) (LOCAL ("/usr/share/acl2-6.3/books/std/lists/prefixp.lisp" "prefixp" "prefixp" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 689235789)) (LOCAL ("/usr/share/acl2-6.3/books/std/lists/final-cdr.lisp" "final-cdr" "final-cdr" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 96013958)) (LOCAL ("/usr/share/acl2-6.3/books/std/lists/duplicity.lisp" "duplicity" "duplicity" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 914433854)) (LOCAL ("/usr/share/acl2-6.3/books/std/lists/flatten.lisp" "flatten" "flatten" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1125138266)) ("/usr/share/acl2-6.3/books/std/lists/equiv.lisp" "equiv" "equiv" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1948483556) ("/usr/share/acl2-6.3/books/tools/rulesets.lisp" "tools/rulesets" "rulesets" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 639683473) ("/usr/share/acl2-6.3/books/str/char-case.lisp" "char-case" "char-case" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 2059343298) ("/usr/share/acl2-6.3/books/tools/bstar.lisp" "tools/bstar" "bstar" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1482974359) ("/usr/share/acl2-6.3/books/tools/pack.lisp" "pack" "pack" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1797170439) ("/usr/share/acl2-6.3/books/str/eqv.lisp" "eqv" "eqv" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1920438599) (LOCAL ("/usr/share/acl2-6.3/books/str/arithmetic.lisp" "arithmetic" "arithmetic" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 216355320)) (LOCAL ("/usr/share/acl2-6.3/books/std/lists/repeat.lisp" "std/lists/repeat" "repeat" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 293545519)) (LOCAL ("/usr/share/acl2-6.3/books/std/lists/nthcdr.lisp" "nthcdr" "nthcdr" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1415704060)) ("/usr/share/acl2-6.3/books/std/lists/rev.lisp" "rev" "rev" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 327117871) (LOCAL ("/usr/share/acl2-6.3/books/std/lists/nthcdr.lisp" "std/lists/nthcdr" "nthcdr" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1415704060)) (LOCAL ("/usr/share/acl2-6.3/books/std/lists/len.lisp" "std/lists/len" "len" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 963137114)) (LOCAL ("/usr/share/acl2-6.3/books/std/lists/take.lisp" "std/lists/take" "take" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1496833916)) ("/usr/share/acl2-6.3/books/std/lists/rev.lisp" "std/lists/rev" "rev" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 327117871) (LOCAL ("/usr/share/acl2-6.3/books/std/lists/append.lisp" "append" "append" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 567759210)) (LOCAL ("/usr/share/acl2-6.3/books/std/lists/revappend.lisp" "revappend" "revappend" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1368863429)) ("/usr/share/acl2-6.3/books/std/lists/equiv.lisp" "std/lists/equiv" "equiv" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1948483556) (LOCAL ("/usr/share/acl2-6.3/books/std/lists/take.lisp" "take" "take" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1496833916)) ("/usr/share/acl2-6.3/books/str/coerce.lisp" "coerce" "coerce" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1053051260) ("/usr/share/acl2-6.3/books/str/make-character-list.lisp" "make-character-list" "make-character-list" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1622566814) (LOCAL ("/usr/share/acl2-6.3/books/std/lists/append.lisp" "std/lists/append" "append" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 567759210)) ("/usr/share/acl2-6.3/books/std/lists/list-fix.lisp" "list-fix" "list-fix" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1844974260) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic/top.lisp" "arithmetic/top" "top" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 956305966)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic/rationals.lisp" "rationals" "rationals" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1403689963)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic/mod-gcd.lisp" "mod-gcd" "mod-gcd" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1629957550)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic/natp-posp.lisp" "natp-posp" "natp-posp" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 2140150970)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic/inequalities.lisp" "inequalities" "inequalities" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1221989523)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic/nat-listp.lisp" "nat-listp" "nat-listp" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1767896370)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic/rational-listp.lisp" "rational-listp" "rational-listp" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1775556314)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic/equalities.lisp" "equalities" "equalities" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 597034595)) (LOCAL ("/usr/share/acl2-6.3/books/cowles/acl2-crg.lisp" "cowles/acl2-crg" "acl2-crg" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 761519866)) (LOCAL ("/usr/share/acl2-6.3/books/cowles/acl2-agp.lisp" "acl2-agp" "acl2-agp" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 2007324914)) (LOCAL ("/usr/share/acl2-6.3/books/cowles/acl2-asg.lisp" "acl2-asg" "acl2-asg" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1939433116)) ("/usr/share/acl2-6.3/books/str/char-fix.lisp" "char-fix" "char-fix" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 70055851) ("/usr/share/acl2-6.3/books/misc/definline.lisp" "misc/definline" "definline" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1571016648) ("/usr/share/acl2-6.3/books/xdoc/top.lisp" "xdoc/top" "top" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1214825095) ("/usr/share/acl2-6.3/books/xdoc/book-thms.lisp" "book-thms" "book-thms" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1105796063) ("/usr/share/acl2-6.3/books/xdoc/base.lisp" "base" "base" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 454271148) ("/usr/share/acl2-6.3/books/xdoc/portcullis.lisp" "portcullis" "portcullis" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1473208573) ("/usr/share/acl2-6.3/books/cutil/portcullis.lisp" "cutil/portcullis" "portcullis" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1188104018) ("/usr/share/acl2-6.3/books/std/osets/portcullis.lisp" "std/osets/portcullis" "portcullis" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1689687557) ("/usr/share/acl2-6.3/books/xdoc/portcullis.lisp" "xdoc/portcullis" "portcullis" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1473208573) ("/usr/share/acl2-6.3/books/str/portcullis.lisp" "str/portcullis" "portcullis" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 2077071243))
1859562669
acl2-books-certs 6.3-5 / usr / share / acl2-6.3 / books / str / case-conversion.cert
