/usr/share/acl2-6.3/books/str/coerce.cert is in acl2-books-certs 6.3-5.
This file is owned by root:root, with mode 0o644.
The actual contents of the file can be viewed below.
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 | (IN-PACKAGE "ACL2")
"ACL2 Version 6.3"
:BEGIN-PORTCULLIS-CMDS
(INCLUDE-BOOK "cutil/portcullis" :DIR :SYSTEM)
:END-PORTCULLIS-CMDS
:EXPANSION-ALIST
((2 RECORD-EXPANSION (DEFSECTION STR::STR/COERCE :PARENTS (STR::COERCION COERCE) :SHORT "Lemmas about @(see coerce) available in the @(see str) library." :LONG "<p>We typically do not want to ever reason about coerce. Instead, we
rewrite it away into @(see explode) or @(see implode).</p>" (LOCAL (DEFTHM STR::COERCE-STRING-LEMMA (IMPLIES (AND (CHARACTER-LISTP X) (CHARACTER-LISTP Y) (NOT (EQUAL X Y))) (NOT (EQUAL (COERCE X (QUOTE STRING)) (COERCE Y (QUOTE STRING))))) :HINTS (("Goal" :USE ((:INSTANCE COERCE-INVERSE-1 (X X)) (:INSTANCE COERCE-INVERSE-1 (X Y))))))) (DEFTHM STR::EQUAL-OF-COERCE-STRINGS (IMPLIES (AND (CHARACTER-LISTP X) (CHARACTER-LISTP Y)) (EQUAL (EQUAL (COERCE X (QUOTE STRING)) (COERCE Y (QUOTE STRING))) (EQUAL X Y)))) (LOCAL (DEFTHM STR::COERCE-LIST-LEMMA (IMPLIES (AND (STRINGP X) (STRINGP Y) (NOT (EQUAL X Y))) (NOT (EQUAL (COERCE X (QUOTE LIST)) (COERCE Y (QUOTE LIST))))) :HINTS (("Goal" :USE ((:INSTANCE COERCE-INVERSE-2 (X X)) (:INSTANCE COERCE-INVERSE-2 (X Y))))))) (DEFTHM STR::EQUAL-OF-COERCE-LISTS (IMPLIES (AND (STRINGP X) (STRINGP Y)) (EQUAL (EQUAL (COERCE X (QUOTE LIST)) (COERCE Y (QUOTE LIST))) (EQUAL X Y)))) (DEFTHM STR::COERCE-LIST-UNDER-IFF (IFF (COERCE STRING (QUOTE LIST)) (AND (STRINGP STRING) (NOT (EQUAL "" STRING)))) :HINTS (("Goal" :IN-THEORY (DISABLE STR::EQUAL-OF-COERCE-LISTS) :USE ((:INSTANCE STR::EQUAL-OF-COERCE-LISTS (X STRING) (Y "")))))) (DEFTHM STR::LENGTH-OF-COERCE (EQUAL (LENGTH (COERCE X Y)) (COND ((EQUAL Y (QUOTE LIST)) (IF (STRINGP X) (LENGTH X) 0)) (T (IF (STRINGP X) 0 (LEN X))))) :HINTS (("Goal" :USE ((:INSTANCE COMPLETION-OF-COERCE (X X) (Y Y)))))) (DEFTHM STR::LEN-OF-COERCE-TO-STRING (EQUAL (LEN (COERCE X (QUOTE STRING))) 0)) (DEFTHM STR::COERCE-INVERSE-1-BETTER (EQUAL (COERCE (COERCE X (QUOTE STRING)) (QUOTE LIST)) (IF (STRINGP X) NIL (MAKE-CHARACTER-LIST X))) :HINTS (("Goal" :USE ((:INSTANCE COMPLETION-OF-COERCE (X X) (Y (QUOTE STRING))))))) (DEFTHM STR::COERCE-INVERSE-2-BETTER (EQUAL (COERCE (COERCE X (QUOTE LIST)) (QUOTE STRING)) (IF (STRINGP X) X ""))) (IN-THEORY (DISABLE COERCE-INVERSE-1 COERCE-INVERSE-2)) (DEFTHM STR::COERCE-TO-LIST-OF-MAKE-CHARACTER-LIST (EQUAL (COERCE (MAKE-CHARACTER-LIST X) (QUOTE STRING)) (COERCE X (QUOTE STRING))) :HINTS (("Goal" :USE ((:INSTANCE COMPLETION-OF-COERCE (X X) (Y (QUOTE STRING)))))))) (WITH-OUTPUT :STACK :PUSH :OFF :ALL :ON ERROR (PROGN (TABLE INTRO-TABLE :MARK (QUOTE STR::STR/COERCE)) (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (LOCAL (DEFTHM STR::COERCE-STRING-LEMMA (IMPLIES (AND (CHARACTER-LISTP X) (CHARACTER-LISTP Y) (NOT (EQUAL X Y))) (NOT (EQUAL (COERCE X (QUOTE STRING)) (COERCE Y (QUOTE STRING))))) :HINTS (("Goal" :USE ((:INSTANCE COERCE-INVERSE-1 (X X)) (:INSTANCE COERCE-INVERSE-1 (X Y))))))) (DEFTHM STR::EQUAL-OF-COERCE-STRINGS (IMPLIES (AND (CHARACTER-LISTP X) (CHARACTER-LISTP Y)) (EQUAL (EQUAL (COERCE X (QUOTE STRING)) (COERCE Y (QUOTE STRING))) (EQUAL X Y)))) (LOCAL (DEFTHM STR::COERCE-LIST-LEMMA (IMPLIES (AND (STRINGP X) (STRINGP Y) (NOT (EQUAL X Y))) (NOT (EQUAL (COERCE X (QUOTE LIST)) (COERCE Y (QUOTE LIST))))) :HINTS (("Goal" :USE ((:INSTANCE COERCE-INVERSE-2 (X X)) (:INSTANCE COERCE-INVERSE-2 (X Y))))))) (DEFTHM STR::EQUAL-OF-COERCE-LISTS (IMPLIES (AND (STRINGP X) (STRINGP Y)) (EQUAL (EQUAL (COERCE X (QUOTE LIST)) (COERCE Y (QUOTE LIST))) (EQUAL X Y)))) (DEFTHM STR::COERCE-LIST-UNDER-IFF (IFF (COERCE STRING (QUOTE LIST)) (AND (STRINGP STRING) (NOT (EQUAL "" STRING)))) :HINTS (("Goal" :IN-THEORY (DISABLE STR::EQUAL-OF-COERCE-LISTS) :USE ((:INSTANCE STR::EQUAL-OF-COERCE-LISTS (X STRING) (Y "")))))) (DEFTHM STR::LENGTH-OF-COERCE (EQUAL (LENGTH (COERCE X Y)) (COND ((EQUAL Y (QUOTE LIST)) (IF (STRINGP X) (LENGTH X) 0)) (T (IF (STRINGP X) 0 (LEN X))))) :HINTS (("Goal" :USE ((:INSTANCE COMPLETION-OF-COERCE (X X) (Y Y)))))) (DEFTHM STR::LEN-OF-COERCE-TO-STRING (EQUAL (LEN (COERCE X (QUOTE STRING))) 0)) (DEFTHM STR::COERCE-INVERSE-1-BETTER (EQUAL (COERCE (COERCE X (QUOTE STRING)) (QUOTE LIST)) (IF (STRINGP X) NIL (MAKE-CHARACTER-LIST X))) :HINTS (("Goal" :USE ((:INSTANCE COMPLETION-OF-COERCE (X X) (Y (QUOTE STRING))))))) (DEFTHM STR::COERCE-INVERSE-2-BETTER (EQUAL (COERCE (COERCE X (QUOTE LIST)) (QUOTE STRING)) (IF (STRINGP X) X ""))) (IN-THEORY (DISABLE COERCE-INVERSE-1 COERCE-INVERSE-2)) (DEFTHM STR::COERCE-TO-LIST-OF-MAKE-CHARACTER-LIST (EQUAL (COERCE (MAKE-CHARACTER-LIST X) (QUOTE STRING)) (COERCE X (QUOTE STRING))) :HINTS (("Goal" :USE ((:INSTANCE COMPLETION-OF-COERCE (X X) (Y (QUOTE STRING))))))))) (RECORD-EXPANSION (MAKE-EVENT (LET* ((XDOC::NAME (QUOTE STR::STR/COERCE)) (XDOC::PARENTS (QUOTE (STR::COERCION COERCE))) (XDOC::SHORT (QUOTE "Lemmas about @(see coerce) available in the @(see str) library.")) (XDOC::EXTENSION (QUOTE NIL)) (XDOC::WRLD (W STATE)) (XDOC::TRIPS (REVERSED-WORLD-SINCE-EVENT XDOC::WRLD (QUOTE (TABLE INTRO-TABLE :MARK (QUOTE STR::STR/COERCE))) 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>We typically do not want to ever reason about coerce. Instead, we
rewrite it away into @(see explode) or @(see implode).</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::STR/COERCE) (:BASE-PKG . STR::ACL2-PKG-WITNESS) (:PARENTS STR::COERCION COERCE) (:SHORT . "Lemmas about @(see coerce) available in the @(see str) library.") (:LONG . "<p>We typically do not want to ever reason about coerce. Instead, we
rewrite it away into @(see explode) or @(see implode).</p>
<h3>Definitions and Theorems</h3>@(def |STR|::|EQUAL-OF-COERCE-STRINGS|)
@(def |STR|::|EQUAL-OF-COERCE-LISTS|)
@(def |STR|::|COERCE-LIST-UNDER-IFF|)
@(def |STR|::|LENGTH-OF-COERCE|)
@(def |STR|::|LEN-OF-COERCE-TO-STRING|)
@(def |STR|::|COERCE-INVERSE-1-BETTER|)
@(def |STR|::|COERCE-INVERSE-2-BETTER|)
@(def |STR|::|COERCE-TO-LIST-OF-MAKE-CHARACTER-LIST|)") (:FROM . "[books]/str/coerce.lisp"))) (XDOC::GET-XDOC-TABLE WORLD))) (VALUE-TRIPLE (QUOTE (DEFXDOC STR::STR/COERCE)))))) (VALUE-TRIPLE (QUOTE STR::STR/COERCE))))) (3 RECORD-EXPANSION (DEFSECTION EXPLODE :PARENTS (STR::COERCION COERCE) :SHORT "Convert a string to a character list." :LONG "<p>@(call explode) is logically nothing more than @('(coerce x
'list)').</p>
<p>Even though @(see coerce) is built into ACL2, we prefer to use @('explode') as
our normal form. We rewrite all uses of @('(coerce x 'list)') into
@('(str::explode x')') with the following rule:</p>
@(def coerce-to-list-removal)
<p>The basic rationale for this is that @('coerce')'s extra @(''list') argument
means we can't write, e.g., congruence relations about @('(coerce x 'list)'),
whereas this is no problem for @('(explode x)').</p>
<p>We do the same thing for @('(coerce x 'string)') — see @(see
implode).</p>
<p><b>BOZO</b> consider using misc/fast-coerce here.</p>" (DEFINLINED EXPLODE (X) (DECLARE (TYPE STRING X)) (COERCE X (QUOTE LIST))) (IN-THEORY (DISABLE (:T EXPLODE))) (LOCAL (IN-THEORY (ENABLE EXPLODE))) (DEFTHM STR::TRUE-LISTP-OF-EXPLODE (TRUE-LISTP (EXPLODE X)) :RULE-CLASSES :TYPE-PRESCRIPTION) (DEFTHM STR::CHARACTER-LISTP-OF-EXPLODE (CHARACTER-LISTP (EXPLODE X))) (DEFTHM STR::EXPLODE-WHEN-NOT-STRINGP (IMPLIES (NOT (STRINGP X)) (EQUAL (EXPLODE X) NIL))) (DEFTHM STR::EQUAL-OF-EXPLODES (IMPLIES (AND (STRINGP X) (STRINGP Y)) (EQUAL (EQUAL (EXPLODE X) (EXPLODE Y)) (EQUAL X Y)))) (DEFTHM STR::EXPLODE-UNDER-IFF (IFF (EXPLODE STRING) (AND (STRINGP STRING) (NOT (EQUAL "" STRING))))) (LOCAL (DEFTHM STR::L0 (IMPLIES (TRUE-LISTP X) (IFF (CONSP X) X)))) (DEFTHM STR::CONSP-OF-EXPLODE (EQUAL (CONSP (EXPLODE STRING)) (AND (STRINGP STRING) (NOT (EQUAL "" STRING))))) (DEFTHM STR::COERCE-TO-LIST-REMOVAL (EQUAL (COERCE X (QUOTE LIST)) (EXPLODE X))) (LOCAL (IN-THEORY (DISABLE EXPLODE))) (THEORY-INVARIANT (INCOMPATIBLE (:DEFINITION EXPLODE$INLINE) (:REWRITE STR::COERCE-TO-LIST-REMOVAL)))) (WITH-OUTPUT :STACK :PUSH :OFF :ALL :ON ERROR (PROGN (TABLE INTRO-TABLE :MARK (QUOTE EXPLODE)) (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (DEFINLINED EXPLODE (X) (DECLARE (TYPE STRING X)) (COERCE X (QUOTE LIST))) (IN-THEORY (DISABLE (:T EXPLODE))) (LOCAL (IN-THEORY (ENABLE EXPLODE))) (DEFTHM STR::TRUE-LISTP-OF-EXPLODE (TRUE-LISTP (EXPLODE X)) :RULE-CLASSES :TYPE-PRESCRIPTION) (DEFTHM STR::CHARACTER-LISTP-OF-EXPLODE (CHARACTER-LISTP (EXPLODE X))) (DEFTHM STR::EXPLODE-WHEN-NOT-STRINGP (IMPLIES (NOT (STRINGP X)) (EQUAL (EXPLODE X) NIL))) (DEFTHM STR::EQUAL-OF-EXPLODES (IMPLIES (AND (STRINGP X) (STRINGP Y)) (EQUAL (EQUAL (EXPLODE X) (EXPLODE Y)) (EQUAL X Y)))) (DEFTHM STR::EXPLODE-UNDER-IFF (IFF (EXPLODE STRING) (AND (STRINGP STRING) (NOT (EQUAL "" STRING))))) (LOCAL (DEFTHM STR::L0 (IMPLIES (TRUE-LISTP X) (IFF (CONSP X) X)))) (DEFTHM STR::CONSP-OF-EXPLODE (EQUAL (CONSP (EXPLODE STRING)) (AND (STRINGP STRING) (NOT (EQUAL "" STRING))))) (DEFTHM STR::COERCE-TO-LIST-REMOVAL (EQUAL (COERCE X (QUOTE LIST)) (EXPLODE X))) (LOCAL (IN-THEORY (DISABLE EXPLODE))) (THEORY-INVARIANT (INCOMPATIBLE (:DEFINITION EXPLODE$INLINE) (:REWRITE STR::COERCE-TO-LIST-REMOVAL))))) (RECORD-EXPANSION (MAKE-EVENT (LET* ((XDOC::NAME (QUOTE EXPLODE)) (XDOC::PARENTS (QUOTE (STR::COERCION COERCE))) (XDOC::SHORT (QUOTE "Convert a string to 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 EXPLODE))) 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 explode) is logically nothing more than @('(coerce x
'list)').</p>
<p>Even though @(see coerce) is built into ACL2, we prefer to use @('explode') as
our normal form. We rewrite all uses of @('(coerce x 'list)') into
@('(str::explode x')') with the following rule:</p>
@(def coerce-to-list-removal)
<p>The basic rationale for this is that @('coerce')'s extra @(''list') argument
means we can't write, e.g., congruence relations about @('(coerce x 'list)'),
whereas this is no problem for @('(explode x)').</p>
<p>We do the same thing for @('(coerce x 'string)') — see @(see
implode).</p>
<p><b>BOZO</b> consider using misc/fast-coerce here.</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 . EXPLODE) (:BASE-PKG . STR::ACL2-PKG-WITNESS) (:PARENTS STR::COERCION COERCE) (:SHORT . "Convert a string to a character list.") (:LONG . "<p>@(call explode) is logically nothing more than @('(coerce x
'list)').</p>
<p>Even though @(see coerce) is built into ACL2, we prefer to use @('explode') as
our normal form. We rewrite all uses of @('(coerce x 'list)') into
@('(str::explode x')') with the following rule:</p>
@(def coerce-to-list-removal)
<p>The basic rationale for this is that @('coerce')'s extra @(''list') argument
means we can't write, e.g., congruence relations about @('(coerce x 'list)'),
whereas this is no problem for @('(explode x)').</p>
<p>We do the same thing for @('(coerce x 'string)') — see @(see
implode).</p>
<p><b>BOZO</b> consider using misc/fast-coerce here.</p>
<h3>Definitions and Theorems</h3>@(def |ACL2|::|EXPLODE$INLINE|)
@(def |STR|::|TRUE-LISTP-OF-EXPLODE|)
@(def |STR|::|CHARACTER-LISTP-OF-EXPLODE|)
@(def |STR|::|EXPLODE-WHEN-NOT-STRINGP|)
@(def |STR|::|EQUAL-OF-EXPLODES|)
@(def |STR|::|EXPLODE-UNDER-IFF|)
@(def |STR|::|CONSP-OF-EXPLODE|)
@(def |STR|::|COERCE-TO-LIST-REMOVAL|)") (:FROM . "[books]/str/coerce.lisp"))) (XDOC::GET-XDOC-TABLE WORLD))) (VALUE-TRIPLE (QUOTE (DEFXDOC EXPLODE)))))) (VALUE-TRIPLE (QUOTE EXPLODE))))) (4 RECORD-EXPANSION (DEFSECTION IMPLODE :PARENTS (STR::COERCION COERCE) :SHORT "Convert a character list into a string." :LONG "<p>@(call implode) is logically nothing more than @('(coerce x
'string)').</p>
<p>Even though @(see coerce) is built into ACL2, we prefer to use @('implode')
as our normal form. We rewrite all uses of @('(coerce x 'string)') into
@('(str::implode x')') with the following rule:</p>
@(def coerce-to-string-removal)
<p>The basic rationale for this is that @('coerce')'s extra @(''string')
argument means we can't write, e.g., congruence relations about @('(coerce x
'string)'), whereas this is no problem for @('(implode x)').</p>
<p>We do the same thing for @('(coerce x 'list)') — see @(see
explode).</p>" (DEFINLINED IMPLODE (X) (DECLARE (XARGS :GUARD (CHARACTER-LISTP X))) (COERCE X (QUOTE STRING))) (IN-THEORY (DISABLE (:T IMPLODE))) (LOCAL (IN-THEORY (ENABLE IMPLODE))) (DEFTHM STR::STRINGP-OF-IMPLODE (STRINGP (IMPLODE X)) :RULE-CLASSES :TYPE-PRESCRIPTION) (DEFTHM STR::EQUAL-OF-IMPLODES (IMPLIES (AND (CHARACTER-LISTP X) (CHARACTER-LISTP Y)) (EQUAL (EQUAL (IMPLODE X) (IMPLODE Y)) (EQUAL X Y)))) (DEFTHM STR::IMPLODE-OF-MAKE-CHARACTER-LIST (EQUAL (IMPLODE (MAKE-CHARACTER-LIST X)) (IMPLODE X))) (LOCAL (DEFTHM STR::L0 (EQUAL (EQUAL (LEN X) 0) (ATOM X)))) (DEFTHM STR::EQUAL-OF-IMPLODE-WITH-EMPTY-STRING (EQUAL (EQUAL "" (IMPLODE X)) (ATOM X)) :HINTS (("Goal" :IN-THEORY (DISABLE STR::LENGTH-OF-COERCE) :USE ((:INSTANCE STR::LENGTH-OF-COERCE (X X) (Y (QUOTE STRING))))))) (DEFTHM STR::COERCE-TO-STRING-REMOVAL (EQUAL (COERCE X (QUOTE STRING)) (IMPLODE X))) (LOCAL (IN-THEORY (DISABLE IMPLODE$INLINE))) (THEORY-INVARIANT (INCOMPATIBLE (:DEFINITION IMPLODE$INLINE) (:REWRITE STR::COERCE-TO-STRING-REMOVAL)))) (WITH-OUTPUT :STACK :PUSH :OFF :ALL :ON ERROR (PROGN (TABLE INTRO-TABLE :MARK (QUOTE IMPLODE)) (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (DEFINLINED IMPLODE (X) (DECLARE (XARGS :GUARD (CHARACTER-LISTP X))) (COERCE X (QUOTE STRING))) (IN-THEORY (DISABLE (:T IMPLODE))) (LOCAL (IN-THEORY (ENABLE IMPLODE))) (DEFTHM STR::STRINGP-OF-IMPLODE (STRINGP (IMPLODE X)) :RULE-CLASSES :TYPE-PRESCRIPTION) (DEFTHM STR::EQUAL-OF-IMPLODES (IMPLIES (AND (CHARACTER-LISTP X) (CHARACTER-LISTP Y)) (EQUAL (EQUAL (IMPLODE X) (IMPLODE Y)) (EQUAL X Y)))) (DEFTHM STR::IMPLODE-OF-MAKE-CHARACTER-LIST (EQUAL (IMPLODE (MAKE-CHARACTER-LIST X)) (IMPLODE X))) (LOCAL (DEFTHM STR::L0 (EQUAL (EQUAL (LEN X) 0) (ATOM X)))) (DEFTHM STR::EQUAL-OF-IMPLODE-WITH-EMPTY-STRING (EQUAL (EQUAL "" (IMPLODE X)) (ATOM X)) :HINTS (("Goal" :IN-THEORY (DISABLE STR::LENGTH-OF-COERCE) :USE ((:INSTANCE STR::LENGTH-OF-COERCE (X X) (Y (QUOTE STRING))))))) (DEFTHM STR::COERCE-TO-STRING-REMOVAL (EQUAL (COERCE X (QUOTE STRING)) (IMPLODE X))) (LOCAL (IN-THEORY (DISABLE IMPLODE$INLINE))) (THEORY-INVARIANT (INCOMPATIBLE (:DEFINITION IMPLODE$INLINE) (:REWRITE STR::COERCE-TO-STRING-REMOVAL))))) (RECORD-EXPANSION (MAKE-EVENT (LET* ((XDOC::NAME (QUOTE IMPLODE)) (XDOC::PARENTS (QUOTE (STR::COERCION COERCE))) (XDOC::SHORT (QUOTE "Convert a character list into a string.")) (XDOC::EXTENSION (QUOTE NIL)) (XDOC::WRLD (W STATE)) (XDOC::TRIPS (REVERSED-WORLD-SINCE-EVENT XDOC::WRLD (QUOTE (TABLE INTRO-TABLE :MARK (QUOTE IMPLODE))) 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 implode) is logically nothing more than @('(coerce x
'string)').</p>
<p>Even though @(see coerce) is built into ACL2, we prefer to use @('implode')
as our normal form. We rewrite all uses of @('(coerce x 'string)') into
@('(str::implode x')') with the following rule:</p>
@(def coerce-to-string-removal)
<p>The basic rationale for this is that @('coerce')'s extra @(''string')
argument means we can't write, e.g., congruence relations about @('(coerce x
'string)'), whereas this is no problem for @('(implode x)').</p>
<p>We do the same thing for @('(coerce x 'list)') — see @(see
explode).</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 . IMPLODE) (:BASE-PKG . STR::ACL2-PKG-WITNESS) (:PARENTS STR::COERCION COERCE) (:SHORT . "Convert a character list into a string.") (:LONG . "<p>@(call implode) is logically nothing more than @('(coerce x
'string)').</p>
<p>Even though @(see coerce) is built into ACL2, we prefer to use @('implode')
as our normal form. We rewrite all uses of @('(coerce x 'string)') into
@('(str::implode x')') with the following rule:</p>
@(def coerce-to-string-removal)
<p>The basic rationale for this is that @('coerce')'s extra @(''string')
argument means we can't write, e.g., congruence relations about @('(coerce x
'string)'), whereas this is no problem for @('(implode x)').</p>
<p>We do the same thing for @('(coerce x 'list)') — see @(see
explode).</p>
<h3>Definitions and Theorems</h3>@(def |ACL2|::|IMPLODE$INLINE|)
@(def |STR|::|STRINGP-OF-IMPLODE|)
@(def |STR|::|EQUAL-OF-IMPLODES|)
@(def |STR|::|IMPLODE-OF-MAKE-CHARACTER-LIST|)
@(def |STR|::|EQUAL-OF-IMPLODE-WITH-EMPTY-STRING|)
@(def |STR|::|COERCE-TO-STRING-REMOVAL|)") (:FROM . "[books]/str/coerce.lisp"))) (XDOC::GET-XDOC-TABLE WORLD))) (VALUE-TRIPLE (QUOTE (DEFXDOC IMPLODE)))))) (VALUE-TRIPLE (QUOTE IMPLODE))))) (5 RECORD-EXPANSION (DEFSECTION STR::IMPLODE-EXPLODE-INVERSION :PARENTS (IMPLODE EXPLODE) :SHORT "Inversion theorems for @(see implode) and @(see explode)." (LOCAL (IN-THEORY (E/D (IMPLODE EXPLODE) (STR::COERCE-TO-STRING-REMOVAL STR::COERCE-TO-LIST-REMOVAL)))) (DEFTHM STR::EXPLODE-OF-IMPLODE (EQUAL (EXPLODE (IMPLODE X)) (IF (STRINGP X) NIL (MAKE-CHARACTER-LIST X)))) (DEFTHM STR::IMPLODE-OF-EXPLODE (EQUAL (IMPLODE (EXPLODE X)) (IF (STRINGP X) X "")))) (WITH-OUTPUT :STACK :PUSH :OFF :ALL :ON ERROR (PROGN (TABLE INTRO-TABLE :MARK (QUOTE STR::IMPLODE-EXPLODE-INVERSION)) (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (LOCAL (IN-THEORY (E/D (IMPLODE EXPLODE) (STR::COERCE-TO-STRING-REMOVAL STR::COERCE-TO-LIST-REMOVAL)))) (DEFTHM STR::EXPLODE-OF-IMPLODE (EQUAL (EXPLODE (IMPLODE X)) (IF (STRINGP X) NIL (MAKE-CHARACTER-LIST X)))) (DEFTHM STR::IMPLODE-OF-EXPLODE (EQUAL (IMPLODE (EXPLODE X)) (IF (STRINGP X) X ""))))) (RECORD-EXPANSION (MAKE-EVENT (LET* ((XDOC::NAME (QUOTE STR::IMPLODE-EXPLODE-INVERSION)) (XDOC::PARENTS (QUOTE (IMPLODE EXPLODE))) (XDOC::SHORT (QUOTE "Inversion theorems for @(see implode) and @(see explode).")) (XDOC::EXTENSION (QUOTE NIL)) (XDOC::WRLD (W STATE)) (XDOC::TRIPS (REVERSED-WORLD-SINCE-EVENT XDOC::WRLD (QUOTE (TABLE INTRO-TABLE :MARK (QUOTE STR::IMPLODE-EXPLODE-INVERSION))) 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::IMPLODE-EXPLODE-INVERSION) (:BASE-PKG . STR::ACL2-PKG-WITNESS) (:PARENTS IMPLODE EXPLODE) (:SHORT . "Inversion theorems for @(see implode) and @(see explode).") (:LONG . "
<h3>Definitions and Theorems</h3>@(def |STR|::|EXPLODE-OF-IMPLODE|)
@(def |STR|::|IMPLODE-OF-EXPLODE|)") (:FROM . "[books]/str/coerce.lisp"))) (XDOC::GET-XDOC-TABLE WORLD))) (VALUE-TRIPLE (QUOTE (DEFXDOC STR::IMPLODE-EXPLODE-INVERSION)))))) (VALUE-TRIPLE (QUOTE STR::IMPLODE-EXPLODE-INVERSION))))))
(("/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/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)) (LOCAL ("/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))
903295566
|