ACL2 analogues of Nqthm functions and commands

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. General Form: (nqthm-to-acl2 name)

where

We close with two tables that contain all the information used by this

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 --> O-P ORD-LESSP --> O< 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 --> ZP 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.