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

(IN-PACKAGE "ACL2")
"ACL2 Version 6.3"
:BEGIN-PORTCULLIS-CMDS
(INCLUDE-BOOK "cutil/portcullis" :DIR :SYSTEM)
:END-PORTCULLIS-CMDS
:EXPANSION-ALIST
((5 RECORD-EXPANSION (DEFSECTION STR::STRSUBST-AUX :PARENTS (STR::STRSUBST) :SHORT "Fast implementation of @(see strsubst)." (DEFUND STR::STRSUBST-AUX (STR::OLD STR::NEW X N STR::XL STR::OLDL STR::ACC) (DECLARE (TYPE STRING STR::OLD STR::NEW X) (TYPE (INTEGER 0 *) N STR::XL STR::OLDL) (XARGS :GUARD (AND (STRINGP STR::OLD) (STRINGP STR::NEW) (STRINGP X) (NATP N) (NATP STR::XL) (POSP STR::OLDL) (= STR::OLDL (LENGTH STR::OLD)) (= STR::XL (LENGTH X))) :MEASURE (NFIX (- (NFIX STR::XL) (NFIX N))))) (COND ((MBE :LOGIC (ZP STR::OLDL) :EXEC NIL) STR::ACC) ((MBE :LOGIC (ZP (- (NFIX STR::XL) (NFIX N))) :EXEC (>= N STR::XL)) STR::ACC) ((STR::STRPREFIXP-IMPL STR::OLD X 0 N STR::OLDL STR::XL) (LET ((STR::ACC (STR::REVAPPEND-CHARS STR::NEW STR::ACC))) (STR::STRSUBST-AUX STR::OLD STR::NEW X (THE (INTEGER 0 *) (+ STR::OLDL (THE (INTEGER 0 *) (LNFIX N)))) STR::XL STR::OLDL STR::ACC))) (T (LET ((STR::ACC (CONS (CHAR X N) STR::ACC))) (STR::STRSUBST-AUX STR::OLD STR::NEW X (THE (INTEGER 0 *) (+ 1 (THE (INTEGER 0 *) (LNFIX N)))) STR::XL STR::OLDL STR::ACC))))) (LOCAL (IN-THEORY (ENABLE STR::STRSUBST-AUX))) (DEFTHM STR::CHARACTER-LISTP-OF-STRSUBST-AUX (IMPLIES (AND (STRINGP STR::OLD) (STRINGP STR::NEW) (STRINGP X) (NATP N) (NATP STR::XL) (POSP STR::OLDL) (= STR::OLDL (LENGTH STR::OLD)) (= STR::XL (LENGTH X)) (CHARACTER-LISTP STR::ACC)) (CHARACTER-LISTP (STR::STRSUBST-AUX STR::OLD STR::NEW X N STR::XL STR::OLDL STR::ACC))))) (WITH-OUTPUT :STACK :PUSH :OFF :ALL :ON ERROR (PROGN (TABLE INTRO-TABLE :MARK (QUOTE STR::STRSUBST-AUX)) (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (DEFUND STR::STRSUBST-AUX (STR::OLD STR::NEW X N STR::XL STR::OLDL STR::ACC) (DECLARE (TYPE STRING STR::OLD STR::NEW X) (TYPE (INTEGER 0 *) N STR::XL STR::OLDL) (XARGS :GUARD (AND (STRINGP STR::OLD) (STRINGP STR::NEW) (STRINGP X) (NATP N) (NATP STR::XL) (POSP STR::OLDL) (= STR::OLDL (LENGTH STR::OLD)) (= STR::XL (LENGTH X))) :MEASURE (NFIX (- (NFIX STR::XL) (NFIX N))))) (COND ((MBE :LOGIC (ZP STR::OLDL) :EXEC NIL) STR::ACC) ((MBE :LOGIC (ZP (- (NFIX STR::XL) (NFIX N))) :EXEC (>= N STR::XL)) STR::ACC) ((STR::STRPREFIXP-IMPL STR::OLD X 0 N STR::OLDL STR::XL) (LET ((STR::ACC (STR::REVAPPEND-CHARS STR::NEW STR::ACC))) (STR::STRSUBST-AUX STR::OLD STR::NEW X (THE (INTEGER 0 *) (+ STR::OLDL (THE (INTEGER 0 *) (LNFIX N)))) STR::XL STR::OLDL STR::ACC))) (T (LET ((STR::ACC (CONS (CHAR X N) STR::ACC))) (STR::STRSUBST-AUX STR::OLD STR::NEW X (THE (INTEGER 0 *) (+ 1 (THE (INTEGER 0 *) (LNFIX N)))) STR::XL STR::OLDL STR::ACC))))) (LOCAL (IN-THEORY (ENABLE STR::STRSUBST-AUX))) (DEFTHM STR::CHARACTER-LISTP-OF-STRSUBST-AUX (IMPLIES (AND (STRINGP STR::OLD) (STRINGP STR::NEW) (STRINGP X) (NATP N) (NATP STR::XL) (POSP STR::OLDL) (= STR::OLDL (LENGTH STR::OLD)) (= STR::XL (LENGTH X)) (CHARACTER-LISTP STR::ACC)) (CHARACTER-LISTP (STR::STRSUBST-AUX STR::OLD STR::NEW X N STR::XL STR::OLDL STR::ACC)))))) (RECORD-EXPANSION (MAKE-EVENT (LET* ((XDOC::NAME (QUOTE STR::STRSUBST-AUX)) (XDOC::PARENTS (QUOTE (STR::STRSUBST))) (XDOC::SHORT (QUOTE "Fast implementation of @(see strsubst).")) (XDOC::EXTENSION (QUOTE NIL)) (XDOC::WRLD (W STATE)) (XDOC::TRIPS (REVERSED-WORLD-SINCE-EVENT XDOC::WRLD (QUOTE (TABLE INTRO-TABLE :MARK (QUOTE STR::STRSUBST-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 "") (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::STRSUBST-AUX) (:BASE-PKG . STR::ACL2-PKG-WITNESS) (:PARENTS STR::STRSUBST) (:SHORT . "Fast implementation of @(see strsubst).") (:LONG . "

<h3>Definitions and Theorems</h3>@(def |STR|::|STRSUBST-AUX|)
@(def |STR|::|CHARACTER-LISTP-OF-STRSUBST-AUX|)") (:FROM . "[books]/str/strsubst.lisp"))) (XDOC::GET-XDOC-TABLE WORLD))) (VALUE-TRIPLE (QUOTE (DEFXDOC STR::STRSUBST-AUX)))))) (VALUE-TRIPLE (QUOTE STR::STRSUBST-AUX))))) (6 RECORD-EXPANSION (DEFSECTION STR::STRSUBST :PARENTS (STR::SUBSTITUTION SUBSTITUTE) :SHORT "Replace substrings throughout a string." :LONG "<p>@(call strsubst) replaces each occurrence of @('old') with @('new')
throughout @('x').  Each argument is a string, and a new string is returned.
The replacement is done globally and non-recursively.</p>

<p>Examples:</p>
@({
 (strsubst \"World\" \"Star\" \"Hello, World!\")
   -->
 \"Hello, Star!\"

 (strsubst \"oo\" \"aa\" \"xoooyoo\")
   -->
 \"xaaoyaa\"
})

<p>ACL2 has a built in @(see substitute) function, but it only works on
individual characters, whereas @('strsubst') works on substrings.</p>" (DEFUND STR::STRSUBST (STR::OLD STR::NEW X) (DECLARE (XARGS :GUARD (AND (STRINGP STR::OLD) (STRINGP STR::NEW) (STRINGP X)))) (LET ((STR::OLDL (MBE :LOGIC (LEN (EXPLODE STR::OLD)) :EXEC (LENGTH STR::OLD)))) (IF (ZP STR::OLDL) (MBE :LOGIC (STR::STR-FIX X) :EXEC X) (STR::RCHARS-TO-STRING (STR::STRSUBST-AUX STR::OLD STR::NEW X 0 (LENGTH X) STR::OLDL NIL))))) (LOCAL (IN-THEORY (ENABLE STR::STRSUBST))) (DEFTHM STR::STRINGP-OF-STRSUBST (STRINGP (STR::STRSUBST STR::OLD STR::NEW X)) :RULE-CLASSES :TYPE-PRESCRIPTION) (LOCAL (ASSERT! (EQUAL (STR::STRSUBST "World" "Star" "Hello, World!") "Hello, Star!"))) (LOCAL (ASSERT! (EQUAL (STR::STRSUBST "oo" "aa" "xoooyoo") "xaaoyaa")))) (WITH-OUTPUT :STACK :PUSH :OFF :ALL :ON ERROR (PROGN (TABLE INTRO-TABLE :MARK (QUOTE STR::STRSUBST)) (RECORD-EXPANSION (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (DEFUND STR::STRSUBST (STR::OLD STR::NEW X) (DECLARE (XARGS :GUARD (AND (STRINGP STR::OLD) (STRINGP STR::NEW) (STRINGP X)))) (LET ((STR::OLDL (MBE :LOGIC (LEN (EXPLODE STR::OLD)) :EXEC (LENGTH STR::OLD)))) (IF (ZP STR::OLDL) (MBE :LOGIC (STR::STR-FIX X) :EXEC X) (STR::RCHARS-TO-STRING (STR::STRSUBST-AUX STR::OLD STR::NEW X 0 (LENGTH X) STR::OLDL NIL))))) (LOCAL (IN-THEORY (ENABLE STR::STRSUBST))) (DEFTHM STR::STRINGP-OF-STRSUBST (STRINGP (STR::STRSUBST STR::OLD STR::NEW X)) :RULE-CLASSES :TYPE-PRESCRIPTION) (LOCAL (ASSERT! (EQUAL (STR::STRSUBST "World" "Star" "Hello, World!") "Hello, Star!"))) (LOCAL (ASSERT! (EQUAL (STR::STRSUBST "oo" "aa" "xoooyoo") "xaaoyaa"))))) (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (DEFUND STR::STRSUBST (STR::OLD STR::NEW X) (DECLARE (XARGS :GUARD (AND (STRINGP STR::OLD) (STRINGP STR::NEW) (STRINGP X)))) (LET ((STR::OLDL (MBE :LOGIC (LEN (EXPLODE STR::OLD)) :EXEC (LENGTH STR::OLD)))) (IF (ZP STR::OLDL) (MBE :LOGIC (STR::STR-FIX X) :EXEC X) (STR::RCHARS-TO-STRING (STR::STRSUBST-AUX STR::OLD STR::NEW X 0 (LENGTH X) STR::OLDL NIL))))) (LOCAL (IN-THEORY (ENABLE STR::STRSUBST))) (DEFTHM STR::STRINGP-OF-STRSUBST (STRINGP (STR::STRSUBST STR::OLD STR::NEW X)) :RULE-CLASSES :TYPE-PRESCRIPTION) (RECORD-EXPANSION (LOCAL (ASSERT! (EQUAL (STR::STRSUBST "World" "Star" "Hello, World!") "Hello, Star!"))) (LOCAL (VALUE-TRIPLE :ELIDED))) (RECORD-EXPANSION (LOCAL (ASSERT! (EQUAL (STR::STRSUBST "oo" "aa" "xoooyoo") "xaaoyaa"))) (LOCAL (VALUE-TRIPLE :ELIDED)))))) (RECORD-EXPANSION (MAKE-EVENT (LET* ((XDOC::NAME (QUOTE STR::STRSUBST)) (XDOC::PARENTS (QUOTE (STR::SUBSTITUTION SUBSTITUTE))) (XDOC::SHORT (QUOTE "Replace substrings throughout a string.")) (XDOC::EXTENSION (QUOTE NIL)) (XDOC::WRLD (W STATE)) (XDOC::TRIPS (REVERSED-WORLD-SINCE-EVENT XDOC::WRLD (QUOTE (TABLE INTRO-TABLE :MARK (QUOTE STR::STRSUBST))) 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 strsubst) replaces each occurrence of @('old') with @('new')
throughout @('x').  Each argument is a string, and a new string is returned.
The replacement is done globally and non-recursively.</p>

<p>Examples:</p>
@({
 (strsubst \"World\" \"Star\" \"Hello, World!\")
   -->
 \"Hello, Star!\"

 (strsubst \"oo\" \"aa\" \"xoooyoo\")
   -->
 \"xaaoyaa\"
})

<p>ACL2 has a built in @(see substitute) function, but it only works on
individual characters, whereas @('strsubst') works on substrings.</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::STRSUBST) (:BASE-PKG . STR::ACL2-PKG-WITNESS) (:PARENTS STR::SUBSTITUTION SUBSTITUTE) (:SHORT . "Replace substrings throughout a string.") (:LONG . "<p>@(call strsubst) replaces each occurrence of @('old') with @('new')
throughout @('x').  Each argument is a string, and a new string is returned.
The replacement is done globally and non-recursively.</p>

<p>Examples:</p>
@({
 (strsubst \"World\" \"Star\" \"Hello, World!\")
   -->
 \"Hello, Star!\"

 (strsubst \"oo\" \"aa\" \"xoooyoo\")
   -->
 \"xaaoyaa\"
})

<p>ACL2 has a built in @(see substitute) function, but it only works on
individual characters, whereas @('strsubst') works on substrings.</p>

<h3>Definitions and Theorems</h3>@(def |STR|::|STRSUBST|)
@(def |STR|::|STRINGP-OF-STRSUBST|)") (:FROM . "[books]/str/strsubst.lisp"))) (XDOC::GET-XDOC-TABLE WORLD))) (VALUE-TRIPLE (QUOTE (DEFXDOC STR::STRSUBST)))))) (VALUE-TRIPLE (QUOTE STR::STRSUBST))))) (7 RECORD-EXPANSION (DEFSECTION STR::STRSUBST-LIST :PARENTS (STR::SUBSTITUTION) :SHORT "Carry out a @(see strsubst) replacement throughout a list of strings." :LONG "<p>@(call strsubst-list) replaces every occurrence of @('old') with
@('new') throughout @('x').  Here, @('old') and @('new') are strings, but
@('x') is a list of strings.  A new list of strings is returned.</p>

<p>Example:</p>
@({
 (strsubst-list \"Sun\"
                \"Moon\"
                '(\"Sun Roof\" \"Hello Sun\" \"Sunny Sunshades\"))
   -->
 (\"Moon Roof\" \"Hello Moon\" \"Moonny Moonshades\")
})" (DEFUND STR::STRSUBST-LIST (STR::OLD STR::NEW X) (DECLARE (XARGS :GUARD (AND (STRINGP STR::OLD) (STRINGP STR::NEW) (STRING-LISTP X)))) (IF (ATOM X) NIL (CONS (STR::STRSUBST STR::OLD STR::NEW (CAR X)) (STR::STRSUBST-LIST STR::OLD STR::NEW (CDR X))))) (LOCAL (IN-THEORY (ENABLE STR::STRSUBST-LIST))) (DEFTHM STR::STRSUBST-LIST-WHEN-ATOM (IMPLIES (ATOM X) (EQUAL (STR::STRSUBST-LIST STR::OLD STR::NEW X) NIL))) (DEFTHM STR::STRSUBST-LIST-OF-CONS (EQUAL (STR::STRSUBST-LIST STR::OLD STR::NEW (CONS A X)) (CONS (STR::STRSUBST STR::OLD STR::NEW A) (STR::STRSUBST-LIST STR::OLD STR::NEW X)))) (DEFTHM STR::STRING-LISTP-OF-STRSUBST-LIST (STRING-LISTP (STR::STRSUBST-LIST STR::OLD STR::NEW X))) (LOCAL (DEFTHM STR::L0 (EQUAL (STR::STRSUBST-LIST STR::OLD STR::NEW (LIST-FIX X)) (STR::STRSUBST-LIST STR::OLD STR::NEW X)))) (DEFCONG LIST-EQUIV EQUAL (STR::STRSUBST-LIST STR::OLD STR::NEW X) 3 :HINTS (("Goal" :IN-THEORY (DISABLE STR::L0) :USE ((:INSTANCE STR::L0 (X X)) (:INSTANCE STR::L0 (X X-EQUIV)))))) (DEFTHM STR::STRSUBST-LIST-OF-APPEND (EQUAL (STR::STRSUBST-LIST STR::OLD STR::NEW (APPEND X Y)) (APPEND (STR::STRSUBST-LIST STR::OLD STR::NEW X) (STR::STRSUBST-LIST STR::OLD STR::NEW Y)))) (DEFTHM STR::STRSUBST-LIST-OF-REVAPPEND (EQUAL (STR::STRSUBST-LIST STR::OLD STR::NEW (REVAPPEND X Y)) (REVAPPEND (STR::STRSUBST-LIST STR::OLD STR::NEW X) (STR::STRSUBST-LIST STR::OLD STR::NEW Y)))) (DEFTHM STR::STRSUBST-LIST-OF-REV (EQUAL (STR::STRSUBST-LIST STR::OLD STR::NEW (REV X)) (REV (STR::STRSUBST-LIST STR::OLD STR::NEW X))))) (WITH-OUTPUT :STACK :PUSH :OFF :ALL :ON ERROR (PROGN (TABLE INTRO-TABLE :MARK (QUOTE STR::STRSUBST-LIST)) (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (DEFUND STR::STRSUBST-LIST (STR::OLD STR::NEW X) (DECLARE (XARGS :GUARD (AND (STRINGP STR::OLD) (STRINGP STR::NEW) (STRING-LISTP X)))) (IF (ATOM X) NIL (CONS (STR::STRSUBST STR::OLD STR::NEW (CAR X)) (STR::STRSUBST-LIST STR::OLD STR::NEW (CDR X))))) (LOCAL (IN-THEORY (ENABLE STR::STRSUBST-LIST))) (DEFTHM STR::STRSUBST-LIST-WHEN-ATOM (IMPLIES (ATOM X) (EQUAL (STR::STRSUBST-LIST STR::OLD STR::NEW X) NIL))) (DEFTHM STR::STRSUBST-LIST-OF-CONS (EQUAL (STR::STRSUBST-LIST STR::OLD STR::NEW (CONS A X)) (CONS (STR::STRSUBST STR::OLD STR::NEW A) (STR::STRSUBST-LIST STR::OLD STR::NEW X)))) (DEFTHM STR::STRING-LISTP-OF-STRSUBST-LIST (STRING-LISTP (STR::STRSUBST-LIST STR::OLD STR::NEW X))) (LOCAL (DEFTHM STR::L0 (EQUAL (STR::STRSUBST-LIST STR::OLD STR::NEW (LIST-FIX X)) (STR::STRSUBST-LIST STR::OLD STR::NEW X)))) (DEFCONG LIST-EQUIV EQUAL (STR::STRSUBST-LIST STR::OLD STR::NEW X) 3 :HINTS (("Goal" :IN-THEORY (DISABLE STR::L0) :USE ((:INSTANCE STR::L0 (X X)) (:INSTANCE STR::L0 (X X-EQUIV)))))) (DEFTHM STR::STRSUBST-LIST-OF-APPEND (EQUAL (STR::STRSUBST-LIST STR::OLD STR::NEW (APPEND X Y)) (APPEND (STR::STRSUBST-LIST STR::OLD STR::NEW X) (STR::STRSUBST-LIST STR::OLD STR::NEW Y)))) (DEFTHM STR::STRSUBST-LIST-OF-REVAPPEND (EQUAL (STR::STRSUBST-LIST STR::OLD STR::NEW (REVAPPEND X Y)) (REVAPPEND (STR::STRSUBST-LIST STR::OLD STR::NEW X) (STR::STRSUBST-LIST STR::OLD STR::NEW Y)))) (DEFTHM STR::STRSUBST-LIST-OF-REV (EQUAL (STR::STRSUBST-LIST STR::OLD STR::NEW (REV X)) (REV (STR::STRSUBST-LIST STR::OLD STR::NEW X)))))) (RECORD-EXPANSION (MAKE-EVENT (LET* ((XDOC::NAME (QUOTE STR::STRSUBST-LIST)) (XDOC::PARENTS (QUOTE (STR::SUBSTITUTION))) (XDOC::SHORT (QUOTE "Carry out a @(see strsubst) replacement throughout a list of strings.")) (XDOC::EXTENSION (QUOTE NIL)) (XDOC::WRLD (W STATE)) (XDOC::TRIPS (REVERSED-WORLD-SINCE-EVENT XDOC::WRLD (QUOTE (TABLE INTRO-TABLE :MARK (QUOTE STR::STRSUBST-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 "<p>@(call strsubst-list) replaces every occurrence of @('old') with
@('new') throughout @('x').  Here, @('old') and @('new') are strings, but
@('x') is a list of strings.  A new list of strings is returned.</p>

<p>Example:</p>
@({
 (strsubst-list \"Sun\"
                \"Moon\"
                '(\"Sun Roof\" \"Hello Sun\" \"Sunny Sunshades\"))
   -->
 (\"Moon Roof\" \"Hello Moon\" \"Moonny Moonshades\")
})") (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::STRSUBST-LIST) (:BASE-PKG . STR::ACL2-PKG-WITNESS) (:PARENTS STR::SUBSTITUTION) (:SHORT . "Carry out a @(see strsubst) replacement throughout a list of strings.") (:LONG . "<p>@(call strsubst-list) replaces every occurrence of @('old') with
@('new') throughout @('x').  Here, @('old') and @('new') are strings, but
@('x') is a list of strings.  A new list of strings is returned.</p>

<p>Example:</p>
@({
 (strsubst-list \"Sun\"
                \"Moon\"
                '(\"Sun Roof\" \"Hello Sun\" \"Sunny Sunshades\"))
   -->
 (\"Moon Roof\" \"Hello Moon\" \"Moonny Moonshades\")
})

<h3>Definitions and Theorems</h3>@(def |STR|::|STRSUBST-LIST|)
@(def |STR|::|STRSUBST-LIST-WHEN-ATOM|)
@(def |STR|::|STRSUBST-LIST-OF-CONS|)
@(def |STR|::|STRING-LISTP-OF-STRSUBST-LIST|)
@(def |ACL2|::|LIST-EQUIV-IMPLIES-EQUAL-STRSUBST-LIST-3|)
@(def |STR|::|STRSUBST-LIST-OF-APPEND|)
@(def |STR|::|STRSUBST-LIST-OF-REVAPPEND|)
@(def |STR|::|STRSUBST-LIST-OF-REV|)") (:FROM . "[books]/str/strsubst.lisp"))) (XDOC::GET-XDOC-TABLE WORLD))) (VALUE-TRIPLE (QUOTE (DEFXDOC STR::STRSUBST-LIST)))))) (VALUE-TRIPLE (QUOTE STR::STRSUBST-LIST))))))
(("/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/strsubst.lisp" "strsubst" "strsubst" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1100185597) (LOCAL ("/usr/share/acl2-6.3/books/misc/assert.lisp" "misc/assert" "assert" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1184956729)) (LOCAL ("/usr/share/acl2-6.3/books/misc/eval.lisp" "eval" "eval" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1069973718)) ("/usr/share/acl2-6.3/books/str/strprefixp.lisp" "strprefixp" "strprefixp" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 2141614236) ("/usr/share/acl2-6.3/books/std/lists/prefixp.lisp" "std/lists/prefixp" "prefixp" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 689235789) ("/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)) ("/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))
1805227428
acl2-books-certs 6.3-5 / usr / share / acl2-6.3 / books / str / strsubst.cert
