1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
|
<html>
<head><title>NQTHM-TO-ACL2.html -- ACL2 Version 3.1</title></head>
<body text=#000000 bgcolor="#FFFFFF">
<h2>NQTHM-TO-ACL2</h2>ACL2 analogues of Nqthm functions and commands
<pre>Major Section: <a href="DOCUMENTATION.html">DOCUMENTATION</a>
</pre><p>
<pre>
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.
<p>
General Form:
(nqthm-to-acl2 name)
</pre>
where <code>name</code> 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.<p>
We close with two tables that contain all the information used by
this <code>nqthm-to-acl2</code> 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.<p>
<pre>
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<p>
========================================<p>
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.
</pre>
<br><br><br><a href="acl2-doc.html"><img src="llogo.gif"></a> <a href="acl2-doc-index.html"><img src="index.gif"></a>
</body>
</html>
|
