NQTHM-TO-ACL2

ACL2 analogues of Nqthm functions and commands
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.

General Form: (nqthm-to-acl2 name)

where name is 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 this 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      -->  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.