/usr/share/acl2-6.3/books/str/strnatless.cert

(IN-PACKAGE "ACL2")
"ACL2 Version 6.3"
:BEGIN-PORTCULLIS-CMDS
(INCLUDE-BOOK "cutil/portcullis" :DIR :SYSTEM)
:END-PORTCULLIS-CMDS
:EXPANSION-ALIST
((4 RECORD-EXPANSION (DEFSECTION STR::PARSE-NAT-FROM-CHARLIST :PARENTS (STR::NUMBERS) :SHORT "Parse a natural number from the beginning of a character list." :LONG "<p>@(call parse-nat-from-charlist) tries to read a natural number from
the beginning of the character list @('x').</p>

<ul>

<li>@('val') is an accumulator for the value of the digits we have read so far,
and typically should be set to 0 to begin with.</li>

<li>@('len') is an accumulator for the number of digits we have read, and
should typically be set to 0 to begin with.</li>

</ul>

<p>We return @('(mv val len rest)'), where @('x') after reading as many digits
as possible.</p>

<p>See also @(call digit-list-value), which is simpler for interpreting strings
where all of the characters are digits.</p>" (DEFUND STR::PARSE-NAT-FROM-CHARLIST (X STR::VAL LEN) (DECLARE (TYPE INTEGER STR::VAL) (TYPE INTEGER LEN) (XARGS :GUARD (AND (CHARACTER-LISTP X) (NATP STR::VAL) (NATP LEN)) :VERIFY-GUARDS NIL)) (MBE :LOGIC (COND ((ATOM X) (MV (NFIX STR::VAL) (NFIX LEN) NIL)) ((STR::DIGITP (CAR X)) (LET ((STR::DIGIT-VAL (STR::DIGIT-VAL (CAR X)))) (STR::PARSE-NAT-FROM-CHARLIST (CDR X) (+ STR::DIGIT-VAL (* 10 (NFIX STR::VAL))) (+ 1 (NFIX LEN))))) (T (MV (NFIX STR::VAL) (NFIX LEN) X))) :EXEC (COND ((ATOM X) (MV STR::VAL LEN NIL)) (T (LET ((STR::CODE (THE (UNSIGNED-BYTE 8) (CHAR-CODE (THE CHARACTER (CAR X)))))) (DECLARE (TYPE (UNSIGNED-BYTE 8) STR::CODE)) (IF (AND (<= (THE (UNSIGNED-BYTE 8) 48) (THE (UNSIGNED-BYTE 8) STR::CODE)) (<= (THE (UNSIGNED-BYTE 8) STR::CODE) (THE (UNSIGNED-BYTE 8) 57))) (LET ((STR::DIGIT-VAL (THE (UNSIGNED-BYTE 8) (- (THE (UNSIGNED-BYTE 8) STR::CODE) (THE (UNSIGNED-BYTE 8) 48))))) (STR::PARSE-NAT-FROM-CHARLIST (CDR X) (THE INTEGER (+ (THE (UNSIGNED-BYTE 8) STR::DIGIT-VAL) (THE INTEGER (* 10 (THE INTEGER STR::VAL))))) (THE INTEGER (+ 1 (THE INTEGER LEN))))) (MV STR::VAL LEN X))))))) (LOCAL (IN-THEORY (ENABLE STR::PARSE-NAT-FROM-CHARLIST))) (VERIFY-GUARDS STR::PARSE-NAT-FROM-CHARLIST :HINTS (("Goal" :IN-THEORY (ENABLE STR::DIGITP STR::DIGIT-VAL STR::CHAR-FIX)))) (ENCAPSULATE NIL (LOCAL (DEFUND STR::LEADING-DIGITS-VALUE (X STR::VAL) (DECLARE (XARGS :VERIFY-GUARDS NIL)) (IF (CONSP X) (IF (STR::DIGITP (CAR X)) (STR::LEADING-DIGITS-VALUE (CDR X) (+ (STR::DIGIT-VAL (CAR X)) (* 10 (NFIX STR::VAL)))) (NFIX STR::VAL)) (NFIX STR::VAL)))) (LOCAL (DEFTHM STR::LEMMA-1 (EQUAL (MV-NTH 0 (STR::PARSE-NAT-FROM-CHARLIST X STR::VAL LEN)) (STR::LEADING-DIGITS-VALUE X STR::VAL)) :HINTS (("Goal" :IN-THEORY (ENABLE STR::LEADING-DIGITS-VALUE))))) (LOCAL (DEFTHM STR::LEMMA-2 (EQUAL (STR::LEADING-DIGITS-VALUE X STR::VAL) (STR::DIGIT-LIST-VALUE1 (STR::TAKE-LEADING-DIGITS X) STR::VAL)) :HINTS (("Goal" :IN-THEORY (E/D (STR::LEADING-DIGITS-VALUE STR::DIGIT-LIST-VALUE1 STR::TAKE-LEADING-DIGITS) (STR::DIGIT-LIST-VALUE1-REMOVAL)))))) (DEFTHM STR::VAL-OF-PARSE-NAT-FROM-CHARLIST (EQUAL (MV-NTH 0 (STR::PARSE-NAT-FROM-CHARLIST X STR::VAL LEN)) (+ (STR::DIGIT-LIST-VALUE (STR::TAKE-LEADING-DIGITS X)) (* (NFIX STR::VAL) (EXPT 10 (LEN (STR::TAKE-LEADING-DIGITS X)))))))) (ENCAPSULATE NIL (LOCAL (DEFUND STR::COUNT-LEADING-DIGITS1 (X LEN) (DECLARE (XARGS :VERIFY-GUARDS NIL)) (IF (CONSP X) (IF (STR::DIGITP (CAR X)) (STR::COUNT-LEADING-DIGITS1 (CDR X) (+ 1 (NFIX LEN))) (NFIX LEN)) (NFIX LEN)))) (LOCAL (DEFTHM STR::LEMMA-1 (EQUAL (MV-NTH 1 (STR::PARSE-NAT-FROM-CHARLIST X STR::VAL LEN)) (STR::COUNT-LEADING-DIGITS1 X LEN)) :HINTS (("Goal" :IN-THEORY (ENABLE STR::COUNT-LEADING-DIGITS1))))) (LOCAL (DEFTHM STR::LEMMA-2 (EQUAL (STR::COUNT-LEADING-DIGITS1 X LEN) (+ (NFIX LEN) (LEN (STR::TAKE-LEADING-DIGITS X)))) :HINTS (("Goal" :IN-THEORY (ENABLE STR::COUNT-LEADING-DIGITS1 STR::TAKE-LEADING-DIGITS))))) (DEFTHM STR::LEN-OF-PARSE-NAT-FROM-CHARLIST (EQUAL (MV-NTH 1 (STR::PARSE-NAT-FROM-CHARLIST X STR::VAL LEN)) (+ (NFIX LEN) (LEN (STR::TAKE-LEADING-DIGITS X)))))) (DEFTHM STR::REST-OF-PARSE-NAT-FROM-CHARLIST (EQUAL (MV-NTH 2 (STR::PARSE-NAT-FROM-CHARLIST X STR::VAL LEN)) (STR::SKIP-LEADING-DIGITS X)) :HINTS (("Goal" :IN-THEORY (ENABLE STR::SKIP-LEADING-DIGITS))))) (WITH-OUTPUT :STACK :PUSH :OFF :ALL :ON ERROR (PROGN (TABLE INTRO-TABLE :MARK (QUOTE STR::PARSE-NAT-FROM-CHARLIST)) (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (DEFUND STR::PARSE-NAT-FROM-CHARLIST (X STR::VAL LEN) (DECLARE (TYPE INTEGER STR::VAL) (TYPE INTEGER LEN) (XARGS :GUARD (AND (CHARACTER-LISTP X) (NATP STR::VAL) (NATP LEN)) :VERIFY-GUARDS NIL)) (MBE :LOGIC (COND ((ATOM X) (MV (NFIX STR::VAL) (NFIX LEN) NIL)) ((STR::DIGITP (CAR X)) (LET ((STR::DIGIT-VAL (STR::DIGIT-VAL (CAR X)))) (STR::PARSE-NAT-FROM-CHARLIST (CDR X) (+ STR::DIGIT-VAL (* 10 (NFIX STR::VAL))) (+ 1 (NFIX LEN))))) (T (MV (NFIX STR::VAL) (NFIX LEN) X))) :EXEC (COND ((ATOM X) (MV STR::VAL LEN NIL)) (T (LET ((STR::CODE (THE (UNSIGNED-BYTE 8) (CHAR-CODE (THE CHARACTER (CAR X)))))) (DECLARE (TYPE (UNSIGNED-BYTE 8) STR::CODE)) (IF (AND (<= (THE (UNSIGNED-BYTE 8) 48) (THE (UNSIGNED-BYTE 8) STR::CODE)) (<= (THE (UNSIGNED-BYTE 8) STR::CODE) (THE (UNSIGNED-BYTE 8) 57))) (LET ((STR::DIGIT-VAL (THE (UNSIGNED-BYTE 8) (- (THE (UNSIGNED-BYTE 8) STR::CODE) (THE (UNSIGNED-BYTE 8) 48))))) (STR::PARSE-NAT-FROM-CHARLIST (CDR X) (THE INTEGER (+ (THE (UNSIGNED-BYTE 8) STR::DIGIT-VAL) (THE INTEGER (* 10 (THE INTEGER STR::VAL))))) (THE INTEGER (+ 1 (THE INTEGER LEN))))) (MV STR::VAL LEN X))))))) (LOCAL (IN-THEORY (ENABLE STR::PARSE-NAT-FROM-CHARLIST))) (VERIFY-GUARDS STR::PARSE-NAT-FROM-CHARLIST :HINTS (("Goal" :IN-THEORY (ENABLE STR::DIGITP STR::DIGIT-VAL STR::CHAR-FIX)))) (ENCAPSULATE NIL (LOCAL (DEFUND STR::LEADING-DIGITS-VALUE (X STR::VAL) (DECLARE (XARGS :VERIFY-GUARDS NIL)) (IF (CONSP X) (IF (STR::DIGITP (CAR X)) (STR::LEADING-DIGITS-VALUE (CDR X) (+ (STR::DIGIT-VAL (CAR X)) (* 10 (NFIX STR::VAL)))) (NFIX STR::VAL)) (NFIX STR::VAL)))) (LOCAL (DEFTHM STR::LEMMA-1 (EQUAL (MV-NTH 0 (STR::PARSE-NAT-FROM-CHARLIST X STR::VAL LEN)) (STR::LEADING-DIGITS-VALUE X STR::VAL)) :HINTS (("Goal" :IN-THEORY (ENABLE STR::LEADING-DIGITS-VALUE))))) (LOCAL (DEFTHM STR::LEMMA-2 (EQUAL (STR::LEADING-DIGITS-VALUE X STR::VAL) (STR::DIGIT-LIST-VALUE1 (STR::TAKE-LEADING-DIGITS X) STR::VAL)) :HINTS (("Goal" :IN-THEORY (E/D (STR::LEADING-DIGITS-VALUE STR::DIGIT-LIST-VALUE1 STR::TAKE-LEADING-DIGITS) (STR::DIGIT-LIST-VALUE1-REMOVAL)))))) (DEFTHM STR::VAL-OF-PARSE-NAT-FROM-CHARLIST (EQUAL (MV-NTH 0 (STR::PARSE-NAT-FROM-CHARLIST X STR::VAL LEN)) (+ (STR::DIGIT-LIST-VALUE (STR::TAKE-LEADING-DIGITS X)) (* (NFIX STR::VAL) (EXPT 10 (LEN (STR::TAKE-LEADING-DIGITS X)))))))) (ENCAPSULATE NIL (LOCAL (DEFUND STR::COUNT-LEADING-DIGITS1 (X LEN) (DECLARE (XARGS :VERIFY-GUARDS NIL)) (IF (CONSP X) (IF (STR::DIGITP (CAR X)) (STR::COUNT-LEADING-DIGITS1 (CDR X) (+ 1 (NFIX LEN))) (NFIX LEN)) (NFIX LEN)))) (LOCAL (DEFTHM STR::LEMMA-1 (EQUAL (MV-NTH 1 (STR::PARSE-NAT-FROM-CHARLIST X STR::VAL LEN)) (STR::COUNT-LEADING-DIGITS1 X LEN)) :HINTS (("Goal" :IN-THEORY (ENABLE STR::COUNT-LEADING-DIGITS1))))) (LOCAL (DEFTHM STR::LEMMA-2 (EQUAL (STR::COUNT-LEADING-DIGITS1 X LEN) (+ (NFIX LEN) (LEN (STR::TAKE-LEADING-DIGITS X)))) :HINTS (("Goal" :IN-THEORY (ENABLE STR::COUNT-LEADING-DIGITS1 STR::TAKE-LEADING-DIGITS))))) (DEFTHM STR::LEN-OF-PARSE-NAT-FROM-CHARLIST (EQUAL (MV-NTH 1 (STR::PARSE-NAT-FROM-CHARLIST X STR::VAL LEN)) (+ (NFIX LEN) (LEN (STR::TAKE-LEADING-DIGITS X)))))) (DEFTHM STR::REST-OF-PARSE-NAT-FROM-CHARLIST (EQUAL (MV-NTH 2 (STR::PARSE-NAT-FROM-CHARLIST X STR::VAL LEN)) (STR::SKIP-LEADING-DIGITS X)) :HINTS (("Goal" :IN-THEORY (ENABLE STR::SKIP-LEADING-DIGITS)))))) (RECORD-EXPANSION (MAKE-EVENT (LET* ((XDOC::NAME (QUOTE STR::PARSE-NAT-FROM-CHARLIST)) (XDOC::PARENTS (QUOTE (STR::NUMBERS))) (XDOC::SHORT (QUOTE "Parse a natural number from the beginning of a character list.")) (XDOC::EXTENSION (QUOTE NIL)) (XDOC::WRLD (W STATE)) (XDOC::TRIPS (REVERSED-WORLD-SINCE-EVENT XDOC::WRLD (QUOTE (TABLE INTRO-TABLE :MARK (QUOTE STR::PARSE-NAT-FROM-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 parse-nat-from-charlist) tries to read a natural number from
the beginning of the character list @('x').</p>

<ul>

<li>@('val') is an accumulator for the value of the digits we have read so far,
and typically should be set to 0 to begin with.</li>

<li>@('len') is an accumulator for the number of digits we have read, and
should typically be set to 0 to begin with.</li>

</ul>

<p>We return @('(mv val len rest)'), where @('x') after reading as many digits
as possible.</p>

<p>See also @(call digit-list-value), which is simpler for interpreting strings
where all of the characters are digits.</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::PARSE-NAT-FROM-CHARLIST) (:BASE-PKG . STR::ACL2-PKG-WITNESS) (:PARENTS STR::NUMBERS) (:SHORT . "Parse a natural number from the beginning of a character list.") (:LONG . "<p>@(call parse-nat-from-charlist) tries to read a natural number from
the beginning of the character list @('x').</p>

<ul>

<li>@('val') is an accumulator for the value of the digits we have read so far,
and typically should be set to 0 to begin with.</li>

<li>@('len') is an accumulator for the number of digits we have read, and
should typically be set to 0 to begin with.</li>

</ul>

<p>We return @('(mv val len rest)'), where @('x') after reading as many digits
as possible.</p>

<p>See also @(call digit-list-value), which is simpler for interpreting strings
where all of the characters are digits.</p>

<h3>Definitions and Theorems</h3>@(def |STR|::|PARSE-NAT-FROM-CHARLIST|)
@(def |STR|::|VAL-OF-PARSE-NAT-FROM-CHARLIST|)
@(def |STR|::|LEN-OF-PARSE-NAT-FROM-CHARLIST|)
@(def |STR|::|REST-OF-PARSE-NAT-FROM-CHARLIST|)") (:FROM . "[books]/str/strnatless.lisp"))) (XDOC::GET-XDOC-TABLE WORLD))) (VALUE-TRIPLE (QUOTE (DEFXDOC STR::PARSE-NAT-FROM-CHARLIST)))))) (VALUE-TRIPLE (QUOTE STR::PARSE-NAT-FROM-CHARLIST))))) (5 RECORD-EXPANSION (DEFSECTION STR::PARSE-NAT-FROM-STRING :PARENTS (STR::NUMBERS) :SHORT "Parse a natural number from a string, at some offset." :LONG "<p>@(call parse-nat-from-string) is somewhat elaborate:</p>

<ul>

<li>@('x') is a string that we want to parse a value from</li>

<li>@('val') is an accumulator for the value we have parsed, and it should
generally be 0 to begin with.</li>

<li>@('len') is an accumulator for the number of characters we have read so
far, and should generally be 0 to begin with.</li>

<li>@('n') is an offset into @('x') where we should begin parsing.  It must be
a valid index into the string, i.e., @('0 <= n < (length x)').</li>

<li>@('xl') must be exactly equal to @('(length x)'), and only serves as a
cache to avoid recomputing the length.</li>

</ul>

<p>We return @('(mv val len)'), the final values of the accumulators, which are
respectively the natural number we have just parsed and the number of digits
that we parsed.</p>

<p>Both @('val') and @('len') are guaranteed to be natural numbers; failure is
indicated by a return @('len') of zero.</p>

<p>Because of leading zeroes, the @('len') may be much larger than you would
expect based on @('val') alone.  The @('len') argument is generally useful if
you want to continue parsing through the string, i.e., the @('n') you started
with plus the @('len') you got out will be the next position in the string
after the number.</p>

<p>See also @(see parse-nat-from-charlist) for a simpler function that reads a
number from the start of a character list.  This function also serves as part
of our logical definition.</p>" (LOCAL (IN-THEORY (DISABLE NTH-WHEN-BIGGER NEGATIVE-WHEN-NATP DEFAULT-+-2 DEFAULT-+-1 DEFAULT-<-2 COMMUTATIVITY-OF-+ DEFAULT-<-1 |x < y  =>  0 < y-x|))) (DEFUND STR::PARSE-NAT-FROM-STRING (X STR::VAL LEN N STR::XL) (DECLARE (TYPE STRING X) (TYPE (INTEGER 0 *) STR::VAL LEN N STR::XL) (XARGS :GUARD (AND (STRINGP X) (NATP STR::VAL) (NATP LEN) (NATP N) (EQUAL STR::XL (LENGTH X)) (<= N STR::XL)) :MEASURE (NFIX (- (NFIX STR::XL) (NFIX N))) :VERIFY-GUARDS NIL)) (MBE :LOGIC (COND ((ZP (- (NFIX STR::XL) (NFIX N))) (MV (NFIX STR::VAL) (NFIX LEN))) ((STR::DIGITP (CHAR X N)) (LET ((STR::DIGIT-VAL (STR::DIGIT-VAL (CHAR X N)))) (STR::PARSE-NAT-FROM-STRING X (+ STR::DIGIT-VAL (* 10 (NFIX STR::VAL))) (+ 1 (NFIX LEN)) (+ 1 (NFIX N)) (NFIX STR::XL)))) (T (MV (NFIX STR::VAL) (NFIX LEN)))) :EXEC (COND ((INT= N STR::XL) (MV STR::VAL LEN)) (T (LET ((STR::CODE (THE (UNSIGNED-BYTE 8) (CHAR-CODE (THE CHARACTER (CHAR (THE STRING X) (THE (INTEGER 0 *) N))))))) (DECLARE (TYPE (UNSIGNED-BYTE 8) STR::CODE)) (IF (AND (<= (THE (UNSIGNED-BYTE 8) 48) (THE (UNSIGNED-BYTE 8) STR::CODE)) (<= (THE (UNSIGNED-BYTE 8) STR::CODE) (THE (UNSIGNED-BYTE 8) 57))) (LET ((STR::DIGIT-VAL (THE (UNSIGNED-BYTE 8) (- (THE (UNSIGNED-BYTE 8) STR::CODE) (THE (UNSIGNED-BYTE 8) 48))))) (STR::PARSE-NAT-FROM-STRING (THE STRING X) (THE (INTEGER 0 *) (+ (THE (UNSIGNED-BYTE 8) STR::DIGIT-VAL) (THE (INTEGER 0 *) (* 10 (THE (INTEGER 0 *) STR::VAL))))) (THE (INTEGER 0 *) (+ 1 (THE (INTEGER 0 *) LEN))) (THE (INTEGER 0 *) (+ 1 (THE (INTEGER 0 *) N))) (THE (INTEGER 0 *) STR::XL))) (MV STR::VAL LEN))))))) (LOCAL (IN-THEORY (ENABLE STR::PARSE-NAT-FROM-STRING))) (VERIFY-GUARDS STR::PARSE-NAT-FROM-STRING :HINTS (("Goal" :IN-THEORY (ENABLE STR::DIGITP STR::DIGIT-VAL)))) (DEFTHM STR::NATP-OF-VAL-OF-PARSE-NAT-FROM-STRING (AND (INTEGERP (MV-NTH 0 (STR::PARSE-NAT-FROM-STRING X STR::VAL LEN N STR::XL))) (<= 0 (MV-NTH 0 (STR::PARSE-NAT-FROM-STRING X STR::VAL LEN N STR::XL)))) :RULE-CLASSES :TYPE-PRESCRIPTION :HINTS (("Goal" :IN-THEORY (DISABLE NTH NFIX)))) (DEFTHM STR::NATP-OF-LEN-OF-PARSE-NAT-FROM-STRING (AND (INTEGERP (MV-NTH 1 (STR::PARSE-NAT-FROM-STRING X STR::VAL LEN N STR::XL))) (<= 0 (MV-NTH 1 (STR::PARSE-NAT-FROM-STRING X STR::VAL LEN N STR::XL)))) :RULE-CLASSES :TYPE-PRESCRIPTION :HINTS (("Goal" :IN-THEORY (DISABLE NTH NFIX)))) (DEFTHM STR::PROGRESS-OF-PARSE-NAT-FROM-STRING (IMPLIES (AND (EQUAL STR::XL (LENGTH X)) (OR (< 0 (NFIX LEN)) (STR::DIGITP (CHAR X (NFIX N))))) (< 0 (MV-NTH 1 (STR::PARSE-NAT-FROM-STRING X STR::VAL LEN N STR::XL)))) :RULE-CLASSES ((:REWRITE) (:LINEAR)) :HINTS (("Goal" :INDUCT (STR::PARSE-NAT-FROM-STRING X STR::VAL LEN N STR::XL)))) (DEFTHM STR::VAL-OF-PARSE-NAT-FROM-STRING (IMPLIES (AND (NATP STR::VAL) (NATP LEN) (NATP N) (EQUAL STR::XL (LEN (EXPLODE X))) (<= N STR::XL)) (EQUAL (MV-NTH 0 (STR::PARSE-NAT-FROM-STRING X STR::VAL LEN N STR::XL)) (MV-NTH 0 (STR::PARSE-NAT-FROM-CHARLIST (NTHCDR N (EXPLODE X)) STR::VAL LEN)))) :HINTS (("Goal" :INDUCT (STR::PARSE-NAT-FROM-STRING X STR::VAL LEN N STR::XL) :IN-THEORY (E/D (STR::PARSE-NAT-FROM-CHARLIST) (STR::VAL-OF-PARSE-NAT-FROM-CHARLIST)) :DO-NOT (QUOTE (GENERALIZE FERTILIZE))))) (DEFTHM STR::LEN-OF-PARSE-NAT-FROM-STRING (IMPLIES (AND (NATP STR::VAL) (NATP LEN) (NATP N) (EQUAL STR::XL (LEN (EXPLODE X))) (<= N STR::XL)) (EQUAL (MV-NTH 1 (STR::PARSE-NAT-FROM-STRING X STR::VAL LEN N STR::XL)) (MV-NTH 1 (STR::PARSE-NAT-FROM-CHARLIST (NTHCDR N (EXPLODE X)) STR::VAL LEN)))) :HINTS (("Goal" :INDUCT (STR::PARSE-NAT-FROM-STRING X STR::VAL LEN N STR::XL) :IN-THEORY (E/D (STR::PARSE-NAT-FROM-CHARLIST) (STR::LEN-OF-PARSE-NAT-FROM-CHARLIST)) :DO-NOT (QUOTE (GENERALIZE FERTILIZE)))))) (WITH-OUTPUT :STACK :PUSH :OFF :ALL :ON ERROR (PROGN (TABLE INTRO-TABLE :MARK (QUOTE STR::PARSE-NAT-FROM-STRING)) (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (LOCAL (IN-THEORY (DISABLE NTH-WHEN-BIGGER NEGATIVE-WHEN-NATP DEFAULT-+-2 DEFAULT-+-1 DEFAULT-<-2 COMMUTATIVITY-OF-+ DEFAULT-<-1 |x < y  =>  0 < y-x|))) (DEFUND STR::PARSE-NAT-FROM-STRING (X STR::VAL LEN N STR::XL) (DECLARE (TYPE STRING X) (TYPE (INTEGER 0 *) STR::VAL LEN N STR::XL) (XARGS :GUARD (AND (STRINGP X) (NATP STR::VAL) (NATP LEN) (NATP N) (EQUAL STR::XL (LENGTH X)) (<= N STR::XL)) :MEASURE (NFIX (- (NFIX STR::XL) (NFIX N))) :VERIFY-GUARDS NIL)) (MBE :LOGIC (COND ((ZP (- (NFIX STR::XL) (NFIX N))) (MV (NFIX STR::VAL) (NFIX LEN))) ((STR::DIGITP (CHAR X N)) (LET ((STR::DIGIT-VAL (STR::DIGIT-VAL (CHAR X N)))) (STR::PARSE-NAT-FROM-STRING X (+ STR::DIGIT-VAL (* 10 (NFIX STR::VAL))) (+ 1 (NFIX LEN)) (+ 1 (NFIX N)) (NFIX STR::XL)))) (T (MV (NFIX STR::VAL) (NFIX LEN)))) :EXEC (COND ((INT= N STR::XL) (MV STR::VAL LEN)) (T (LET ((STR::CODE (THE (UNSIGNED-BYTE 8) (CHAR-CODE (THE CHARACTER (CHAR (THE STRING X) (THE (INTEGER 0 *) N))))))) (DECLARE (TYPE (UNSIGNED-BYTE 8) STR::CODE)) (IF (AND (<= (THE (UNSIGNED-BYTE 8) 48) (THE (UNSIGNED-BYTE 8) STR::CODE)) (<= (THE (UNSIGNED-BYTE 8) STR::CODE) (THE (UNSIGNED-BYTE 8) 57))) (LET ((STR::DIGIT-VAL (THE (UNSIGNED-BYTE 8) (- (THE (UNSIGNED-BYTE 8) STR::CODE) (THE (UNSIGNED-BYTE 8) 48))))) (STR::PARSE-NAT-FROM-STRING (THE STRING X) (THE (INTEGER 0 *) (+ (THE (UNSIGNED-BYTE 8) STR::DIGIT-VAL) (THE (INTEGER 0 *) (* 10 (THE (INTEGER 0 *) STR::VAL))))) (THE (INTEGER 0 *) (+ 1 (THE (INTEGER 0 *) LEN))) (THE (INTEGER 0 *) (+ 1 (THE (INTEGER 0 *) N))) (THE (INTEGER 0 *) STR::XL))) (MV STR::VAL LEN))))))) (LOCAL (IN-THEORY (ENABLE STR::PARSE-NAT-FROM-STRING))) (VERIFY-GUARDS STR::PARSE-NAT-FROM-STRING :HINTS (("Goal" :IN-THEORY (ENABLE STR::DIGITP STR::DIGIT-VAL)))) (DEFTHM STR::NATP-OF-VAL-OF-PARSE-NAT-FROM-STRING (AND (INTEGERP (MV-NTH 0 (STR::PARSE-NAT-FROM-STRING X STR::VAL LEN N STR::XL))) (<= 0 (MV-NTH 0 (STR::PARSE-NAT-FROM-STRING X STR::VAL LEN N STR::XL)))) :RULE-CLASSES :TYPE-PRESCRIPTION :HINTS (("Goal" :IN-THEORY (DISABLE NTH NFIX)))) (DEFTHM STR::NATP-OF-LEN-OF-PARSE-NAT-FROM-STRING (AND (INTEGERP (MV-NTH 1 (STR::PARSE-NAT-FROM-STRING X STR::VAL LEN N STR::XL))) (<= 0 (MV-NTH 1 (STR::PARSE-NAT-FROM-STRING X STR::VAL LEN N STR::XL)))) :RULE-CLASSES :TYPE-PRESCRIPTION :HINTS (("Goal" :IN-THEORY (DISABLE NTH NFIX)))) (DEFTHM STR::PROGRESS-OF-PARSE-NAT-FROM-STRING (IMPLIES (AND (EQUAL STR::XL (LENGTH X)) (OR (< 0 (NFIX LEN)) (STR::DIGITP (CHAR X (NFIX N))))) (< 0 (MV-NTH 1 (STR::PARSE-NAT-FROM-STRING X STR::VAL LEN N STR::XL)))) :RULE-CLASSES ((:REWRITE) (:LINEAR)) :HINTS (("Goal" :INDUCT (STR::PARSE-NAT-FROM-STRING X STR::VAL LEN N STR::XL)))) (DEFTHM STR::VAL-OF-PARSE-NAT-FROM-STRING (IMPLIES (AND (NATP STR::VAL) (NATP LEN) (NATP N) (EQUAL STR::XL (LEN (EXPLODE X))) (<= N STR::XL)) (EQUAL (MV-NTH 0 (STR::PARSE-NAT-FROM-STRING X STR::VAL LEN N STR::XL)) (MV-NTH 0 (STR::PARSE-NAT-FROM-CHARLIST (NTHCDR N (EXPLODE X)) STR::VAL LEN)))) :HINTS (("Goal" :INDUCT (STR::PARSE-NAT-FROM-STRING X STR::VAL LEN N STR::XL) :IN-THEORY (E/D (STR::PARSE-NAT-FROM-CHARLIST) (STR::VAL-OF-PARSE-NAT-FROM-CHARLIST)) :DO-NOT (QUOTE (GENERALIZE FERTILIZE))))) (DEFTHM STR::LEN-OF-PARSE-NAT-FROM-STRING (IMPLIES (AND (NATP STR::VAL) (NATP LEN) (NATP N) (EQUAL STR::XL (LEN (EXPLODE X))) (<= N STR::XL)) (EQUAL (MV-NTH 1 (STR::PARSE-NAT-FROM-STRING X STR::VAL LEN N STR::XL)) (MV-NTH 1 (STR::PARSE-NAT-FROM-CHARLIST (NTHCDR N (EXPLODE X)) STR::VAL LEN)))) :HINTS (("Goal" :INDUCT (STR::PARSE-NAT-FROM-STRING X STR::VAL LEN N STR::XL) :IN-THEORY (E/D (STR::PARSE-NAT-FROM-CHARLIST) (STR::LEN-OF-PARSE-NAT-FROM-CHARLIST)) :DO-NOT (QUOTE (GENERALIZE FERTILIZE))))))) (RECORD-EXPANSION (MAKE-EVENT (LET* ((XDOC::NAME (QUOTE STR::PARSE-NAT-FROM-STRING)) (XDOC::PARENTS (QUOTE (STR::NUMBERS))) (XDOC::SHORT (QUOTE "Parse a natural number from a string, at some offset.")) (XDOC::EXTENSION (QUOTE NIL)) (XDOC::WRLD (W STATE)) (XDOC::TRIPS (REVERSED-WORLD-SINCE-EVENT XDOC::WRLD (QUOTE (TABLE INTRO-TABLE :MARK (QUOTE STR::PARSE-NAT-FROM-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 parse-nat-from-string) is somewhat elaborate:</p>

<ul>

<li>@('x') is a string that we want to parse a value from</li>

<li>@('val') is an accumulator for the value we have parsed, and it should
generally be 0 to begin with.</li>

<li>@('len') is an accumulator for the number of characters we have read so
far, and should generally be 0 to begin with.</li>

<li>@('n') is an offset into @('x') where we should begin parsing.  It must be
a valid index into the string, i.e., @('0 <= n < (length x)').</li>

<li>@('xl') must be exactly equal to @('(length x)'), and only serves as a
cache to avoid recomputing the length.</li>

</ul>

<p>We return @('(mv val len)'), the final values of the accumulators, which are
respectively the natural number we have just parsed and the number of digits
that we parsed.</p>

<p>Both @('val') and @('len') are guaranteed to be natural numbers; failure is
indicated by a return @('len') of zero.</p>

<p>Because of leading zeroes, the @('len') may be much larger than you would
expect based on @('val') alone.  The @('len') argument is generally useful if
you want to continue parsing through the string, i.e., the @('n') you started
with plus the @('len') you got out will be the next position in the string
after the number.</p>

<p>See also @(see parse-nat-from-charlist) for a simpler function that reads a
number from the start of a character list.  This function also serves as part
of our 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::PARSE-NAT-FROM-STRING) (:BASE-PKG . STR::ACL2-PKG-WITNESS) (:PARENTS STR::NUMBERS) (:SHORT . "Parse a natural number from a string, at some offset.") (:LONG . "<p>@(call parse-nat-from-string) is somewhat elaborate:</p>

<ul>

<li>@('x') is a string that we want to parse a value from</li>

<li>@('val') is an accumulator for the value we have parsed, and it should
generally be 0 to begin with.</li>

<li>@('len') is an accumulator for the number of characters we have read so
far, and should generally be 0 to begin with.</li>

<li>@('n') is an offset into @('x') where we should begin parsing.  It must be
a valid index into the string, i.e., @('0 <= n < (length x)').</li>

<li>@('xl') must be exactly equal to @('(length x)'), and only serves as a
cache to avoid recomputing the length.</li>

</ul>

<p>We return @('(mv val len)'), the final values of the accumulators, which are
respectively the natural number we have just parsed and the number of digits
that we parsed.</p>

<p>Both @('val') and @('len') are guaranteed to be natural numbers; failure is
indicated by a return @('len') of zero.</p>

<p>Because of leading zeroes, the @('len') may be much larger than you would
expect based on @('val') alone.  The @('len') argument is generally useful if
you want to continue parsing through the string, i.e., the @('n') you started
with plus the @('len') you got out will be the next position in the string
after the number.</p>

<p>See also @(see parse-nat-from-charlist) for a simpler function that reads a
number from the start of a character list.  This function also serves as part
of our logical definition.</p>

<h3>Definitions and Theorems</h3>@(def |STR|::|PARSE-NAT-FROM-STRING|)
@(def |STR|::|NATP-OF-VAL-OF-PARSE-NAT-FROM-STRING|)
@(def |STR|::|NATP-OF-LEN-OF-PARSE-NAT-FROM-STRING|)
@(def |STR|::|PROGRESS-OF-PARSE-NAT-FROM-STRING|)
@(def |STR|::|VAL-OF-PARSE-NAT-FROM-STRING|)
@(def |STR|::|LEN-OF-PARSE-NAT-FROM-STRING|)") (:FROM . "[books]/str/strnatless.lisp"))) (XDOC::GET-XDOC-TABLE WORLD))) (VALUE-TRIPLE (QUOTE (DEFXDOC STR::PARSE-NAT-FROM-STRING)))))) (VALUE-TRIPLE (QUOTE STR::PARSE-NAT-FROM-STRING))))) (6 RECORD-EXPANSION (DEFSECTION STR::CHARLISTNAT< :PARENTS (STR::ORDERING) :SHORT "Mixed alphanumeric character-list less-than test." :LONG "<p>@(call charlistnat<) determines if the character list @('x') is
\"smaller\" than the character list @('y'), using an ordering that is nice for
humans.</p>

<p>This is almost an ordinary case-sensitive lexicographic ordering.  But,
unlike a simple lexicographic order, we identify sequences of natural number
digits and group them together so that they can be sorted numerically.</p>

<p>Even though this function operates on character lists, let's just talk about
strings instead since they are easier to write down.  If you give most string
sorts a list of inputs like \"x0\" through \"x11\", they will end up in a
peculiar order:</p>

@({\"x0\", \"x1\", \"x10\", \"x11\", \"x2\", \"x3\", ... \"x9\"})

<p>But in @('charlistnat<'), we see the adjacent digits as bundles and sort
them as numbers.  This leads to a nicer ordering:</p>

@({\"x0\", \"x1\", \"x2\", ..., \"x9\", \"x10\", \"x11\"})

<p>This is almost entirely straightforward.  One twist is how to accommodate
leading zeroes.  Our approach is: instead of grouping adjacent digits and
treating them as a natural number, treat them as a pair with a value and a
length.  We then sort these pairs first by value, and then by length.  Hence, a
string such as \"x0\" is considered to be less than \"x00\", etc.</p>

<p>See also @(see strnat<) and @(see icharlist<).</p>" (LOCAL (IN-THEORY (DISABLE NTH-WHEN-BIGGER NEGATIVE-WHEN-NATP DEFAULT-+-2 DEFAULT-+-1 DEFAULT-<-2 COMMUTATIVITY-OF-+ DEFAULT-<-1 |x < y  =>  0 < y-x| STR::CHAR<-TRICHOTOMY-STRONG STR::CHAR<-ANTISYMMETRIC STR::CHAR<-TRICHOTOMY-WEAK STR::CHAR<-TRANSITIVE EXPT DEFAULT-CAR DEFAULT-CDR))) (DEFUND STR::CHARLISTNAT< (X Y) (DECLARE (XARGS :GUARD (AND (CHARACTER-LISTP X) (CHARACTER-LISTP Y)) :MEASURE (LEN X))) (COND ((ATOM Y) NIL) ((ATOM X) T) ((AND (STR::DIGITP (CAR X)) (STR::DIGITP (CAR Y))) (B* (((MV STR::V1 STR::L1 STR::REST-X) (STR::PARSE-NAT-FROM-CHARLIST X 0 0)) ((MV STR::V2 STR::L2 STR::REST-Y) (STR::PARSE-NAT-FROM-CHARLIST Y 0 0))) (COND ((OR (< STR::V1 STR::V2) (AND (INT= STR::V1 STR::V2) (< STR::L1 STR::L2))) T) ((OR (< STR::V2 STR::V1) (AND (INT= STR::V1 STR::V2) (< STR::L2 STR::L1))) NIL) (T (STR::CHARLISTNAT< STR::REST-X STR::REST-Y))))) ((CHAR< (CAR X) (CAR Y)) T) ((CHAR< (CAR Y) (CAR X)) NIL) (T (STR::CHARLISTNAT< (CDR X) (CDR Y))))) (LOCAL (IN-THEORY (ENABLE STR::CHARLISTNAT<))) (DEFCONG STR::CHARLISTEQV EQUAL (STR::CHARLISTNAT< X Y) 1) (DEFCONG STR::CHARLISTEQV EQUAL (STR::CHARLISTNAT< X Y) 2) (DEFTHM STR::CHARLISTNAT<-IRREFLEXIVE (NOT (STR::CHARLISTNAT< X X))) (DEFTHM STR::CHARLISTNAT<-ANTISYMMETRIC (IMPLIES (STR::CHARLISTNAT< X Y) (NOT (STR::CHARLISTNAT< Y X))) :HINTS (("goal" :IN-THEORY (ENABLE STR::CHAR<-ANTISYMMETRIC)))) (ENCAPSULATE NIL (LOCAL (DEFTHM STR::CHAR<-NONSENSE-2 (IMPLIES (AND (CHAR< A Y) (NOT (STR::DIGITP A)) (STR::DIGITP Y) (STR::DIGITP Z)) (CHAR< A Z)) :RULE-CLASSES ((:REWRITE :BACKCHAIN-LIMIT-LST 0)) :HINTS (("Goal" :IN-THEORY (ENABLE CHAR< STR::DIGITP))))) (LOCAL (DEFTHM STR::CHAR<-NONSENSE-3 (IMPLIES (AND (CHAR< Y A) (NOT (STR::DIGITP A)) (STR::DIGITP X) (STR::DIGITP Y)) (CHAR< X A)) :RULE-CLASSES ((:REWRITE :BACKCHAIN-LIMIT-LST 0)) :HINTS (("Goal" :IN-THEORY (ENABLE CHAR< STR::DIGITP))))) (LOCAL (DEFTHM STR::CHAR<-NONSENSE-4 (IMPLIES (AND (CHAR< X Y) (NOT (STR::DIGITP Y)) (STR::DIGITP X) (STR::DIGITP Z)) (NOT (CHAR< Y Z))) :RULE-CLASSES ((:REWRITE :BACKCHAIN-LIMIT-LST 0)) :HINTS (("Goal" :IN-THEORY (ENABLE STR::DIGITP CHAR<))))) (DEFTHM STR::CHARLISTNAT<-TRANSITIVE (IMPLIES (AND (STR::CHARLISTNAT< X Y) (STR::CHARLISTNAT< Y Z)) (STR::CHARLISTNAT< X Z)) :HINTS (("Goal" :IN-THEORY (E/D ((:INDUCTION STR::CHARLISTNAT<) STR::CHAR<-TRICHOTOMY-STRONG STR::CHAR<-TRANSITIVE) (EXPT STR::CHARLISTNAT<-ANTISYMMETRIC STR::TAKE-LEADING-DIGITS-WHEN-DIGIT-LISTP DEFAULT-+-2 DEFAULT-+-1 STR::BOUND-OF-LEN-OF-TAKE-LEADING-DIGITS STR::LEN-OF-PARSE-NAT-FROM-CHARLIST)) :INDUCT T :EXPAND ((:FREE (Y) (STR::CHARLISTNAT< X Y)) (:FREE (Z) (STR::CHARLISTNAT< Y Z))))))) (ENCAPSULATE NIL (LOCAL (ENCAPSULATE NIL (LOCAL (DEFUN STR::EXPR (A X B N) (+ A (* X (EXPT B N))))) (LOCAL (INCLUDE-BOOK "arithmetic-3/floor-mod/floor-mod" :DIR :SYSTEM)) (LOCAL (DEFTHM STR::MOD-OF-EXPR (IMPLIES (AND (NATP STR::A1) (NATP STR::X1) (NATP N) (NATP B) (< STR::A1 (EXPT B N)) (<= STR::X1 B)) (EQUAL (MOD (STR::EXPR STR::A1 STR::X1 B N) (EXPT B N)) STR::A1)))) (LOCAL (DEFTHM STR::MAIN-LEMMA (IMPLIES (AND (NATP STR::A1) (NATP STR::A2) (NATP STR::X1) (NATP STR::X2) (NATP N) (NATP B) (< STR::A1 (EXPT B N)) (< STR::A2 (EXPT B N)) (<= STR::X1 B) (<= STR::X2 B) (NOT (EQUAL STR::A1 STR::A2))) (NOT (EQUAL (STR::EXPR STR::A1 STR::X1 B N) (STR::EXPR STR::A2 STR::X2 B N)))) :HINTS (("Goal" :IN-THEORY (DISABLE STR::EXPR STR::MOD-OF-EXPR) :USE ((:INSTANCE STR::MOD-OF-EXPR) (:INSTANCE STR::MOD-OF-EXPR (STR::A1 STR::A2) (STR::X1 STR::X2))))))) (DEFTHMD STR::ARITH-LEMMA-1 (IMPLIES (AND (NATP STR::A1) (NATP STR::A2) (NATP STR::X1) (NATP STR::X2) (NATP N) (NATP B) (< STR::A1 (EXPT B N)) (< STR::A2 (EXPT B N)) (<= STR::X1 B) (<= STR::X2 B) (NOT (EQUAL STR::A1 STR::A2))) (NOT (EQUAL (+ STR::A1 (* STR::X1 (EXPT B N))) (+ STR::A2 (* STR::X2 (EXPT B N)))))) :HINTS (("Goal" :IN-THEORY (ENABLE STR::EXPR) :USE ((:INSTANCE STR::MAIN-LEMMA))))))) (LOCAL (DEFTHM STR::LEMMA-1 (IMPLIES (AND (NOT (EQUAL (STR::DIGIT-LIST-VALUE STR::X2) (STR::DIGIT-LIST-VALUE STR::Y2))) (NOT (EQUAL STR::X2 STR::Y2)) (CHARACTERP STR::X1) (CHARACTERP STR::Y1) (CHARACTER-LISTP STR::X2) (CHARACTER-LISTP STR::Y2) (STR::DIGITP STR::X1) (STR::DIGITP STR::Y1) (STR::DIGIT-LISTP STR::X2) (STR::DIGIT-LISTP STR::Y2) (EQUAL (LEN STR::X2) (LEN STR::Y2))) (NOT (EQUAL (+ (STR::DIGIT-LIST-VALUE STR::X2) (* (STR::DIGIT-VAL STR::X1) (EXPT 10 (LEN STR::X2)))) (+ (STR::DIGIT-LIST-VALUE STR::Y2) (* (STR::DIGIT-VAL STR::Y1) (EXPT 10 (LEN STR::X2))))))) :HINTS (("Goal" :USE ((:INSTANCE STR::ARITH-LEMMA-1 (STR::A1 (STR::DIGIT-LIST-VALUE STR::X2)) (STR::A2 (STR::DIGIT-LIST-VALUE STR::Y2)) (STR::X1 (STR::DIGIT-VAL STR::X1)) (STR::X2 (STR::DIGIT-VAL STR::Y1)) (B 10) (N (LEN STR::X2)))))))) (LOCAL (DEFUN STR::MY-INDUCTION (X Y) (IF (AND (CONSP X) (CONSP Y)) (STR::MY-INDUCTION (CDR X) (CDR Y)) NIL))) (LOCAL (DEFTHM STR::LEMMA-2 (IMPLIES (AND (EQUAL (LEN X) (LEN Y)) (CHARACTER-LISTP X) (CHARACTER-LISTP Y) (STR::DIGIT-LISTP X) (STR::DIGIT-LISTP Y)) (EQUAL (EQUAL (STR::DIGIT-LIST-VALUE X) (STR::DIGIT-LIST-VALUE Y)) (EQUAL X Y))) :HINTS (("Goal" :INDUCT (STR::MY-INDUCTION X Y) :IN-THEORY (ENABLE STR::DIGIT-LISTP STR::DIGIT-LIST-VALUE COMMUTATIVITY-OF-+))))) (LOCAL (DEFTHM STR::LEMMA-3 (IMPLIES (AND (EQUAL (LEN (STR::TAKE-LEADING-DIGITS Y)) (LEN (STR::TAKE-LEADING-DIGITS X))) (EQUAL (STR::DIGIT-LIST-VALUE (STR::TAKE-LEADING-DIGITS Y)) (STR::DIGIT-LIST-VALUE (STR::TAKE-LEADING-DIGITS X))) (STR::CHARLISTEQV (STR::SKIP-LEADING-DIGITS X) (STR::SKIP-LEADING-DIGITS Y))) (EQUAL (STR::CHARLISTEQV X Y) T)) :HINTS (("Goal" :IN-THEORY (ENABLE STR::TAKE-LEADING-DIGITS STR::SKIP-LEADING-DIGITS STR::CHARLISTEQV STR::DIGIT-LIST-VALUE))))) (DEFTHM STR::CHARLISTNAT<-TRICHOTOMY-WEAK (IMPLIES (AND (NOT (STR::CHARLISTNAT< X Y)) (NOT (STR::CHARLISTNAT< Y X))) (EQUAL (STR::CHARLISTEQV X Y) T)) :HINTS (("Goal" :IN-THEORY (E/D (STR::CHAR<-TRICHOTOMY-STRONG) (STR::BOUND-OF-LEN-OF-TAKE-LEADING-DIGITS STR::TAKE-LEADING-DIGITS-WHEN-DIGIT-LISTP RIGHT-CANCELLATION-FOR-+ STR::CHARLISTNAT<-ANTISYMMETRIC STR::CHARLISTNAT<-IRREFLEXIVE))))) (DEFTHM STR::CHARLISTNAT<-TRICHOTOMY-STRONG (EQUAL (STR::CHARLISTNAT< X Y) (AND (NOT (STR::CHARLISTEQV X Y)) (NOT (STR::CHARLISTNAT< Y X)))) :RULE-CLASSES ((:REWRITE :LOOP-STOPPER ((X Y))))))) (WITH-OUTPUT :STACK :PUSH :OFF :ALL :ON ERROR (PROGN (TABLE INTRO-TABLE :MARK (QUOTE STR::CHARLISTNAT<)) (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (LOCAL (IN-THEORY (DISABLE NTH-WHEN-BIGGER NEGATIVE-WHEN-NATP DEFAULT-+-2 DEFAULT-+-1 DEFAULT-<-2 COMMUTATIVITY-OF-+ DEFAULT-<-1 |x < y  =>  0 < y-x| STR::CHAR<-TRICHOTOMY-STRONG STR::CHAR<-ANTISYMMETRIC STR::CHAR<-TRICHOTOMY-WEAK STR::CHAR<-TRANSITIVE EXPT DEFAULT-CAR DEFAULT-CDR))) (DEFUND STR::CHARLISTNAT< (X Y) (DECLARE (XARGS :GUARD (AND (CHARACTER-LISTP X) (CHARACTER-LISTP Y)) :MEASURE (LEN X))) (COND ((ATOM Y) NIL) ((ATOM X) T) ((AND (STR::DIGITP (CAR X)) (STR::DIGITP (CAR Y))) (B* (((MV STR::V1 STR::L1 STR::REST-X) (STR::PARSE-NAT-FROM-CHARLIST X 0 0)) ((MV STR::V2 STR::L2 STR::REST-Y) (STR::PARSE-NAT-FROM-CHARLIST Y 0 0))) (COND ((OR (< STR::V1 STR::V2) (AND (INT= STR::V1 STR::V2) (< STR::L1 STR::L2))) T) ((OR (< STR::V2 STR::V1) (AND (INT= STR::V1 STR::V2) (< STR::L2 STR::L1))) NIL) (T (STR::CHARLISTNAT< STR::REST-X STR::REST-Y))))) ((CHAR< (CAR X) (CAR Y)) T) ((CHAR< (CAR Y) (CAR X)) NIL) (T (STR::CHARLISTNAT< (CDR X) (CDR Y))))) (LOCAL (IN-THEORY (ENABLE STR::CHARLISTNAT<))) (DEFCONG STR::CHARLISTEQV EQUAL (STR::CHARLISTNAT< X Y) 1) (DEFCONG STR::CHARLISTEQV EQUAL (STR::CHARLISTNAT< X Y) 2) (DEFTHM STR::CHARLISTNAT<-IRREFLEXIVE (NOT (STR::CHARLISTNAT< X X))) (DEFTHM STR::CHARLISTNAT<-ANTISYMMETRIC (IMPLIES (STR::CHARLISTNAT< X Y) (NOT (STR::CHARLISTNAT< Y X))) :HINTS (("goal" :IN-THEORY (ENABLE STR::CHAR<-ANTISYMMETRIC)))) (ENCAPSULATE NIL (LOCAL (DEFTHM STR::CHAR<-NONSENSE-2 (IMPLIES (AND (CHAR< A Y) (NOT (STR::DIGITP A)) (STR::DIGITP Y) (STR::DIGITP Z)) (CHAR< A Z)) :RULE-CLASSES ((:REWRITE :BACKCHAIN-LIMIT-LST 0)) :HINTS (("Goal" :IN-THEORY (ENABLE CHAR< STR::DIGITP))))) (LOCAL (DEFTHM STR::CHAR<-NONSENSE-3 (IMPLIES (AND (CHAR< Y A) (NOT (STR::DIGITP A)) (STR::DIGITP X) (STR::DIGITP Y)) (CHAR< X A)) :RULE-CLASSES ((:REWRITE :BACKCHAIN-LIMIT-LST 0)) :HINTS (("Goal" :IN-THEORY (ENABLE CHAR< STR::DIGITP))))) (LOCAL (DEFTHM STR::CHAR<-NONSENSE-4 (IMPLIES (AND (CHAR< X Y) (NOT (STR::DIGITP Y)) (STR::DIGITP X) (STR::DIGITP Z)) (NOT (CHAR< Y Z))) :RULE-CLASSES ((:REWRITE :BACKCHAIN-LIMIT-LST 0)) :HINTS (("Goal" :IN-THEORY (ENABLE STR::DIGITP CHAR<))))) (DEFTHM STR::CHARLISTNAT<-TRANSITIVE (IMPLIES (AND (STR::CHARLISTNAT< X Y) (STR::CHARLISTNAT< Y Z)) (STR::CHARLISTNAT< X Z)) :HINTS (("Goal" :IN-THEORY (E/D ((:INDUCTION STR::CHARLISTNAT<) STR::CHAR<-TRICHOTOMY-STRONG STR::CHAR<-TRANSITIVE) (EXPT STR::CHARLISTNAT<-ANTISYMMETRIC STR::TAKE-LEADING-DIGITS-WHEN-DIGIT-LISTP DEFAULT-+-2 DEFAULT-+-1 STR::BOUND-OF-LEN-OF-TAKE-LEADING-DIGITS STR::LEN-OF-PARSE-NAT-FROM-CHARLIST)) :INDUCT T :EXPAND ((:FREE (Y) (STR::CHARLISTNAT< X Y)) (:FREE (Z) (STR::CHARLISTNAT< Y Z))))))) (ENCAPSULATE NIL (LOCAL (ENCAPSULATE NIL (LOCAL (DEFUN STR::EXPR (A X B N) (+ A (* X (EXPT B N))))) (LOCAL (INCLUDE-BOOK "arithmetic-3/floor-mod/floor-mod" :DIR :SYSTEM)) (LOCAL (DEFTHM STR::MOD-OF-EXPR (IMPLIES (AND (NATP STR::A1) (NATP STR::X1) (NATP N) (NATP B) (< STR::A1 (EXPT B N)) (<= STR::X1 B)) (EQUAL (MOD (STR::EXPR STR::A1 STR::X1 B N) (EXPT B N)) STR::A1)))) (LOCAL (DEFTHM STR::MAIN-LEMMA (IMPLIES (AND (NATP STR::A1) (NATP STR::A2) (NATP STR::X1) (NATP STR::X2) (NATP N) (NATP B) (< STR::A1 (EXPT B N)) (< STR::A2 (EXPT B N)) (<= STR::X1 B) (<= STR::X2 B) (NOT (EQUAL STR::A1 STR::A2))) (NOT (EQUAL (STR::EXPR STR::A1 STR::X1 B N) (STR::EXPR STR::A2 STR::X2 B N)))) :HINTS (("Goal" :IN-THEORY (DISABLE STR::EXPR STR::MOD-OF-EXPR) :USE ((:INSTANCE STR::MOD-OF-EXPR) (:INSTANCE STR::MOD-OF-EXPR (STR::A1 STR::A2) (STR::X1 STR::X2))))))) (DEFTHMD STR::ARITH-LEMMA-1 (IMPLIES (AND (NATP STR::A1) (NATP STR::A2) (NATP STR::X1) (NATP STR::X2) (NATP N) (NATP B) (< STR::A1 (EXPT B N)) (< STR::A2 (EXPT B N)) (<= STR::X1 B) (<= STR::X2 B) (NOT (EQUAL STR::A1 STR::A2))) (NOT (EQUAL (+ STR::A1 (* STR::X1 (EXPT B N))) (+ STR::A2 (* STR::X2 (EXPT B N)))))) :HINTS (("Goal" :IN-THEORY (ENABLE STR::EXPR) :USE ((:INSTANCE STR::MAIN-LEMMA))))))) (LOCAL (DEFTHM STR::LEMMA-1 (IMPLIES (AND (NOT (EQUAL (STR::DIGIT-LIST-VALUE STR::X2) (STR::DIGIT-LIST-VALUE STR::Y2))) (NOT (EQUAL STR::X2 STR::Y2)) (CHARACTERP STR::X1) (CHARACTERP STR::Y1) (CHARACTER-LISTP STR::X2) (CHARACTER-LISTP STR::Y2) (STR::DIGITP STR::X1) (STR::DIGITP STR::Y1) (STR::DIGIT-LISTP STR::X2) (STR::DIGIT-LISTP STR::Y2) (EQUAL (LEN STR::X2) (LEN STR::Y2))) (NOT (EQUAL (+ (STR::DIGIT-LIST-VALUE STR::X2) (* (STR::DIGIT-VAL STR::X1) (EXPT 10 (LEN STR::X2)))) (+ (STR::DIGIT-LIST-VALUE STR::Y2) (* (STR::DIGIT-VAL STR::Y1) (EXPT 10 (LEN STR::X2))))))) :HINTS (("Goal" :USE ((:INSTANCE STR::ARITH-LEMMA-1 (STR::A1 (STR::DIGIT-LIST-VALUE STR::X2)) (STR::A2 (STR::DIGIT-LIST-VALUE STR::Y2)) (STR::X1 (STR::DIGIT-VAL STR::X1)) (STR::X2 (STR::DIGIT-VAL STR::Y1)) (B 10) (N (LEN STR::X2)))))))) (LOCAL (DEFUN STR::MY-INDUCTION (X Y) (IF (AND (CONSP X) (CONSP Y)) (STR::MY-INDUCTION (CDR X) (CDR Y)) NIL))) (LOCAL (DEFTHM STR::LEMMA-2 (IMPLIES (AND (EQUAL (LEN X) (LEN Y)) (CHARACTER-LISTP X) (CHARACTER-LISTP Y) (STR::DIGIT-LISTP X) (STR::DIGIT-LISTP Y)) (EQUAL (EQUAL (STR::DIGIT-LIST-VALUE X) (STR::DIGIT-LIST-VALUE Y)) (EQUAL X Y))) :HINTS (("Goal" :INDUCT (STR::MY-INDUCTION X Y) :IN-THEORY (ENABLE STR::DIGIT-LISTP STR::DIGIT-LIST-VALUE COMMUTATIVITY-OF-+))))) (LOCAL (DEFTHM STR::LEMMA-3 (IMPLIES (AND (EQUAL (LEN (STR::TAKE-LEADING-DIGITS Y)) (LEN (STR::TAKE-LEADING-DIGITS X))) (EQUAL (STR::DIGIT-LIST-VALUE (STR::TAKE-LEADING-DIGITS Y)) (STR::DIGIT-LIST-VALUE (STR::TAKE-LEADING-DIGITS X))) (STR::CHARLISTEQV (STR::SKIP-LEADING-DIGITS X) (STR::SKIP-LEADING-DIGITS Y))) (EQUAL (STR::CHARLISTEQV X Y) T)) :HINTS (("Goal" :IN-THEORY (ENABLE STR::TAKE-LEADING-DIGITS STR::SKIP-LEADING-DIGITS STR::CHARLISTEQV STR::DIGIT-LIST-VALUE))))) (DEFTHM STR::CHARLISTNAT<-TRICHOTOMY-WEAK (IMPLIES (AND (NOT (STR::CHARLISTNAT< X Y)) (NOT (STR::CHARLISTNAT< Y X))) (EQUAL (STR::CHARLISTEQV X Y) T)) :HINTS (("Goal" :IN-THEORY (E/D (STR::CHAR<-TRICHOTOMY-STRONG) (STR::BOUND-OF-LEN-OF-TAKE-LEADING-DIGITS STR::TAKE-LEADING-DIGITS-WHEN-DIGIT-LISTP RIGHT-CANCELLATION-FOR-+ STR::CHARLISTNAT<-ANTISYMMETRIC STR::CHARLISTNAT<-IRREFLEXIVE))))) (DEFTHM STR::CHARLISTNAT<-TRICHOTOMY-STRONG (EQUAL (STR::CHARLISTNAT< X Y) (AND (NOT (STR::CHARLISTEQV X Y)) (NOT (STR::CHARLISTNAT< Y X)))) :RULE-CLASSES ((:REWRITE :LOOP-STOPPER ((X Y)))))))) (RECORD-EXPANSION (MAKE-EVENT (LET* ((XDOC::NAME (QUOTE STR::CHARLISTNAT<)) (XDOC::PARENTS (QUOTE (STR::ORDERING))) (XDOC::SHORT (QUOTE "Mixed alphanumeric character-list less-than test.")) (XDOC::EXTENSION (QUOTE NIL)) (XDOC::WRLD (W STATE)) (XDOC::TRIPS (REVERSED-WORLD-SINCE-EVENT XDOC::WRLD (QUOTE (TABLE INTRO-TABLE :MARK (QUOTE STR::CHARLISTNAT<))) 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 charlistnat<) determines if the character list @('x') is
\"smaller\" than the character list @('y'), using an ordering that is nice for
humans.</p>

<p>This is almost an ordinary case-sensitive lexicographic ordering.  But,
unlike a simple lexicographic order, we identify sequences of natural number
digits and group them together so that they can be sorted numerically.</p>

<p>Even though this function operates on character lists, let's just talk about
strings instead since they are easier to write down.  If you give most string
sorts a list of inputs like \"x0\" through \"x11\", they will end up in a
peculiar order:</p>

@({\"x0\", \"x1\", \"x10\", \"x11\", \"x2\", \"x3\", ... \"x9\"})

<p>But in @('charlistnat<'), we see the adjacent digits as bundles and sort
them as numbers.  This leads to a nicer ordering:</p>

@({\"x0\", \"x1\", \"x2\", ..., \"x9\", \"x10\", \"x11\"})

<p>This is almost entirely straightforward.  One twist is how to accommodate
leading zeroes.  Our approach is: instead of grouping adjacent digits and
treating them as a natural number, treat them as a pair with a value and a
length.  We then sort these pairs first by value, and then by length.  Hence, a
string such as \"x0\" is considered to be less than \"x00\", etc.</p>

<p>See also @(see strnat<) and @(see icharlist<).</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::CHARLISTNAT<) (:BASE-PKG . STR::ACL2-PKG-WITNESS) (:PARENTS STR::ORDERING) (:SHORT . "Mixed alphanumeric character-list less-than test.") (:LONG . "<p>@(call charlistnat<) determines if the character list @('x') is
\"smaller\" than the character list @('y'), using an ordering that is nice for
humans.</p>

<p>This is almost an ordinary case-sensitive lexicographic ordering.  But,
unlike a simple lexicographic order, we identify sequences of natural number
digits and group them together so that they can be sorted numerically.</p>

<p>Even though this function operates on character lists, let's just talk about
strings instead since they are easier to write down.  If you give most string
sorts a list of inputs like \"x0\" through \"x11\", they will end up in a
peculiar order:</p>

@({\"x0\", \"x1\", \"x10\", \"x11\", \"x2\", \"x3\", ... \"x9\"})

<p>But in @('charlistnat<'), we see the adjacent digits as bundles and sort
them as numbers.  This leads to a nicer ordering:</p>

@({\"x0\", \"x1\", \"x2\", ..., \"x9\", \"x10\", \"x11\"})

<p>This is almost entirely straightforward.  One twist is how to accommodate
leading zeroes.  Our approach is: instead of grouping adjacent digits and
treating them as a natural number, treat them as a pair with a value and a
length.  We then sort these pairs first by value, and then by length.  Hence, a
string such as \"x0\" is considered to be less than \"x00\", etc.</p>

<p>See also @(see strnat<) and @(see icharlist<).</p>

<h3>Definitions and Theorems</h3>@(def |STR|::|CHARLISTNAT<|)
@(def |STR|::|CHARLISTEQV-IMPLIES-EQUAL-CHARLISTNAT<-1|)
@(def |STR|::|CHARLISTEQV-IMPLIES-EQUAL-CHARLISTNAT<-2|)
@(def |STR|::|CHARLISTNAT<-IRREFLEXIVE|)
@(def |STR|::|CHARLISTNAT<-ANTISYMMETRIC|)
@(def |STR|::|CHARLISTNAT<-TRANSITIVE|)
@(def |STR|::|CHARLISTNAT<-TRICHOTOMY-WEAK|)
@(def |STR|::|CHARLISTNAT<-TRICHOTOMY-STRONG|)") (:FROM . "[books]/str/strnatless.lisp"))) (XDOC::GET-XDOC-TABLE WORLD))) (VALUE-TRIPLE (QUOTE (DEFXDOC STR::CHARLISTNAT<)))))) (VALUE-TRIPLE (QUOTE STR::CHARLISTNAT<))))) (7 RECORD-EXPANSION (DEFSECTION STR::STRNAT<-AUX :PARENTS (STR::STRNAT<) :SHORT "Implementation of @(see strnat<)." :LONG "<p>@(call strnat<-aux) is basically the adaptation of @(see
charlistnat<) for strings.  Here, X and Y are the strings being compared, and
XL and YL are their pre-computed lengths.  XN and YN are the indices into the
two strings that are our current positions.</p>

<p>BOZO why do we have XN and YN separately?  It seems like we should only need
one index.</p>" (LOCAL (IN-THEORY (DISABLE NTH-WHEN-BIGGER NEGATIVE-WHEN-NATP DEFAULT-+-2 DEFAULT-+-1 DEFAULT-<-2 COMMUTATIVITY-OF-+ DEFAULT-<-1 |x < y  =>  0 < y-x| |x < y  =>  0 < -x+y| STR::CHAR<-TRICHOTOMY-STRONG STR::CHAR<-ANTISYMMETRIC STR::CHAR<-TRICHOTOMY-WEAK STR::CHAR<-TRANSITIVE NEGATIVE-WHEN-NATP NATP-RW EXPT DEFAULT-CAR DEFAULT-CDR (:REWRITE STR::PROGRESS-OF-PARSE-NAT-FROM-STRING)))) (DEFUND STR::STRNAT<-AUX (X Y STR::XN STR::YN STR::XL STR::YL) (DECLARE (TYPE STRING X) (TYPE STRING Y) (TYPE INTEGER STR::XN) (TYPE INTEGER STR::YN) (TYPE INTEGER STR::XL) (TYPE INTEGER STR::YL) (XARGS :GUARD (AND (STRINGP X) (STRINGP Y) (NATP STR::XN) (NATP STR::YN) (EQUAL STR::XL (LENGTH X)) (EQUAL STR::YL (LENGTH Y)) (<= STR::XN STR::XL) (<= STR::YN STR::YL)) :VERIFY-GUARDS NIL :MEASURE (LET* ((X (IF (STRINGP X) X "")) (Y (IF (STRINGP Y) Y "")) (STR::XN (NFIX STR::XN)) (STR::YN (NFIX STR::YN)) (STR::XL (LENGTH X)) (STR::YL (LENGTH Y))) (NFIX (+ (- STR::YL STR::YN) (- STR::XL STR::XN)))) :HINTS (("Goal" :IN-THEORY (DISABLE STR::VAL-OF-PARSE-NAT-FROM-STRING STR::LEN-OF-PARSE-NAT-FROM-STRING)))) (IGNORABLE STR::XL STR::YL)) (MBE :LOGIC (LET* ((X (IF (STRINGP X) X "")) (Y (IF (STRINGP Y) Y "")) (STR::XN (NFIX STR::XN)) (STR::YN (NFIX STR::YN)) (STR::XL (LENGTH X)) (STR::YL (LENGTH Y))) (COND ((ZP (- STR::YL STR::YN)) NIL) ((ZP (- STR::XL STR::XN)) T) ((AND (STR::DIGITP (CHAR X STR::XN)) (STR::DIGITP (CHAR Y STR::YN))) (B* (((MV STR::V1 STR::L1) (STR::PARSE-NAT-FROM-STRING X 0 0 STR::XN STR::XL)) ((MV STR::V2 STR::L2) (STR::PARSE-NAT-FROM-STRING Y 0 0 STR::YN STR::YL))) (COND ((OR (< STR::V1 STR::V2) (AND (INT= STR::V1 STR::V2) (< STR::L1 STR::L2))) T) ((OR (< STR::V2 STR::V1) (AND (INT= STR::V1 STR::V2) (< STR::L2 STR::L1))) NIL) (T (STR::STRNAT<-AUX X Y (+ STR::XN STR::L1) (+ STR::YN STR::L2) STR::XL STR::YL))))) ((CHAR< (CHAR X STR::XN) (CHAR Y STR::YN)) T) ((CHAR< (CHAR Y STR::YN) (CHAR X STR::XN)) NIL) (T (STR::STRNAT<-AUX X Y (+ 1 STR::XN) (+ 1 STR::YN) STR::XL STR::YL)))) :EXEC (COND ((INT= STR::YN STR::YL) NIL) ((INT= STR::XN STR::XL) T) (T (LET* ((STR::CHAR-X (THE CHARACTER (CHAR (THE STRING X) (THE INTEGER STR::XN)))) (STR::CHAR-Y (THE CHARACTER (CHAR (THE STRING Y) (THE INTEGER STR::YN)))) (STR::CODE-X (THE (UNSIGNED-BYTE 8) (CHAR-CODE (THE CHARACTER STR::CHAR-X)))) (STR::CODE-Y (THE (UNSIGNED-BYTE 8) (CHAR-CODE (THE CHARACTER STR::CHAR-Y))))) (DECLARE (TYPE CHARACTER STR::CHAR-X) (TYPE CHARACTER STR::CHAR-Y) (TYPE (UNSIGNED-BYTE 8) STR::CODE-X) (TYPE (UNSIGNED-BYTE 8) STR::CODE-Y)) (COND ((AND (<= (THE (UNSIGNED-BYTE 8) 48) (THE (UNSIGNED-BYTE 8) STR::CODE-X)) (<= (THE (UNSIGNED-BYTE 8) STR::CODE-X) (THE (UNSIGNED-BYTE 8) 57)) (<= (THE (UNSIGNED-BYTE 8) 48) (THE (UNSIGNED-BYTE 8) STR::CODE-Y)) (<= (THE (UNSIGNED-BYTE 8) STR::CODE-Y) (THE (UNSIGNED-BYTE 8) 57))) (B* (((MV STR::V1 STR::L1) (STR::PARSE-NAT-FROM-STRING (THE STRING X) (THE INTEGER 0) (THE INTEGER 0) (THE INTEGER STR::XN) (THE INTEGER STR::XL))) ((MV STR::V2 STR::L2) (STR::PARSE-NAT-FROM-STRING (THE STRING Y) (THE INTEGER 0) (THE INTEGER 0) (THE INTEGER STR::YN) (THE INTEGER STR::YL)))) (COND ((OR (< (THE INTEGER STR::V1) (THE INTEGER STR::V2)) (AND (INT= STR::V1 STR::V2) (< (THE INTEGER STR::L1) (THE INTEGER STR::L2)))) T) ((OR (< (THE INTEGER STR::V2) (THE INTEGER STR::V1)) (AND (INT= STR::V1 STR::V2) (< (THE INTEGER STR::L2) (THE INTEGER STR::L1)))) NIL) (T (STR::STRNAT<-AUX (THE STRING X) (THE STRING Y) (THE INTEGER (+ (THE INTEGER STR::XN) (THE INTEGER STR::L1))) (THE INTEGER (+ (THE INTEGER STR::YN) (THE INTEGER STR::L2))) (THE INTEGER STR::XL) (THE INTEGER STR::YL)))))) ((< (THE (UNSIGNED-BYTE 8) STR::CODE-X) (THE (UNSIGNED-BYTE 8) STR::CODE-Y)) T) ((< (THE (UNSIGNED-BYTE 8) STR::CODE-Y) (THE (UNSIGNED-BYTE 8) STR::CODE-X)) NIL) (T (STR::STRNAT<-AUX (THE STRING X) (THE STRING Y) (THE INTEGER (+ (THE INTEGER 1) (THE INTEGER STR::XN))) (THE INTEGER (+ (THE INTEGER 1) (THE INTEGER STR::YN))) (THE INTEGER STR::XL) (THE INTEGER STR::YL))))))))) (LOCAL (IN-THEORY (ENABLE STR::STRNAT<-AUX))) (SET-INHIBIT-WARNINGS "theory") (ENCAPSULATE NIL (LOCAL (IN-THEORY (DISABLE NTH-WHEN-BIGGER STR::TAKE-LEADING-DIGITS-WHEN-DIGIT-LISTP STR::DIGIT-LISTP-WHEN-NOT-CONSP (:TYPE-PRESCRIPTION CHARACTER-LISTP) (:TYPE-PRESCRIPTION EQLABLE-LISTP) (:TYPE-PRESCRIPTION ATOM-LISTP) (:TYPE-PRESCRIPTION STR::DIGITP$INLINE) (:TYPE-PRESCRIPTION STR::STRNAT<-AUX) (:TYPE-PRESCRIPTION CHAR<) DEFAULT-CHAR-CODE STR::CHAR<-ANTISYMMETRIC STR::CHAR<-TRICHOTOMY-STRONG DEFAULT-<-1 DEFAULT-<-2 DEFAULT-+-1 DEFAULT-+-2 OPEN-SMALL-NTHCDR NTHCDR-WHEN-ZP NTHCDR-WHEN-ATOM |x < y  =>  0 < -x+y| NTHCDR LEN NTH NOT STR::STRNAT<-AUX NATP-FC-1 NATP-FC-2 (:FORWARD-CHAINING EQLABLE-LISTP-FORWARD-TO-ATOM-LISTP) (:FORWARD-CHAINING CHARACTER-LISTP-FORWARD-TO-EQLABLE-LISTP) (:FORWARD-CHAINING ATOM-LISTP-FORWARD-TO-TRUE-LISTP)))) (VERIFY-GUARDS STR::STRNAT<-AUX :HINTS ((AND STABLE-UNDER-SIMPLIFICATIONP (QUOTE (:IN-THEORY (ENABLE STR::DIGITP STR::DIGIT-VAL STR::CHAR-FIX CHAR<))))))) (LOCAL (DEFTHM STR::SKIP-LEADING-DIGITS-TO-NTHCDR (IMPLIES (FORCE (TRUE-LISTP X)) (EQUAL (STR::SKIP-LEADING-DIGITS X) (NTHCDR (LEN (STR::TAKE-LEADING-DIGITS X)) X))) :HINTS (("Goal" :IN-THEORY (ENABLE STR::SKIP-LEADING-DIGITS STR::TAKE-LEADING-DIGITS))))) (DEFTHM STR::STRNAT<-AUX-CORRECT (IMPLIES (AND (STRINGP X) (STRINGP Y) (NATP STR::XN) (NATP STR::YN) (EQUAL STR::XL (LENGTH X)) (EQUAL STR::YL (LENGTH Y)) (<= STR::XN STR::XL) (<= STR::YN STR::YL)) (EQUAL (STR::STRNAT<-AUX X Y STR::XN STR::YN STR::XL STR::YL) (STR::CHARLISTNAT< (NTHCDR STR::XN (EXPLODE X)) (NTHCDR STR::YN (EXPLODE Y))))) :HINTS (("Goal" :INDUCT (STR::STRNAT<-AUX X Y STR::XN STR::YN STR::XL STR::YL) :EXPAND ((STR::CHARLISTNAT< (NTHCDR STR::XN (EXPLODE X)) (NTHCDR STR::YN (EXPLODE Y))) (:FREE (STR::XL STR::YL) (STR::STRNAT<-AUX X Y STR::XN STR::YN STR::XL STR::YL))) :IN-THEORY (E/D (STR::CHARLISTNAT< COMMUTATIVITY-OF-+) (STR::CHARLISTNAT<-ANTISYMMETRIC STR::CHARLISTNAT<-TRICHOTOMY-STRONG STR::TAKE-LEADING-DIGITS-WHEN-DIGIT-LISTP STR::DIGIT-LISTP-WHEN-NOT-CONSP STR::CHARLISTNAT< (:DEFINITION STR::STRNAT<-AUX) DEFAULT-+-1 DEFAULT-+-2 NTH-WHEN-BIGGER)) :DO-NOT (QUOTE (GENERALIZE FERTILIZE)))))) (WITH-OUTPUT :STACK :PUSH :OFF :ALL :ON ERROR (PROGN (TABLE INTRO-TABLE :MARK (QUOTE STR::STRNAT<-AUX)) (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (LOCAL (IN-THEORY (DISABLE NTH-WHEN-BIGGER NEGATIVE-WHEN-NATP DEFAULT-+-2 DEFAULT-+-1 DEFAULT-<-2 COMMUTATIVITY-OF-+ DEFAULT-<-1 |x < y  =>  0 < y-x| |x < y  =>  0 < -x+y| STR::CHAR<-TRICHOTOMY-STRONG STR::CHAR<-ANTISYMMETRIC STR::CHAR<-TRICHOTOMY-WEAK STR::CHAR<-TRANSITIVE NEGATIVE-WHEN-NATP NATP-RW EXPT DEFAULT-CAR DEFAULT-CDR (:REWRITE STR::PROGRESS-OF-PARSE-NAT-FROM-STRING)))) (DEFUND STR::STRNAT<-AUX (X Y STR::XN STR::YN STR::XL STR::YL) (DECLARE (TYPE STRING X) (TYPE STRING Y) (TYPE INTEGER STR::XN) (TYPE INTEGER STR::YN) (TYPE INTEGER STR::XL) (TYPE INTEGER STR::YL) (XARGS :GUARD (AND (STRINGP X) (STRINGP Y) (NATP STR::XN) (NATP STR::YN) (EQUAL STR::XL (LENGTH X)) (EQUAL STR::YL (LENGTH Y)) (<= STR::XN STR::XL) (<= STR::YN STR::YL)) :VERIFY-GUARDS NIL :MEASURE (LET* ((X (IF (STRINGP X) X "")) (Y (IF (STRINGP Y) Y "")) (STR::XN (NFIX STR::XN)) (STR::YN (NFIX STR::YN)) (STR::XL (LENGTH X)) (STR::YL (LENGTH Y))) (NFIX (+ (- STR::YL STR::YN) (- STR::XL STR::XN)))) :HINTS (("Goal" :IN-THEORY (DISABLE STR::VAL-OF-PARSE-NAT-FROM-STRING STR::LEN-OF-PARSE-NAT-FROM-STRING)))) (IGNORABLE STR::XL STR::YL)) (MBE :LOGIC (LET* ((X (IF (STRINGP X) X "")) (Y (IF (STRINGP Y) Y "")) (STR::XN (NFIX STR::XN)) (STR::YN (NFIX STR::YN)) (STR::XL (LENGTH X)) (STR::YL (LENGTH Y))) (COND ((ZP (- STR::YL STR::YN)) NIL) ((ZP (- STR::XL STR::XN)) T) ((AND (STR::DIGITP (CHAR X STR::XN)) (STR::DIGITP (CHAR Y STR::YN))) (B* (((MV STR::V1 STR::L1) (STR::PARSE-NAT-FROM-STRING X 0 0 STR::XN STR::XL)) ((MV STR::V2 STR::L2) (STR::PARSE-NAT-FROM-STRING Y 0 0 STR::YN STR::YL))) (COND ((OR (< STR::V1 STR::V2) (AND (INT= STR::V1 STR::V2) (< STR::L1 STR::L2))) T) ((OR (< STR::V2 STR::V1) (AND (INT= STR::V1 STR::V2) (< STR::L2 STR::L1))) NIL) (T (STR::STRNAT<-AUX X Y (+ STR::XN STR::L1) (+ STR::YN STR::L2) STR::XL STR::YL))))) ((CHAR< (CHAR X STR::XN) (CHAR Y STR::YN)) T) ((CHAR< (CHAR Y STR::YN) (CHAR X STR::XN)) NIL) (T (STR::STRNAT<-AUX X Y (+ 1 STR::XN) (+ 1 STR::YN) STR::XL STR::YL)))) :EXEC (COND ((INT= STR::YN STR::YL) NIL) ((INT= STR::XN STR::XL) T) (T (LET* ((STR::CHAR-X (THE CHARACTER (CHAR (THE STRING X) (THE INTEGER STR::XN)))) (STR::CHAR-Y (THE CHARACTER (CHAR (THE STRING Y) (THE INTEGER STR::YN)))) (STR::CODE-X (THE (UNSIGNED-BYTE 8) (CHAR-CODE (THE CHARACTER STR::CHAR-X)))) (STR::CODE-Y (THE (UNSIGNED-BYTE 8) (CHAR-CODE (THE CHARACTER STR::CHAR-Y))))) (DECLARE (TYPE CHARACTER STR::CHAR-X) (TYPE CHARACTER STR::CHAR-Y) (TYPE (UNSIGNED-BYTE 8) STR::CODE-X) (TYPE (UNSIGNED-BYTE 8) STR::CODE-Y)) (COND ((AND (<= (THE (UNSIGNED-BYTE 8) 48) (THE (UNSIGNED-BYTE 8) STR::CODE-X)) (<= (THE (UNSIGNED-BYTE 8) STR::CODE-X) (THE (UNSIGNED-BYTE 8) 57)) (<= (THE (UNSIGNED-BYTE 8) 48) (THE (UNSIGNED-BYTE 8) STR::CODE-Y)) (<= (THE (UNSIGNED-BYTE 8) STR::CODE-Y) (THE (UNSIGNED-BYTE 8) 57))) (B* (((MV STR::V1 STR::L1) (STR::PARSE-NAT-FROM-STRING (THE STRING X) (THE INTEGER 0) (THE INTEGER 0) (THE INTEGER STR::XN) (THE INTEGER STR::XL))) ((MV STR::V2 STR::L2) (STR::PARSE-NAT-FROM-STRING (THE STRING Y) (THE INTEGER 0) (THE INTEGER 0) (THE INTEGER STR::YN) (THE INTEGER STR::YL)))) (COND ((OR (< (THE INTEGER STR::V1) (THE INTEGER STR::V2)) (AND (INT= STR::V1 STR::V2) (< (THE INTEGER STR::L1) (THE INTEGER STR::L2)))) T) ((OR (< (THE INTEGER STR::V2) (THE INTEGER STR::V1)) (AND (INT= STR::V1 STR::V2) (< (THE INTEGER STR::L2) (THE INTEGER STR::L1)))) NIL) (T (STR::STRNAT<-AUX (THE STRING X) (THE STRING Y) (THE INTEGER (+ (THE INTEGER STR::XN) (THE INTEGER STR::L1))) (THE INTEGER (+ (THE INTEGER STR::YN) (THE INTEGER STR::L2))) (THE INTEGER STR::XL) (THE INTEGER STR::YL)))))) ((< (THE (UNSIGNED-BYTE 8) STR::CODE-X) (THE (UNSIGNED-BYTE 8) STR::CODE-Y)) T) ((< (THE (UNSIGNED-BYTE 8) STR::CODE-Y) (THE (UNSIGNED-BYTE 8) STR::CODE-X)) NIL) (T (STR::STRNAT<-AUX (THE STRING X) (THE STRING Y) (THE INTEGER (+ (THE INTEGER 1) (THE INTEGER STR::XN))) (THE INTEGER (+ (THE INTEGER 1) (THE INTEGER STR::YN))) (THE INTEGER STR::XL) (THE INTEGER STR::YL))))))))) (LOCAL (IN-THEORY (ENABLE STR::STRNAT<-AUX))) (SET-INHIBIT-WARNINGS "theory") (ENCAPSULATE NIL (LOCAL (IN-THEORY (DISABLE NTH-WHEN-BIGGER STR::TAKE-LEADING-DIGITS-WHEN-DIGIT-LISTP STR::DIGIT-LISTP-WHEN-NOT-CONSP (:TYPE-PRESCRIPTION CHARACTER-LISTP) (:TYPE-PRESCRIPTION EQLABLE-LISTP) (:TYPE-PRESCRIPTION ATOM-LISTP) (:TYPE-PRESCRIPTION STR::DIGITP$INLINE) (:TYPE-PRESCRIPTION STR::STRNAT<-AUX) (:TYPE-PRESCRIPTION CHAR<) DEFAULT-CHAR-CODE STR::CHAR<-ANTISYMMETRIC STR::CHAR<-TRICHOTOMY-STRONG DEFAULT-<-1 DEFAULT-<-2 DEFAULT-+-1 DEFAULT-+-2 OPEN-SMALL-NTHCDR NTHCDR-WHEN-ZP NTHCDR-WHEN-ATOM |x < y  =>  0 < -x+y| NTHCDR LEN NTH NOT STR::STRNAT<-AUX NATP-FC-1 NATP-FC-2 (:FORWARD-CHAINING EQLABLE-LISTP-FORWARD-TO-ATOM-LISTP) (:FORWARD-CHAINING CHARACTER-LISTP-FORWARD-TO-EQLABLE-LISTP) (:FORWARD-CHAINING ATOM-LISTP-FORWARD-TO-TRUE-LISTP)))) (VERIFY-GUARDS STR::STRNAT<-AUX :HINTS ((AND STABLE-UNDER-SIMPLIFICATIONP (QUOTE (:IN-THEORY (ENABLE STR::DIGITP STR::DIGIT-VAL STR::CHAR-FIX CHAR<))))))) (LOCAL (DEFTHM STR::SKIP-LEADING-DIGITS-TO-NTHCDR (IMPLIES (FORCE (TRUE-LISTP X)) (EQUAL (STR::SKIP-LEADING-DIGITS X) (NTHCDR (LEN (STR::TAKE-LEADING-DIGITS X)) X))) :HINTS (("Goal" :IN-THEORY (ENABLE STR::SKIP-LEADING-DIGITS STR::TAKE-LEADING-DIGITS))))) (DEFTHM STR::STRNAT<-AUX-CORRECT (IMPLIES (AND (STRINGP X) (STRINGP Y) (NATP STR::XN) (NATP STR::YN) (EQUAL STR::XL (LENGTH X)) (EQUAL STR::YL (LENGTH Y)) (<= STR::XN STR::XL) (<= STR::YN STR::YL)) (EQUAL (STR::STRNAT<-AUX X Y STR::XN STR::YN STR::XL STR::YL) (STR::CHARLISTNAT< (NTHCDR STR::XN (EXPLODE X)) (NTHCDR STR::YN (EXPLODE Y))))) :HINTS (("Goal" :INDUCT (STR::STRNAT<-AUX X Y STR::XN STR::YN STR::XL STR::YL) :EXPAND ((STR::CHARLISTNAT< (NTHCDR STR::XN (EXPLODE X)) (NTHCDR STR::YN (EXPLODE Y))) (:FREE (STR::XL STR::YL) (STR::STRNAT<-AUX X Y STR::XN STR::YN STR::XL STR::YL))) :IN-THEORY (E/D (STR::CHARLISTNAT< COMMUTATIVITY-OF-+) (STR::CHARLISTNAT<-ANTISYMMETRIC STR::CHARLISTNAT<-TRICHOTOMY-STRONG STR::TAKE-LEADING-DIGITS-WHEN-DIGIT-LISTP STR::DIGIT-LISTP-WHEN-NOT-CONSP STR::CHARLISTNAT< (:DEFINITION STR::STRNAT<-AUX) DEFAULT-+-1 DEFAULT-+-2 NTH-WHEN-BIGGER)) :DO-NOT (QUOTE (GENERALIZE FERTILIZE))))))) (RECORD-EXPANSION (MAKE-EVENT (LET* ((XDOC::NAME (QUOTE STR::STRNAT<-AUX)) (XDOC::PARENTS (QUOTE (STR::STRNAT<))) (XDOC::SHORT (QUOTE "Implementation of @(see strnat<).")) (XDOC::EXTENSION (QUOTE NIL)) (XDOC::WRLD (W STATE)) (XDOC::TRIPS (REVERSED-WORLD-SINCE-EVENT XDOC::WRLD (QUOTE (TABLE INTRO-TABLE :MARK (QUOTE STR::STRNAT<-AUX))) 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 strnat<-aux) is basically the adaptation of @(see
charlistnat<) for strings.  Here, X and Y are the strings being compared, and
XL and YL are their pre-computed lengths.  XN and YN are the indices into the
two strings that are our current positions.</p>

<p>BOZO why do we have XN and YN separately?  It seems like we should only need
one index.</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::STRNAT<-AUX) (:BASE-PKG . STR::ACL2-PKG-WITNESS) (:PARENTS STR::STRNAT<) (:SHORT . "Implementation of @(see strnat<).") (:LONG . "<p>@(call strnat<-aux) is basically the adaptation of @(see
charlistnat<) for strings.  Here, X and Y are the strings being compared, and
XL and YL are their pre-computed lengths.  XN and YN are the indices into the
two strings that are our current positions.</p>

<p>BOZO why do we have XN and YN separately?  It seems like we should only need
one index.</p>

<h3>Definitions and Theorems</h3>@(def |STR|::|STRNAT<-AUX|)
@(def |STR|::|STRNAT<-AUX-CORRECT|)") (:FROM . "[books]/str/strnatless.lisp"))) (XDOC::GET-XDOC-TABLE WORLD))) (VALUE-TRIPLE (QUOTE (DEFXDOC STR::STRNAT<-AUX)))))) (VALUE-TRIPLE (QUOTE STR::STRNAT<-AUX))))) (8 RECORD-EXPANSION (DEFSECTION STR::STRNAT< :PARENTS (STR::ORDERING) :SHORT "Mixed alphanumeric string less-than test." :LONG "<p>@(call strnat<) determines if the string @('x') is \"smaller\"
than the string @('y'), using an ordering that is nice for humans.</p>

<p>See @(see charlistnat<) for a description of this order.</p>

<p>We avoid coercing the strings into character lists, and this is altogether
pretty fast.</p>" (DEFINLINED STR::STRNAT< (X Y) (DECLARE (TYPE STRING X Y)) (MBE :LOGIC (STR::CHARLISTNAT< (EXPLODE X) (EXPLODE Y)) :EXEC (STR::STRNAT<-AUX (THE STRING X) (THE STRING Y) (THE INTEGER 0) (THE INTEGER 0) (THE INTEGER (LENGTH (THE STRING X))) (THE INTEGER (LENGTH (THE STRING Y)))))) (LOCAL (IN-THEORY (ENABLE STR::STRNAT<))) (DEFCONG STR::STREQV EQUAL (STR::STRNAT< X Y) 1) (DEFCONG STR::STREQV EQUAL (STR::STRNAT< X Y) 2) (DEFTHM STR::STRNAT<-IRREFLEXIVE (NOT (STR::STRNAT< X X))) (DEFTHM STR::STRNAT<-ANTISYMMETRIC (IMPLIES (STR::STRNAT< X Y) (NOT (STR::STRNAT< Y X)))) (DEFTHM STR::STRNAT<-TRANSITIVE (IMPLIES (AND (STR::STRNAT< X Y) (STR::STRNAT< Y Z)) (STR::STRNAT< X Z))) (DEFTHM STR::STRNAT<-TRANSITIVE-ALT (IMPLIES (AND (STR::STRNAT< Y Z) (STR::STRNAT< X Y)) (STR::STRNAT< X Z)))) (WITH-OUTPUT :STACK :PUSH :OFF :ALL :ON ERROR (PROGN (TABLE INTRO-TABLE :MARK (QUOTE STR::STRNAT<)) (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (DEFINLINED STR::STRNAT< (X Y) (DECLARE (TYPE STRING X Y)) (MBE :LOGIC (STR::CHARLISTNAT< (EXPLODE X) (EXPLODE Y)) :EXEC (STR::STRNAT<-AUX (THE STRING X) (THE STRING Y) (THE INTEGER 0) (THE INTEGER 0) (THE INTEGER (LENGTH (THE STRING X))) (THE INTEGER (LENGTH (THE STRING Y)))))) (LOCAL (IN-THEORY (ENABLE STR::STRNAT<))) (DEFCONG STR::STREQV EQUAL (STR::STRNAT< X Y) 1) (DEFCONG STR::STREQV EQUAL (STR::STRNAT< X Y) 2) (DEFTHM STR::STRNAT<-IRREFLEXIVE (NOT (STR::STRNAT< X X))) (DEFTHM STR::STRNAT<-ANTISYMMETRIC (IMPLIES (STR::STRNAT< X Y) (NOT (STR::STRNAT< Y X)))) (DEFTHM STR::STRNAT<-TRANSITIVE (IMPLIES (AND (STR::STRNAT< X Y) (STR::STRNAT< Y Z)) (STR::STRNAT< X Z))) (DEFTHM STR::STRNAT<-TRANSITIVE-ALT (IMPLIES (AND (STR::STRNAT< Y Z) (STR::STRNAT< X Y)) (STR::STRNAT< X Z))))) (RECORD-EXPANSION (MAKE-EVENT (LET* ((XDOC::NAME (QUOTE STR::STRNAT<)) (XDOC::PARENTS (QUOTE (STR::ORDERING))) (XDOC::SHORT (QUOTE "Mixed alphanumeric string less-than test.")) (XDOC::EXTENSION (QUOTE NIL)) (XDOC::WRLD (W STATE)) (XDOC::TRIPS (REVERSED-WORLD-SINCE-EVENT XDOC::WRLD (QUOTE (TABLE INTRO-TABLE :MARK (QUOTE STR::STRNAT<))) 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 strnat<) determines if the string @('x') is \"smaller\"
than the string @('y'), using an ordering that is nice for humans.</p>

<p>See @(see charlistnat<) for a description of this order.</p>

<p>We avoid coercing the strings into character lists, and this is altogether
pretty 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::STRNAT<) (:BASE-PKG . STR::ACL2-PKG-WITNESS) (:PARENTS STR::ORDERING) (:SHORT . "Mixed alphanumeric string less-than test.") (:LONG . "<p>@(call strnat<) determines if the string @('x') is \"smaller\"
than the string @('y'), using an ordering that is nice for humans.</p>

<p>See @(see charlistnat<) for a description of this order.</p>

<p>We avoid coercing the strings into character lists, and this is altogether
pretty fast.</p>

<h3>Definitions and Theorems</h3>@(def |STR|::|STRNAT<$INLINE|)
@(def |STR|::|STREQV-IMPLIES-EQUAL-STRNAT<-1|)
@(def |STR|::|STREQV-IMPLIES-EQUAL-STRNAT<-2|)
@(def |STR|::|STRNAT<-IRREFLEXIVE|)
@(def |STR|::|STRNAT<-ANTISYMMETRIC|)
@(def |STR|::|STRNAT<-TRANSITIVE|)
@(def |STR|::|STRNAT<-TRANSITIVE-ALT|)") (:FROM . "[books]/str/strnatless.lisp"))) (XDOC::GET-XDOC-TABLE WORLD))) (VALUE-TRIPLE (QUOTE (DEFXDOC STR::STRNAT<)))))) (VALUE-TRIPLE (QUOTE STR::STRNAT<))))))
(("/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/strnatless.lisp" "strnatless" "strnatless" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1797808730) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-3/floor-mod/floor-mod.lisp" "arithmetic-3/floor-mod/floor-mod" "floor-mod" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 14631641)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-3/bind-free/top.lisp" "../bind-free/top" "top" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 248299501)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-3/bind-free/banner.lisp" "banner" "banner" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 915259697)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-3/bind-free/arithmetic-theory.lisp" "arithmetic-theory" "arithmetic-theory" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 732116275)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-3/bind-free/remove-weak-inequalities.lisp" "remove-weak-inequalities" "remove-weak-inequalities" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 105657945)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-3/bind-free/collect.lisp" "collect" "collect" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 864029516)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-3/bind-free/integerp-meta.lisp" "integerp-meta" "integerp-meta" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 750113408)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-3/bind-free/integerp.lisp" "integerp" "integerp" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1374753694)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-3/bind-free/numerator-and-denominator.lisp" "numerator-and-denominator" "numerator-and-denominator" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 122664565)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-3/bind-free/simplify.lisp" "simplify" "simplify" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 2013733040)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-3/bind-free/simplify-helper.lisp" "simplify-helper" "simplify-helper" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1061645425)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-3/bind-free/normalize.lisp" "normalize" "normalize" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1619080936)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-3/bind-free/basic.lisp" "basic" "basic" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 972646001)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-3/bind-free/basic-helper.lisp" "basic-helper" "basic-helper" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 384804126)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-3/bind-free/common.lisp" "common" "common" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1113724693)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-3/bind-free/mini-theories.lisp" "mini-theories" "mini-theories" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 483566967)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-3/bind-free/mini-theories-helper.lisp" "mini-theories-helper" "mini-theories-helper" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 457663279)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-3/pass1/top.lisp" "../pass1/top" "top" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 513558315)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-3/pass1/numerator-and-denominator.lisp" "numerator-and-denominator" "numerator-and-denominator" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 134470975)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-3/pass1/num-and-denom-helper.lisp" "num-and-denom-helper" "num-and-denom-helper" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 784695287)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-3/pass1/non-linear.lisp" "non-linear" "non-linear" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 2126151702)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-3/pass1/mini-theories.lisp" "mini-theories" "mini-theories" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1504975778)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-3/pass1/expt.lisp" "expt" "expt" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 653127144)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-3/pass1/expt-helper.lisp" "expt-helper" "expt-helper" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1661395704)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-3/pass1/prefer-times.lisp" "prefer-times" "prefer-times" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1273493319)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-3/pass1/inequalities.lisp" "inequalities" "inequalities" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 508744284)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-3/pass1/basic-arithmetic.lisp" "basic-arithmetic" "basic-arithmetic" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1246647817)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-3/pass1/basic-arithmetic-helper.lisp" "basic-arithmetic-helper" "basic-arithmetic-helper" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 376534638)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-3/bind-free/building-blocks.lisp" "building-blocks" "building-blocks" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1061889192)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-3/bind-free/default-hint.lisp" "default-hint" "default-hint" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1153949377)) ("/usr/share/acl2-6.3/books/tools/mv-nth.lisp" "tools/mv-nth" "mv-nth" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 82993140) ("/usr/share/acl2-6.3/books/str/digitp.lisp" "digitp" "digitp" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 479290421) ("/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))
1260403326
acl2-books-certs 6.3-5 / usr / share / acl2-6.3 / books / str / strnatless.cert
