• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
    • Theories
    • Rule-classes
    • Proof-builder
    • Hons-and-memoization
    • Events
    • History
    • Parallelism
    • Programming
    • Start-here
      • Gentle-introduction-to-ACL2-programming
      • ACL2-tutorial
        • Introduction-to-the-theorem-prover
        • Pages Written Especially for the Tours
        • The-method
        • Advanced-features
        • Interesting-applications
        • Tips
        • Alternative-introduction
        • Tidbits
        • Annotated-ACL2-scripts
        • Startup
        • ACL2-as-standalone-program
        • ACL2-sedan
        • Talks
        • Nqthm-to-ACL2
        • Emacs
      • About-ACL2
    • Real
    • Debugging
    • Miscellaneous
    • Output-controls
    • Macros
    • Interfacing-tools
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Testing-utilities
  • Math

• ACL2-tutorial

Nqthm-to-ACL2

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 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.