acl2-books-certs 6.3-5 / usr / share / acl2-6.3 / books / cutil / da-base.cert

(IN-PACKAGE "ACL2")
"ACL2 Version 6.3"
:BEGIN-PORTCULLIS-CMDS
(INCLUDE-BOOK "portcullis")
:END-PORTCULLIS-CMDS
:EXPANSION-ALIST
((3 RECORD-EXPANSION (DEFSECTION TAG :PARENTS (CUTIL::DEFAGGREGATE) :SHORT "Alias for @('car') used by @(see defaggregate)." :LONG "<p>The types introduced by @('defaggregate') are basically objects of
the form @('(tag . field-data)'), where the tag says what kind of object is
being represented (e.g., \"employee\").</p>

<p>The @('tag') function is an alias for @('car'), and so it can be used to get
the tag from these kinds of objects.  We introduce this alias and keep it
disabled so that reasoning about the tags of objects does not slow down
reasoning about @('car') in general.</p>" (DEFINLINED TAG (CUTIL::X) (DECLARE (XARGS :GUARD T)) (MBE :LOGIC (CAR CUTIL::X) :EXEC (IF (CONSP CUTIL::X) (CAR CUTIL::X) NIL))) (DEFTHM CUTIL::TAG-FORWARD-TO-CONSP (IMPLIES (TAG CUTIL::X) (CONSP CUTIL::X)) :RULE-CLASSES :FORWARD-CHAINING :HINTS (("Goal" :IN-THEORY (ENABLE TAG))))) (WITH-OUTPUT :STACK :PUSH :OFF :ALL :ON ERROR (PROGN (TABLE INTRO-TABLE :MARK (QUOTE TAG)) (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (DEFINLINED TAG (CUTIL::X) (DECLARE (XARGS :GUARD T)) (MBE :LOGIC (CAR CUTIL::X) :EXEC (IF (CONSP CUTIL::X) (CAR CUTIL::X) NIL))) (DEFTHM CUTIL::TAG-FORWARD-TO-CONSP (IMPLIES (TAG CUTIL::X) (CONSP CUTIL::X)) :RULE-CLASSES :FORWARD-CHAINING :HINTS (("Goal" :IN-THEORY (ENABLE TAG)))))) (RECORD-EXPANSION (MAKE-EVENT (LET* ((XDOC::NAME (QUOTE TAG)) (XDOC::PARENTS (QUOTE (CUTIL::DEFAGGREGATE))) (XDOC::SHORT (QUOTE "Alias for @('car') used by @(see defaggregate).")) (XDOC::EXTENSION (QUOTE NIL)) (XDOC::WRLD (W STATE)) (XDOC::TRIPS (REVERSED-WORLD-SINCE-EVENT XDOC::WRLD (QUOTE (TABLE INTRO-TABLE :MARK (QUOTE TAG))) 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>The types introduced by @('defaggregate') are basically objects of
the form @('(tag . field-data)'), where the tag says what kind of object is
being represented (e.g., \"employee\").</p>

<p>The @('tag') function is an alias for @('car'), and so it can be used to get
the tag from these kinds of objects.  We introduce this alias and keep it
disabled so that reasoning about the tags of objects does not slow down
reasoning about @('car') in general.</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 . TAG) (:BASE-PKG . CUTIL::ACL2-PKG-WITNESS) (:PARENTS CUTIL::DEFAGGREGATE) (:SHORT . "Alias for @('car') used by @(see defaggregate).") (:LONG . "<p>The types introduced by @('defaggregate') are basically objects of
the form @('(tag . field-data)'), where the tag says what kind of object is
being represented (e.g., \"employee\").</p>

<p>The @('tag') function is an alias for @('car'), and so it can be used to get
the tag from these kinds of objects.  We introduce this alias and keep it
disabled so that reasoning about the tags of objects does not slow down
reasoning about @('car') in general.</p>

<h3>Definitions and Theorems</h3>@(def |ACL2|::|TAG$INLINE|)
@(def |CUTIL|::|TAG-FORWARD-TO-CONSP|)") (:FROM . "[books]/cutil/da-base.lisp"))) (XDOC::GET-XDOC-TABLE WORLD))) (VALUE-TRIPLE (QUOTE (DEFXDOC TAG)))))) (VALUE-TRIPLE (QUOTE TAG))))))
(("/usr/share/acl2-6.3/books/cutil/portcullis.lisp" "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/cutil/da-base.lisp" "da-base" "da-base" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 517345789) ("/usr/share/acl2-6.3/books/cutil/support.lisp" "support" "support" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1180314020) ("/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/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" "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))
1756317979