Major Section: DOCUMENTATION
Example Forms: :nqthm-to-acl2 prove-lemma ; Display ACL2 topic(s) and/or print ; information corresponding to Nqthm ; PROVE-LEMMA command. (nqthm-to-acl2 'prove-lemma) ; Same as above.where
General Form: (nqthm-to-acl2 name)
nameis a notion documented for Nqthm: either a function in the Nqthm logic, or a command. If there is corresponding information available for ACL2, it will be printed in response to this command. This information is not intended to be completely precise, but rather, is intended to help those familiar with Nqthm to make the transition to ACL2.
We close with two tables that contain all the information used by
nqthm-to-acl2 command. The first shows the correspondence
between functions in the Nqthm logic and corresponding ACL2
functions (when possible); the second is similar, but for commands
rather than functions.
Nqthm functions --> ACL2 ---------------------------------------- ADD1 --> 1+ ADD-TO-SET --> ADD-TO-SET-EQUAL and ADD-TO-SET-EQ AND --> AND APPEND --> APPEND and BINARY-APPEND APPLY-SUBR --> No correspondent, but see the documentation for DEFEVALUATOR and META. APPLY$ --> No correspondent, but see the documentation for DEFEVALUATOR and META. ASSOC --> ASSOC-EQUAL, ASSOC and ASSOC-EQ BODY --> No correspondent, but see the documentation for DEFEVALUATOR and META. CAR --> CAR CDR --> CDR CONS --> CONS COUNT --> ACL2-COUNT DIFFERENCE --> - EQUAL --> EQUAL, EQ, EQL and = EVAL$ --> No correspondent, but see the documentation for DEFEVALUATOR and META. FALSE --> Nqthm's F corresponds to the ACL2 symbol NIL. FALSEP --> NOT and NULL FORMALS --> No correspondent, but see the documentation for DEFEVALUATOR and META. GEQ --> >= GREATERP --> > IDENTITY --> IDENTITY IF --> IF IFF --> IFF IMPLIES --> IMPLIES LEQ --> <= LESSP --> < LISTP --> CONSP LITATOM --> SYMBOLP MAX --> MAX MEMBER --> MEMBER-EQUAL, MEMBER and MEMBER-EQ MINUS --> - and UNARY-- NEGATIVEP --> MINUSP NEGATIVE-GUTS --> ABS NLISTP --> ATOM NOT --> NOT NUMBERP --> ACL2-NUMBERP, INTEGERP and RATIONALP OR --> OR ORDINALP --> E0-ORDINALP ORD-LESSP --> E0-ORD-< PACK --> See intern and coerce. PAIRLIST --> PAIRLIS$ PLUS --> + and BINARY-+ QUOTIENT --> / REMAINDER --> REM and MOD STRIP-CARS --> STRIP-CARS SUB1 --> 1- TIMES --> * and BINARY-* TRUE --> The symbol T. UNION --> UNION-EQUAL and UNION-EQ UNPACK --> See symbol-name and coerce. V&C$ --> No correspondent, but see the documentation for DEFEVALUATOR and META. V&C-APPLY$ --> No correspondent, but see the documentation for DEFEVALUATOR and META. ZERO --> The number 0. ZEROP --> ZEROP
Nqthm commands --> ACL2 ---------------------------------------- ACCUMULATED-PERSISTENCE --> ACCUMULATED-PERSISTENCE ADD-AXIOM --> DEFAXIOM ADD-SHELL --> There is no shell principle in ACL2. AXIOM --> DEFAXIOM BACKQUOTE-SETTING --> Backquote is supported in ACL2, but not currently documented. BOOT-STRAP --> GROUND-ZERO BREAK-LEMMA --> MONITOR BREAK-REWRITE --> BREAK-REWRITE CH --> PBT See also :DOC history. CHRONOLOGY --> PBT See also :DOC history. COMMENT --> DEFLABEL COMPILE-UNCOMPILED-DEFNS --> COMP CONSTRAIN --> See :DOC encapsulate and :DOC local. DATA-BASE --> Perhaps the closest ACL2 analogue of DATA-BASE is PROPS. But see :DOC history for a collection of commands for querying the ACL2 database (``world''). Note that the notions of supporters and dependents are not supported in ACL2. DCL --> DEFSTUB DEFN --> DEFUN and DEFMACRO DEFTHEORY --> DEFTHEORY DISABLE --> DISABLE DISABLE-THEORY --> See :DOC theories. The Nqthm command (DISABLE-THEORY FOO) corresponds roughly to the ACL2 command (in-theory (set-difference-theories (current-theory :here) (theory 'foo))). DO-EVENTS --> LD DO-FILE --> LD ELIM --> ELIM ENABLE --> ENABLE ENABLE-THEORY --> See :DOC theories. The Nqthm command (ENABLE-THEORY FOO) corresponds roughly to the ACL2 command (in-theory (union-theories (theory 'foo) (current-theory :here))). EVENTS-SINCE --> PBT FUNCTIONALLY-INSTANTIATE --> ACL2 provides a form of the :USE hint that corresponds roughly to the FUNCTIONALLY-INSTANTIATE event of Nqthm. See :DOC lemma-instance. GENERALIZE --> GENERALIZE HINTS --> HINTS LEMMA --> DEFTHM MAINTAIN-REWRITE-PATH --> BRR MAKE-LIB --> There is no direct analogue of Nqthm's notion of ``library.'' See :DOC books for a description of ACL2's mechanism for creating and saving collections of events. META --> META NAMES --> NAME NOTE-LIB --> INCLUDE-BOOK PPE --> PE PROVE --> THM PROVEALL --> See :DOC ld and :DOC certify-book. The latter corresponds to Nqthm's PROVE-FILE,which may be what you're interested in,really. PROVE-FILE --> CERTIFY-BOOK PROVE-FILE-OUT --> CERTIFY-BOOK PROVE-LEMMA --> DEFTHM See also :DOC hints. R-LOOP --> The top-level ACL2 loop is an evaluation loop as well, so no analogue of R-LOOP is necessary. REWRITE --> REWRITE RULE-CLASSES --> RULE-CLASSES SET-STATUS --> IN-THEORY SKIM-FILE --> LD-SKIP-PROOFSP TOGGLE --> IN-THEORY TOGGLE-DEFINED-FUNCTIONS --> EXECUTABLE-COUNTERPART-THEORY TRANSLATE --> TRANS and TRANS1 UBT --> UBT and U UNBREAK-LEMMA --> UNMONITOR UNDO-BACK-THROUGH --> UBT UNDO-NAME --> See :DOC ubt. There is no way to undo names in ACL2 without undoing back through such names. However, see :DOC ld-skip-proofsp for information about how to quickly recover the state.