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.
