acl2-books-certs 6.3-5 / usr / share / acl2-6.3 / books / system / random.cert

(IN-PACKAGE "ACL2")
"ACL2 Version 6.3"
:BEGIN-PORTCULLIS-CMDS
(DEFPKG "XDOC" (SET-DIFFERENCE-EQ (UNION-EQ (UNION-EQ *ACL2-EXPORTS* *COMMON-LISP-SYMBOLS-FROM-MAIN-LISP-PACKAGE*) (QUOTE (B* QUIT EXIT VALUE DEFXDOC DEFXDOC-RAW MACRO-ARGS XDOC-EXTEND DEFSECTION DEFSECTION-PROGN CUTIL LNFIX SET-DEFAULT-PARENTS GETPROP FORMALS JUSTIFICATION DEF-BODIES CURRENT-ACL2-WORLD DEF-BODY ACCESS THEOREM UNTRANSLATED-THEOREM GUARD XDOC XDOC! UNQUOTE UNDOCUMENTED ASSERT! TOP EXPLODE IMPLODE))) (QUOTE NIL)) NIL ((:SYSTEM . "xdoc/portcullis.lisp") (:SYSTEM . "xdoc/top.lisp")) T)
:END-PORTCULLIS-CMDS
:EXPANSION-ALIST
((5 RECORD-EXPANSION (DEFSECTION RANDOM$-LEMMAS :PARENTS (RANDOM$) :SHORT "Lemmas about random$ available in the system/random book." (LOCAL (IN-THEORY (ENABLE RANDOM$))) (DEFTHM NATP-RANDOM$-BETTER (NATP (MV-NTH 0 (RANDOM$ LIMIT STATE))) :RULE-CLASSES :TYPE-PRESCRIPTION) (DEFTHM RANDOM$-LINEAR-BETTER (AND (<= 0 (MV-NTH 0 (RANDOM$ N STATE))) (IMPLIES (POSP N) (< (MV-NTH 0 (RANDOM$ N STATE)) N))) :HINTS (("Goal" :IN-THEORY (ENABLE MV-NTH) :USE ((:INSTANCE RANDOM$-LINEAR (N N)))))) (DEFTHM STATE-P1-OF-RANDOM (IMPLIES (FORCE (STATE-P1 STATE)) (STATE-P1 (MV-NTH 1 (RANDOM$ LIMIT STATE)))) :HINTS (("Goal" :IN-THEORY (ENABLE RANDOM$ READ-ACL2-ORACLE))))) (WITH-OUTPUT :STACK :PUSH :OFF :ALL :ON ERROR (PROGN (TABLE INTRO-TABLE :MARK (QUOTE RANDOM$-LEMMAS)) (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (LOCAL (IN-THEORY (ENABLE RANDOM$))) (DEFTHM NATP-RANDOM$-BETTER (NATP (MV-NTH 0 (RANDOM$ LIMIT STATE))) :RULE-CLASSES :TYPE-PRESCRIPTION) (DEFTHM RANDOM$-LINEAR-BETTER (AND (<= 0 (MV-NTH 0 (RANDOM$ N STATE))) (IMPLIES (POSP N) (< (MV-NTH 0 (RANDOM$ N STATE)) N))) :HINTS (("Goal" :IN-THEORY (ENABLE MV-NTH) :USE ((:INSTANCE RANDOM$-LINEAR (N N)))))) (DEFTHM STATE-P1-OF-RANDOM (IMPLIES (FORCE (STATE-P1 STATE)) (STATE-P1 (MV-NTH 1 (RANDOM$ LIMIT STATE)))) :HINTS (("Goal" :IN-THEORY (ENABLE RANDOM$ READ-ACL2-ORACLE)))))) (RECORD-EXPANSION (MAKE-EVENT (LET* ((XDOC::NAME (QUOTE RANDOM$-LEMMAS)) (XDOC::PARENTS (QUOTE (RANDOM$))) (XDOC::SHORT (QUOTE "Lemmas about random$ available in the system/random book.")) (XDOC::EXTENSION (QUOTE NIL)) (XDOC::WRLD (W STATE)) (XDOC::TRIPS (REVERSED-WORLD-SINCE-EVENT XDOC::WRLD (QUOTE (TABLE INTRO-TABLE :MARK (QUOTE RANDOM$-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 . RANDOM$-LEMMAS) (:BASE-PKG . ACL2-PKG-WITNESS) (:PARENTS RANDOM$) (:SHORT . "Lemmas about random$ available in the system/random book.") (:LONG . "

<h3>Definitions and Theorems</h3>@(def |ACL2|::|NATP-RANDOM$-BETTER|)
@(def |ACL2|::|RANDOM$-LINEAR-BETTER|)
@(def |ACL2|::|STATE-P1-OF-RANDOM|)") (:FROM . "[books]/system/random.lisp"))) (XDOC::GET-XDOC-TABLE WORLD))) (VALUE-TRIPLE (QUOTE (DEFXDOC RANDOM$-LEMMAS)))))) (VALUE-TRIPLE (QUOTE RANDOM$-LEMMAS))))) (6 RECORD-EXPANSION (DEFSECTION RANDOM-LIST-AUX :PARENTS (RANDOM$) :SHORT "Add random numbers onto an accumulator." (DEFUND RANDOM-LIST-AUX (N LIMIT ACC STATE) (DECLARE (XARGS :GUARD (AND (NATP N) (POSP LIMIT)))) (IF (ZP N) (MV ACC STATE) (B* (((MV X1 STATE) (RANDOM$ LIMIT STATE))) (RANDOM-LIST-AUX (- N 1) LIMIT (CONS X1 ACC) STATE)))) (LOCAL (IN-THEORY (ENABLE RANDOM-LIST-AUX))) (DEFTHM NAT-LISTP-OF-RANDOM-LIST-AUX (EQUAL (NAT-LISTP (MV-NTH 0 (RANDOM-LIST-AUX N LIMIT ACC STATE))) (NAT-LISTP ACC))) (DEFTHM STATE-P1-OF-RANDOM-LIST-AUX (IMPLIES (FORCE (STATE-P1 STATE)) (STATE-P1 (MV-NTH 1 (RANDOM-LIST-AUX N LIMIT ACC STATE)))))) (WITH-OUTPUT :STACK :PUSH :OFF :ALL :ON ERROR (PROGN (TABLE INTRO-TABLE :MARK (QUOTE RANDOM-LIST-AUX)) (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (DEFUND RANDOM-LIST-AUX (N LIMIT ACC STATE) (DECLARE (XARGS :GUARD (AND (NATP N) (POSP LIMIT)))) (IF (ZP N) (MV ACC STATE) (B* (((MV X1 STATE) (RANDOM$ LIMIT STATE))) (RANDOM-LIST-AUX (- N 1) LIMIT (CONS X1 ACC) STATE)))) (LOCAL (IN-THEORY (ENABLE RANDOM-LIST-AUX))) (DEFTHM NAT-LISTP-OF-RANDOM-LIST-AUX (EQUAL (NAT-LISTP (MV-NTH 0 (RANDOM-LIST-AUX N LIMIT ACC STATE))) (NAT-LISTP ACC))) (DEFTHM STATE-P1-OF-RANDOM-LIST-AUX (IMPLIES (FORCE (STATE-P1 STATE)) (STATE-P1 (MV-NTH 1 (RANDOM-LIST-AUX N LIMIT ACC STATE))))))) (RECORD-EXPANSION (MAKE-EVENT (LET* ((XDOC::NAME (QUOTE RANDOM-LIST-AUX)) (XDOC::PARENTS (QUOTE (RANDOM$))) (XDOC::SHORT (QUOTE "Add random numbers onto an accumulator.")) (XDOC::EXTENSION (QUOTE NIL)) (XDOC::WRLD (W STATE)) (XDOC::TRIPS (REVERSED-WORLD-SINCE-EVENT XDOC::WRLD (QUOTE (TABLE INTRO-TABLE :MARK (QUOTE RANDOM-LIST-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 . RANDOM-LIST-AUX) (:BASE-PKG . ACL2-PKG-WITNESS) (:PARENTS RANDOM$) (:SHORT . "Add random numbers onto an accumulator.") (:LONG . "

<h3>Definitions and Theorems</h3>@(def |ACL2|::|RANDOM-LIST-AUX|)
@(def |ACL2|::|NAT-LISTP-OF-RANDOM-LIST-AUX|)
@(def |ACL2|::|STATE-P1-OF-RANDOM-LIST-AUX|)") (:FROM . "[books]/system/random.lisp"))) (XDOC::GET-XDOC-TABLE WORLD))) (VALUE-TRIPLE (QUOTE (DEFXDOC RANDOM-LIST-AUX)))))) (VALUE-TRIPLE (QUOTE RANDOM-LIST-AUX))))) (7 RECORD-EXPANSION (DEFSECTION RANDOM-LIST :PARENTS (RANDOM$) :SHORT "Generate a list of random numbers in [0, limit)." (DEFUND RANDOM-LIST (N LIMIT STATE) (DECLARE (XARGS :GUARD (AND (NATP N) (POSP LIMIT)))) (RANDOM-LIST-AUX N LIMIT NIL STATE)) (LOCAL (IN-THEORY (ENABLE RANDOM-LIST))) (DEFTHM NAT-LISTP-OF-RANDOM-LIST (NAT-LISTP (MV-NTH 0 (RANDOM-LIST N LIMIT STATE)))) (DEFTHM STATE-P1-OF-RANDOM-LIST (IMPLIES (FORCE (STATE-P1 STATE)) (STATE-P1 (MV-NTH 1 (RANDOM-LIST N LIMIT STATE)))))) (WITH-OUTPUT :STACK :PUSH :OFF :ALL :ON ERROR (PROGN (TABLE INTRO-TABLE :MARK (QUOTE RANDOM-LIST)) (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (DEFUND RANDOM-LIST (N LIMIT STATE) (DECLARE (XARGS :GUARD (AND (NATP N) (POSP LIMIT)))) (RANDOM-LIST-AUX N LIMIT NIL STATE)) (LOCAL (IN-THEORY (ENABLE RANDOM-LIST))) (DEFTHM NAT-LISTP-OF-RANDOM-LIST (NAT-LISTP (MV-NTH 0 (RANDOM-LIST N LIMIT STATE)))) (DEFTHM STATE-P1-OF-RANDOM-LIST (IMPLIES (FORCE (STATE-P1 STATE)) (STATE-P1 (MV-NTH 1 (RANDOM-LIST N LIMIT STATE))))))) (RECORD-EXPANSION (MAKE-EVENT (LET* ((XDOC::NAME (QUOTE RANDOM-LIST)) (XDOC::PARENTS (QUOTE (RANDOM$))) (XDOC::SHORT (QUOTE "Generate a list of random numbers in [0, limit).")) (XDOC::EXTENSION (QUOTE NIL)) (XDOC::WRLD (W STATE)) (XDOC::TRIPS (REVERSED-WORLD-SINCE-EVENT XDOC::WRLD (QUOTE (TABLE INTRO-TABLE :MARK (QUOTE RANDOM-LIST))) NIL)) (XDOC::INFO (REVERSE (NEW-FORMULA-INFO XDOC::TRIPS XDOC::WRLD NIL))) (XDOC::AUTODOC (XDOC::FORMULA-INFO-TO-DEFS (NOT XDOC::EXTENSION) XDOC::INFO)) (XDOC::LONG (CONCATENATE (QUOTE STRING) (QUOTE "") (COERCE (LIST #\Newline #\Newline) (QUOTE STRING)) XDOC::AUTODOC))) (IF XDOC::EXTENSION (CONS (QUOTE XDOC-EXTEND) (CONS XDOC::EXTENSION (CONS XDOC::LONG (QUOTE NIL)))) (CONS (QUOTE DEFXDOC) (CONS XDOC::NAME (CONS (QUOTE :PARENTS) (CONS XDOC::PARENTS (CONS (QUOTE :SHORT) (CONS XDOC::SHORT (CONS (QUOTE :LONG) (CONS XDOC::LONG (QUOTE NIL)))))))))))) (WITH-OUTPUT :OFF (EVENT SUMMARY) (PROGN (TABLE XDOC (QUOTE DOC) (CONS (QUOTE ((:NAME . RANDOM-LIST) (:BASE-PKG . ACL2-PKG-WITNESS) (:PARENTS RANDOM$) (:SHORT . "Generate a list of random numbers in [0, limit).") (:LONG . "

<h3>Definitions and Theorems</h3>@(def |ACL2|::|RANDOM-LIST|)
@(def |ACL2|::|NAT-LISTP-OF-RANDOM-LIST|)
@(def |ACL2|::|STATE-P1-OF-RANDOM-LIST|)") (:FROM . "[books]/system/random.lisp"))) (XDOC::GET-XDOC-TABLE WORLD))) (VALUE-TRIPLE (QUOTE (DEFXDOC RANDOM-LIST)))))) (VALUE-TRIPLE (QUOTE RANDOM-LIST))))))
NIL
(("/usr/share/acl2-6.3/books/system/random.lisp" "random" "random" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 848383349) (LOCAL ("/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/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/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))
721769190