acl2-books-certs 6.3-5 / usr / share / acl2-6.3 / books / str / char-fix.cert

(IN-PACKAGE "ACL2")
"ACL2 Version 6.3"
:BEGIN-PORTCULLIS-CMDS
(INCLUDE-BOOK "cutil/portcullis" :DIR :SYSTEM)
:END-PORTCULLIS-CMDS
:EXPANSION-ALIST
((3 RECORD-EXPANSION (DEFSECTION STR::CODE-CHAR-LEMMAS :PARENTS (CODE-CHAR) :SHORT "Lemmas about @(see code-char) from the @(see str) library." (DEFTHM STR::DEFAULT-CODE-CHAR (IMPLIES (OR (ZP X) (NOT (< X 256))) (EQUAL (CODE-CHAR X) (CODE-CHAR 0))) :HINTS (("Goal" :USE ((:INSTANCE COMPLETION-OF-CODE-CHAR))))) (LOCAL (DEFTHM STR::L0 (IMPLIES (NOT (OR (ZP X) (NOT (< X 256)))) (NOT (EQUAL (CODE-CHAR X) (CODE-CHAR 0)))) :HINTS (("Goal" :USE ((:INSTANCE CHAR-CODE-CODE-CHAR-IS-IDENTITY (N X))))))) (LOCAL (DEFTHM STR::L1 (EQUAL (EQUAL (CODE-CHAR X) (CODE-CHAR 0)) (OR (ZP X) (NOT (< X 256)))))) (LOCAL (DEFTHM STR::L2 (IMPLIES (AND (NATP N) (NATP M) (< N 256) (< M 256)) (EQUAL (EQUAL (CODE-CHAR N) (CODE-CHAR M)) (EQUAL N M))) :HINTS (("Goal" :IN-THEORY (DISABLE CHAR-CODE-CODE-CHAR-IS-IDENTITY) :USE ((:INSTANCE CHAR-CODE-CODE-CHAR-IS-IDENTITY (N N)) (:INSTANCE CHAR-CODE-CODE-CHAR-IS-IDENTITY (N M))))))) (DEFTHM STR::EQUAL-OF-CODE-CHAR-AND-CODE-CHAR (EQUAL (EQUAL (CODE-CHAR X) (CODE-CHAR Y)) (LET ((STR::ZERO-X (OR (ZP X) (>= X 256))) (STR::ZERO-Y (OR (ZP Y) (>= Y 256)))) (IF STR::ZERO-X STR::ZERO-Y (EQUAL X Y)))) :HINTS (("Goal" :IN-THEORY (DISABLE STR::L2) :USE ((:INSTANCE STR::L2 (N X) (M Y)))))) (DEFTHM STR::EQUAL-OF-CODE-CODE-AND-CONSTANT (IMPLIES (SYNTAXP (QUOTEP C)) (EQUAL (EQUAL (CODE-CHAR X) C) (AND (CHARACTERP C) (IF (EQUAL C (CODE-CHAR 0)) (OR (ZP X) (NOT (< X 256))) (EQUAL X (CHAR-CODE C)))))) :HINTS (("goal" :USE ((:INSTANCE COMPLETION-OF-CODE-CHAR)))))) (WITH-OUTPUT :STACK :PUSH :OFF :ALL :ON ERROR (PROGN (TABLE INTRO-TABLE :MARK (QUOTE STR::CODE-CHAR-LEMMAS)) (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (DEFTHM STR::DEFAULT-CODE-CHAR (IMPLIES (OR (ZP X) (NOT (< X 256))) (EQUAL (CODE-CHAR X) (CODE-CHAR 0))) :HINTS (("Goal" :USE ((:INSTANCE COMPLETION-OF-CODE-CHAR))))) (LOCAL (DEFTHM STR::L0 (IMPLIES (NOT (OR (ZP X) (NOT (< X 256)))) (NOT (EQUAL (CODE-CHAR X) (CODE-CHAR 0)))) :HINTS (("Goal" :USE ((:INSTANCE CHAR-CODE-CODE-CHAR-IS-IDENTITY (N X))))))) (LOCAL (DEFTHM STR::L1 (EQUAL (EQUAL (CODE-CHAR X) (CODE-CHAR 0)) (OR (ZP X) (NOT (< X 256)))))) (LOCAL (DEFTHM STR::L2 (IMPLIES (AND (NATP N) (NATP M) (< N 256) (< M 256)) (EQUAL (EQUAL (CODE-CHAR N) (CODE-CHAR M)) (EQUAL N M))) :HINTS (("Goal" :IN-THEORY (DISABLE CHAR-CODE-CODE-CHAR-IS-IDENTITY) :USE ((:INSTANCE CHAR-CODE-CODE-CHAR-IS-IDENTITY (N N)) (:INSTANCE CHAR-CODE-CODE-CHAR-IS-IDENTITY (N M))))))) (DEFTHM STR::EQUAL-OF-CODE-CHAR-AND-CODE-CHAR (EQUAL (EQUAL (CODE-CHAR X) (CODE-CHAR Y)) (LET ((STR::ZERO-X (OR (ZP X) (>= X 256))) (STR::ZERO-Y (OR (ZP Y) (>= Y 256)))) (IF STR::ZERO-X STR::ZERO-Y (EQUAL X Y)))) :HINTS (("Goal" :IN-THEORY (DISABLE STR::L2) :USE ((:INSTANCE STR::L2 (N X) (M Y)))))) (DEFTHM STR::EQUAL-OF-CODE-CODE-AND-CONSTANT (IMPLIES (SYNTAXP (QUOTEP C)) (EQUAL (EQUAL (CODE-CHAR X) C) (AND (CHARACTERP C) (IF (EQUAL C (CODE-CHAR 0)) (OR (ZP X) (NOT (< X 256))) (EQUAL X (CHAR-CODE C)))))) :HINTS (("goal" :USE ((:INSTANCE COMPLETION-OF-CODE-CHAR))))))) (RECORD-EXPANSION (MAKE-EVENT (LET* ((XDOC::NAME (QUOTE STR::CODE-CHAR-LEMMAS)) (XDOC::PARENTS (QUOTE (CODE-CHAR))) (XDOC::SHORT (QUOTE "Lemmas about @(see code-char) from 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::CODE-CHAR-LEMMAS))) 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::CODE-CHAR-LEMMAS) (:BASE-PKG . STR::ACL2-PKG-WITNESS) (:PARENTS CODE-CHAR) (:SHORT . "Lemmas about @(see code-char) from the @(see str) library.") (:LONG . "

<h3>Definitions and Theorems</h3>@(def |STR|::|DEFAULT-CODE-CHAR|)
@(def |STR|::|EQUAL-OF-CODE-CHAR-AND-CODE-CHAR|)
@(def |STR|::|EQUAL-OF-CODE-CODE-AND-CONSTANT|)") (:FROM . "[books]/str/char-fix.lisp"))) (XDOC::GET-XDOC-TABLE WORLD))) (VALUE-TRIPLE (QUOTE (DEFXDOC STR::CODE-CHAR-LEMMAS)))))) (VALUE-TRIPLE (QUOTE STR::CODE-CHAR-LEMMAS))))) (4 RECORD-EXPANSION (DEFSECTION STR::CHAR-FIX :PARENTS (STR::EQUIVALENCES) :SHORT "Coerce to a character." :LONG "<p>@(call char-fix) is the identity on @(see acl2::characters), and
returns the NUL character (i.e., the character whose code is 0) for any
non-character.</p>

<p>This is similar to other fixing functions like @(see fix) and @(see nfix).
See also @(see chareqv).</p>" (DEFINLINED STR::CHAR-FIX (X) (DECLARE (XARGS :GUARD T)) (IF (CHARACTERP X) X (CODE-CHAR 0))) (LOCAL (IN-THEORY (ENABLE STR::CHAR-FIX))) (DEFTHM STR::CHAR-FIX-DEFAULT (IMPLIES (NOT (CHARACTERP X)) (EQUAL (STR::CHAR-FIX X) (CODE-CHAR 0)))) (DEFTHM STR::CHAR-FIX-WHEN-CHARACTERP (IMPLIES (CHARACTERP X) (EQUAL (STR::CHAR-FIX X) X)))) (WITH-OUTPUT :STACK :PUSH :OFF :ALL :ON ERROR (PROGN (TABLE INTRO-TABLE :MARK (QUOTE STR::CHAR-FIX)) (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (DEFINLINED STR::CHAR-FIX (X) (DECLARE (XARGS :GUARD T)) (IF (CHARACTERP X) X (CODE-CHAR 0))) (LOCAL (IN-THEORY (ENABLE STR::CHAR-FIX))) (DEFTHM STR::CHAR-FIX-DEFAULT (IMPLIES (NOT (CHARACTERP X)) (EQUAL (STR::CHAR-FIX X) (CODE-CHAR 0)))) (DEFTHM STR::CHAR-FIX-WHEN-CHARACTERP (IMPLIES (CHARACTERP X) (EQUAL (STR::CHAR-FIX X) X))))) (RECORD-EXPANSION (MAKE-EVENT (LET* ((XDOC::NAME (QUOTE STR::CHAR-FIX)) (XDOC::PARENTS (QUOTE (STR::EQUIVALENCES))) (XDOC::SHORT (QUOTE "Coerce to a character.")) (XDOC::EXTENSION (QUOTE NIL)) (XDOC::WRLD (W STATE)) (XDOC::TRIPS (REVERSED-WORLD-SINCE-EVENT XDOC::WRLD (QUOTE (TABLE INTRO-TABLE :MARK (QUOTE STR::CHAR-FIX))) 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 char-fix) is the identity on @(see acl2::characters), and
returns the NUL character (i.e., the character whose code is 0) for any
non-character.</p>

<p>This is similar to other fixing functions like @(see fix) and @(see nfix).
See also @(see chareqv).</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::CHAR-FIX) (:BASE-PKG . STR::ACL2-PKG-WITNESS) (:PARENTS STR::EQUIVALENCES) (:SHORT . "Coerce to a character.") (:LONG . "<p>@(call char-fix) is the identity on @(see acl2::characters), and
returns the NUL character (i.e., the character whose code is 0) for any
non-character.</p>

<p>This is similar to other fixing functions like @(see fix) and @(see nfix).
See also @(see chareqv).</p>

<h3>Definitions and Theorems</h3>@(def |STR|::|CHAR-FIX$INLINE|)
@(def |STR|::|CHAR-FIX-DEFAULT|)
@(def |STR|::|CHAR-FIX-WHEN-CHARACTERP|)") (:FROM . "[books]/str/char-fix.lisp"))) (XDOC::GET-XDOC-TABLE WORLD))) (VALUE-TRIPLE (QUOTE (DEFXDOC STR::CHAR-FIX)))))) (VALUE-TRIPLE (QUOTE STR::CHAR-FIX))))) (5 RECORD-EXPANSION (DEFSECTION STR::CHAR-CODE-LEMMAS :PARENTS (CHAR-CODE) :SHORT "Lemmas about @(see char-code) from the @(see str) library." (DEFTHM STR::EQUAL-OF-CHAR-CODE-AND-CONSTANT (IMPLIES (SYNTAXP (QUOTEP C)) (EQUAL (EQUAL (CHAR-CODE X) C) (IF (CHARACTERP X) (AND (NATP C) (<= C 255) (EQUAL X (CODE-CHAR C))) (EQUAL C 0))))) (LOCAL (DEFTHM STR::L0 (IMPLIES (AND (CHARACTERP X) (CHARACTERP Y)) (EQUAL (EQUAL (CHAR-CODE X) (CHAR-CODE Y)) (EQUAL X Y))) :HINTS (("Goal" :USE EQUAL-CHAR-CODE)))) (DEFTHM STR::EQUAL-OF-CHAR-CODES (EQUAL (EQUAL (CHAR-CODE X) (CHAR-CODE Y)) (EQUAL (STR::CHAR-FIX X) (STR::CHAR-FIX Y))) :HINTS (("Goal" :IN-THEORY (ENABLE STR::CHAR-FIX))))) (WITH-OUTPUT :STACK :PUSH :OFF :ALL :ON ERROR (PROGN (TABLE INTRO-TABLE :MARK (QUOTE STR::CHAR-CODE-LEMMAS)) (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (DEFTHM STR::EQUAL-OF-CHAR-CODE-AND-CONSTANT (IMPLIES (SYNTAXP (QUOTEP C)) (EQUAL (EQUAL (CHAR-CODE X) C) (IF (CHARACTERP X) (AND (NATP C) (<= C 255) (EQUAL X (CODE-CHAR C))) (EQUAL C 0))))) (LOCAL (DEFTHM STR::L0 (IMPLIES (AND (CHARACTERP X) (CHARACTERP Y)) (EQUAL (EQUAL (CHAR-CODE X) (CHAR-CODE Y)) (EQUAL X Y))) :HINTS (("Goal" :USE EQUAL-CHAR-CODE)))) (DEFTHM STR::EQUAL-OF-CHAR-CODES (EQUAL (EQUAL (CHAR-CODE X) (CHAR-CODE Y)) (EQUAL (STR::CHAR-FIX X) (STR::CHAR-FIX Y))) :HINTS (("Goal" :IN-THEORY (ENABLE STR::CHAR-FIX)))))) (RECORD-EXPANSION (MAKE-EVENT (LET* ((XDOC::NAME (QUOTE STR::CHAR-CODE-LEMMAS)) (XDOC::PARENTS (QUOTE (CHAR-CODE))) (XDOC::SHORT (QUOTE "Lemmas about @(see char-code) from 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::CHAR-CODE-LEMMAS))) 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::CHAR-CODE-LEMMAS) (:BASE-PKG . STR::ACL2-PKG-WITNESS) (:PARENTS CHAR-CODE) (:SHORT . "Lemmas about @(see char-code) from the @(see str) library.") (:LONG . "

<h3>Definitions and Theorems</h3>@(def |STR|::|EQUAL-OF-CHAR-CODE-AND-CONSTANT|)
@(def |STR|::|EQUAL-OF-CHAR-CODES|)") (:FROM . "[books]/str/char-fix.lisp"))) (XDOC::GET-XDOC-TABLE WORLD))) (VALUE-TRIPLE (QUOTE (DEFXDOC STR::CHAR-CODE-LEMMAS)))))) (VALUE-TRIPLE (QUOTE STR::CHAR-CODE-LEMMAS))))))
(("/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/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))
1063973971