32
28
* acl2: (acl2-doc-emacs.info). Applicative Common Lisp
40
File: acl2-doc-emacs.info, Node: DEFEXEC, Next: DEFLABEL, Prev: DEFEVALUATOR, Up: EVENTS
42
DEFEXEC attach a terminating executable function to a definition
44
Suppose you define a function (fn x) with a guard of (good-input-p x),
45
and you know that when the guard holds, the measure decreases on each
46
recursive call. Unfortunately, the definitional principle (see *Note
47
DEFUN::) ignores the guard. For example, if the definition has the form
50
(declare (xargs :guard (good-input-p x)))
52
(... (fn (destr x)) ...)
55
then in order to admit this definition, ACL2 must prove the appropriate
56
formula asserting that (destr x) is "smaller than" x under the
57
assumption (not-done-yet x) but without the assumption (good-input-p x),
58
even if (not-done-yet x) is true. In essence, it may be necessary to
59
submit instead the following definition.
62
(declare (xargs :guard (good-input-p x)))
65
(... (fn (destr x)) ...)
69
But it is unfortunate that when calls of fn are evaluated, for example
70
when fn is applied to an explicit constant during a proof, then a call
71
of good-input-p must now be evaluated on each recursive call.
73
Fortunately, defexec provides a way to keep the execution efficient.
74
For the example above we could use the following form.
77
(declare (xargs :guard (good-input-p x)))
78
(mbe :logic (if (good-input-p x)
80
(... (fn (destr x)) ...)
83
:exec (if (not-done-yet x)
84
(... (fn (destr x)) ...)
87
Here "mbe" stands for "must-be-equal" and, roughly speaking, its call
88
above is logically equal to the :logic form but is evaluated using the
89
:exec form when the guard holds. See *Note MBE::. The effect is thus
90
to define fn as shown in the defun form above, but to cause execution of
91
fn using the :exec body. The use of defexec instead of defun in the
92
example above causes a termination proof to be performed, in order to
93
guarantee that evaluation always theoretically terminates, even when
94
using the :exec form for evaluation.
98
; Some of the keyword arguments in the declarations below are irrelevant or
99
; unnecessary, but they serve to illustrate their use.
102
(declare (xargs :measure (+ 15 (acl2-count x))
103
:hints (("Goal" :in-theory (disable nth)))
104
:guard-hints (("Goal" :in-theory (disable last)))
105
:guard (and (integerp x) (<= 0 x) (< x 25)))
107
:test (and (integerp x) (<= 0 x))
108
:default-value 'undef ; defaults to nil
110
:well-founded-relation o<))
111
(mbe :logic (if (zp x)
118
The above example macroexpands to the following.
124
(SET-IRRELEVANT-FORMALS-OK T)
127
(XARGS :VERIFY-GUARDS NIL
128
:HINTS (("Goal" :IN-THEORY (DISABLE NTH)))
130
:WELL-FOUNDED-RELATION O<))
131
(IF (AND (INTEGERP X) (<= 0 X))
132
(IF (= X 0) 1 (* X (F (- X 1))))
134
(LOCAL (DEFTHM F-GUARD-IMPLIES-TEST
135
(IMPLIES (AND (INTEGERP X) (<= 0 X) (< X 25))
136
(AND (INTEGERP X) (<= 0 X)))
137
:RULE-CLASSES NIL))))
139
(DECLARE (XARGS :MEASURE (+ 15 (ACL2-COUNT X))
140
:HINTS (("Goal" :IN-THEORY (DISABLE NTH)))
141
:GUARD-HINTS (("Goal" :IN-THEORY (DISABLE LAST)))
142
:GUARD (AND (INTEGERP X) (<= 0 X) (< X 25))))
144
(IF (ZP X) 1 (* X (F (- X 1))))
146
(IF (= X 0) 1 (* X (F (- X 1)))))))
148
Notice that in the example above, the :hints in the local definition of
149
F are inherited from the :hints in the xargs of the defexec form. We
150
discuss such inheritance below.
153
(defexec fn (var1 ... varn) doc-string dcl ... dcl
154
(mbe :LOGIC logic-body
157
where the syntax is identical to the syntax of defun where the body is a
158
call of mbe, with the exceptions described below. Thus, fn is the
159
symbol you wish to define and is a new symbolic name and (var1 ... varn)
160
is its list of formal parameters (see *Note NAME::). The first
161
exception is that at least one dcl (i.e., declare form) must specify a
162
:guard, guard. The second exception is that one of the dcls is allowed
163
to contain an element of the form (exec-xargs ...). The exec-xargs
164
form, if present, must specify a non-empty keyword-value-listp each of
165
whose keys is one of :test, :default-value, or one of the standard xargs
166
keys of :measure, :well-founded-relation, :hints, or :stobjs. Any of
167
these four standard xargs keys that is present in an xargs of some dcl
168
but is not specified in the (possibly nonexistent) exec-xargs form is
169
considered to be specified in the exec-xargs form, as illustrated in the
170
example above for :hints. (So for example, if you want :hints in the
171
final, non-local definition but not in the local definition, then
172
specify the :hints in the xargs but specify :hints nil in the
173
exec-xargs.) If :test is specified and not nil, let test be its value;
174
otherwise let test default to guard. If :default-value is specified,
175
let default-value be its value; else default-value is nil.
176
Default-value should have the same signature as exec-body; otherwise the
177
defexec form will fail to be admitted.
179
The above General Form's macroexpansion is of the form (PROGN encap
180
final-def), where encap and final-def are as follows. Final-def is
181
simply the result of removing the exec-xargs declaration (if any) from
182
its declare form, and is the result of evaluating the given defexec
183
form, since encap is of the following form.
187
(set-ignore-ok t) ; harmless for proving termination
188
(set-irrelevant-formals-ok t) ; harmless for proving termination
192
The purpose of encap is to ensure the the executable version of name
193
terminates on all arguments. Thus, local-def and local-thm are as
194
follows, where the xargs of the declare form are the result of adding
195
:VERIFY-GUARDS NIL to the result of removing the :test and (optional)
196
:default-value from the exec-xargs.
200
(DECLARE (XARGS :VERIFY-GUARDS NIL ...))
206
(DEFTHM fn-EXEC-GUARD-HOLDS
210
We claim that if the above local-def and local-thm are admitted, then
211
all evaluations of calls of fn terminate. The concern is that the use
212
of mbe in final-def allows for the use of exec-body for a call of fn, as
213
well as for subsequent recursive calls, when guard holds and assuming
214
that the guards have been verified for final-def. However, by local-thm
215
we can conclude in this case that test holds, in which case the call of
216
fn may be viewed as a call of the version of fn defined in local-def.
217
Moreover, since guards have been verified for final-def, then guards
218
hold for subsequent evaluation of exec-body, and in particular for
219
recursive calls of fn, which can thus continue to be viewed as calls
227
File: acl2-doc-emacs.info, Node: DEFLABEL, Next: DEFMACRO, Prev: DEFEXEC, Up: EVENTS
229
DEFLABEL build a landmark and/or add a documentation topic
233
(deflabel interp-section
238
(deflabel name :doc doc-string)
240
where name is a new symbolic name (see *Note NAME::) and doc-string is
241
an optional documentation string (see *Note DOC-STRING::). This event
242
adds the documentation string for symbol name to the :doc data base. By
243
virtue of the fact that deflabel is an event, it also marks the current
244
history with the name. Thus, even undocumented labels are convenient as
245
landmarks in a proof development. For example, you may wish to undo
246
back through some label or compute a theory expression (see *Note
247
THEORIES::) in terms of some labels. Deflabel events are never
248
considered redundant. See *Note REDUNDANT-EVENTS::.
250
See *Note DEFDOC:: for a means of attaching a documentation string to a
251
name without marking the current history with that name.
256
File: acl2-doc-emacs.info, Node: DEFMACRO, Next: DEFPKG, Prev: DEFLABEL, Up: EVENTS
258
DEFMACRO define a macro
263
(list 'if x (list 'not y) y))
265
(defmacro git (sym key)
266
(list 'getprop sym key nil
267
'(quote current-acl2-world)
270
(defmacro one-of (x &rest rst)
271
(declare (xargs :guard (symbol-listp rst)))
272
(cond ((null rst) nil)
274
(list 'eq x (list 'quote (car rst)))
275
(list* 'one-of x (cdr rst))))))
280
(xor a b) (if a (not b) b)
281
(xor a (foo b)) (if a (not (foo b)) (foo b))
283
(git 'car 'lemmas) (getprop 'car 'lemmas nil
287
(one-of x a b c) (or (eq x 'a)
291
(one-of x 1 2 3) ill-formed (guard violation)
294
(defmacro name macro-args doc-string dcl ... dcl body)
296
where name is a new symbolic name (see *Note NAME::), macro-args
297
specifies the formals of the macro (see *Note MACRO-ARGS:: for a
298
description), and body is a term. Doc-string is an optional
299
documentation string; see *Note DOC-STRING::. Each dcl is an optional
300
declaration (see *Note DECLARE::) except that the only xargs keyword
301
permitted by defmacro is :guard.
303
Macroexpansion occurs when a form is read in, i.e., before the
304
evaluation or proof of that form is undertaken. To experiment with
305
macroexpansion, see *Note TRANS::. When a form whose car is name arises
306
as the form is read in, the arguments are bound as described in CLTL
307
pp. 60 and 145, the guard is checked, and then the body is evaluated.
308
The result is used in place of the original form.
310
In ACL2, macros do not have access to state. That is, state is not
311
allowed among the formal parameters. This is in part a reflection of
312
CLTL, pp. 143, "More generally, an implementation of Common Lisp has
313
great latitude in deciding exactly when to expand macro calls with a
314
program. ... Macros should be written in such a way as to depend as
315
little as possible on the execution environment to produce a correct
316
expansion." In ACL2, the product of macroexpansion is independent of the
317
current environment and is determined entirely by the macro body and the
318
functions and constants it references. It is possible, however, to
319
define macros that produce expansions that refer to state or other
320
single-threaded objects (see *Note STOBJ::) or variables not among the
321
macro's arguments. See the git example above.
326
File: acl2-doc-emacs.info, Node: DEFPKG, Next: DEFREFINEMENT, Prev: DEFMACRO, Up: EVENTS
328
DEFPKG define a new symbol package
333
(union-eq *acl2-exports*
334
*common-lisp-symbols-from-main-lisp-package*))
32
File: acl2-doc-emacs.info, Node: MORE!, Next: MORE-DOC, Prev: MORE, Up: DOCUMENTATION
34
MORE! another response to ``(type :more for more, :more! for the rest)''
36
NOTE: The command :more! only makes sense at the terminal.
41
will print all of the remaining documentation started by the last :doc
44
See *Note MORE:: for some background. Typing :more! will print all
45
remaining blocks of documentation.
47
:More! is like :more except that it prints all the text at once. For
48
example, if you type :doc name you will see some text followed by
49
"(type :more for more, :more! for the rest)". If you then type simply
50
:more! you will see all of the details, while if you type :more you
51
will be fed the next block of details.
54
File: acl2-doc-emacs.info, Node: MORE-DOC, Next: NQTHM-TO-ACL2, Prev: MORE!, Up: DOCUMENTATION
56
MORE-DOC a continuation of the :doc documentation
58
NOTE: The :more-doc command only makes sense at the terminal.
61
ACL2 !>:more-doc DEFTHM
62
ACL2 !>:more-doc logical-name
64
Often it is assumed in the text provided by :more-doc name that you
65
have read the text provided by :doc name.
67
:More-doc just continues spewing out at you the documentation string
68
provided with a definition. If the user has done his job, :doc will
69
probably remind you of the basics and :more-doc, if read after :doc,
70
will address obscure details that are nevertheless worth noting.
72
When :more-doc types "(type :more for more, :more! for the rest)" you
73
can get the next block of the continuation by typing :more or all of
74
the remaining blocks by typing :more!. See *Note MORE::.
77
File: acl2-doc-emacs.info, Node: NQTHM-TO-ACL2, Prev: MORE-DOC, Up: DOCUMENTATION
79
NQTHM-TO-ACL2 ACL2 analogues of Nqthm functions and commands
82
:nqthm-to-acl2 prove-lemma ; Display ACL2 topic(s) and/or print
83
; information corresponding to Nqthm
84
; PROVE-LEMMA command.
85
(nqthm-to-acl2 'prove-lemma) ; Same as above.
90
where name is a notion documented for Nqthm: either a function in the
91
Nqthm logic, or a command. If there is corresponding information
92
available for ACL2, it will be printed in response to this command.
93
This information is not intended to be completely precise, but rather,
94
is intended to help those familiar with Nqthm to make the transition to
97
We close with two tables that contain all the information used by this
98
nqthm-to-acl2 command. The first shows the correspondence between
99
functions in the Nqthm logic and corresponding ACL2 functions (when
100
possible); the second is similar, but for commands rather than
103
Nqthm functions --> ACL2
104
----------------------------------------
106
ADD-TO-SET --> ADD-TO-SET-EQUAL and ADD-TO-SET-EQ
108
APPEND --> APPEND and BINARY-APPEND
109
APPLY-SUBR --> No correspondent, but see the documentation for
110
DEFEVALUATOR and META.
111
APPLY$ --> No correspondent, but see the documentation for
112
DEFEVALUATOR and META.
113
ASSOC --> ASSOC-EQUAL, ASSOC and ASSOC-EQ
114
BODY --> No correspondent, but see the documentation for
115
DEFEVALUATOR and META.
121
EQUAL --> EQUAL, EQ, EQL and =
122
EVAL$ --> No correspondent, but see the documentation for
123
DEFEVALUATOR and META.
124
FALSE --> Nqthm's F corresponds to the ACL2 symbol NIL.
125
FALSEP --> NOT and NULL
126
FORMALS --> No correspondent, but see the documentation for
127
DEFEVALUATOR and META.
130
IDENTITY --> IDENTITY
139
MEMBER --> MEMBER-EQUAL, MEMBER and MEMBER-EQ
140
MINUS --> - and UNARY--
142
NEGATIVE-GUTS --> ABS
145
NUMBERP --> ACL2-NUMBERP, INTEGERP and RATIONALP
149
PACK --> See intern and coerce.
150
PAIRLIST --> PAIRLIS$
151
PLUS --> + and BINARY-+
153
REMAINDER --> REM and MOD
154
STRIP-CARS --> STRIP-CARS
156
TIMES --> * and BINARY-*
157
TRUE --> The symbol T.
158
UNION --> UNION-EQUAL and UNION-EQ
159
UNPACK --> See symbol-name and coerce.
160
V&C$ --> No correspondent, but see the documentation for
161
DEFEVALUATOR and META.
162
V&C-APPLY$ --> No correspondent, but see the documentation for
163
DEFEVALUATOR and META.
164
ZERO --> The number 0.
167
========================================
169
Nqthm commands --> ACL2
170
----------------------------------------
171
ACCUMULATED-PERSISTENCE
172
--> ACCUMULATED-PERSISTENCE
173
ADD-AXIOM --> DEFAXIOM
174
ADD-SHELL --> There is no shell principle in ACL2.
177
--> Backquote is supported in ACL2, but not
178
currently documented.
179
BOOT-STRAP --> GROUND-ZERO
180
BREAK-LEMMA --> MONITOR
181
BREAK-REWRITE --> BREAK-REWRITE
183
See also :DOC history.
185
See also :DOC history.
187
COMPILE-UNCOMPILED-DEFNS
189
CONSTRAIN --> See :DOC encapsulate and :DOC local.
190
DATA-BASE --> Perhaps the closest ACL2 analogue of DATA-BASE
191
is PROPS. But see :DOC history for a collection
192
of commands for querying the ACL2 database
193
(``world''). Note that the notions of
194
supporters and dependents are not supported in
197
DEFN --> DEFUN and DEFMACRO
198
DEFTHEORY --> DEFTHEORY
201
--> See :DOC theories. The Nqthm command
202
(DISABLE-THEORY FOO) corresponds roughly to the
204
(in-theory (set-difference-theories
205
(current-theory :here)
211
ENABLE-THEORY --> See :DOC theories. The Nqthm command
212
(ENABLE-THEORY FOO) corresponds roughly to the
214
(in-theory (union-theories
216
(current-theory :here))).
218
FUNCTIONALLY-INSTANTIATE
219
--> ACL2 provides a form of the :USE hint that
220
corresponds roughly to the
221
FUNCTIONALLY-INSTANTIATE event of Nqthm. See
223
GENERALIZE --> GENERALIZE
226
MAINTAIN-REWRITE-PATH
228
MAKE-LIB --> There is no direct analogue of Nqthm's notion of
229
``library.'' See :DOC books for a description
230
of ACL2's mechanism for creating and saving
231
collections of events.
234
NOTE-LIB --> INCLUDE-BOOK
237
PROVEALL --> See :DOC ld and :DOC certify-book. The latter
238
corresponds to Nqthm's PROVE-FILE,which may be
239
what you're interested in,really.
240
PROVE-FILE --> CERTIFY-BOOK
243
PROVE-LEMMA --> DEFTHM
245
R-LOOP --> The top-level ACL2 loop is an evaluation loop as
246
well, so no analogue of R-LOOP is necessary.
248
RULE-CLASSES --> RULE-CLASSES
249
SET-STATUS --> IN-THEORY
250
SKIM-FILE --> LD-SKIP-PROOFSP
252
TOGGLE-DEFINED-FUNCTIONS
253
--> EXECUTABLE-COUNTERPART-THEORY
254
TRANSLATE --> TRANS and TRANS1
256
UNBREAK-LEMMA --> UNMONITOR
259
UNDO-NAME --> See :DOC ubt. There is no way to undo names in
260
ACL2 without undoing back through such names.
261
However, see :DOC ld-skip-proofsp for
262
information about how to quickly recover the
266
File: acl2-doc-emacs.info, Node: EVENTS, Next: HISTORY, Prev: DOCUMENTATION, Up: Top
268
EVENTS functions that extend the logic
272
* ADD-BINOP:: associate a binary function name with a macro name
274
* ADD-DEFAULT-HINTS:: add to the default hints
276
* ADD-DEFAULT-HINTS!:: add to the default hints non-locally
278
* ADD-DIVE-INTO-MACRO:: associate proof-checker diving function with macro name
280
* ADD-INCLUDE-BOOK-DIR:: associate directory to keyword for include-book's :dir argument
282
* ADD-INVISIBLE-FNS:: make some unary functions invisible to the loop-stopper algorithm
284
* ADD-MACRO-ALIAS:: associate a function name with a macro name
286
* ADD-MATCH-FREE-OVERRIDE:: set :match-free value to :once or :all in existing rules
288
* ADD-NTH-ALIAS:: associate one symbol with another for printing of nth/update-nth terms
290
* ASSERT-EVENT:: assert that a given form returns a non-nil value
292
* BINOP-TABLE:: associates binary function with the corresponding macro
294
* COMP:: compile some ACL2 functions
296
* DEFABBREV:: a convenient form of macro definition for simple expansions
298
* DEFAULT-HINTS-TABLE:: a table used to provide hints for proofs
300
* DEFAXIOM:: add an axiom
302
* DEFCHOOSE:: define a Skolem (witnessing) function
304
* DEFCONG:: prove that one equivalence relation preserves another in a given
305
argument position of a given function
307
* DEFCONST:: define a constant
309
* DEFDOC:: add a documentation topic
311
* DEFEQUIV:: prove that a function is an equivalence relation
313
* DEFEVALUATOR:: introduce an evaluator function
315
* DEFEXEC:: attach a terminating executable function to a definition
317
* DEFLABEL:: build a landmark and/or add a documentation topic
319
* DEFMACRO:: define a macro
321
* DEFPKG:: define a new symbol package
323
* DEFREFINEMENT:: prove that equiv1 refines equiv2
325
* DEFSTOBJ:: define a new single-threaded object
327
* DEFSTUB:: stub-out a function symbol
329
* DEFTHEORY:: define a theory (to enable or disable a set of rules)
331
* DEFTHM:: prove and name a theorem
333
* DEFTHMD:: prove and name a theorem and then disable it
335
* DEFTTAG:: introduce a trust tag (ttag)
337
* DEFUN:: define a function symbol
339
* DEFUN-SK:: define a function whose body has an outermost quantifier
341
* DEFUND:: define a function symbol and then disable it
343
* DELETE-INCLUDE-BOOK-DIR:: remove association of keyword for include-book's :dir argument
345
* DIVE-INTO-MACROS-TABLE:: right-associated function information for the proof-checker
347
* ENCAPSULATE:: constrain some functions and/or hide some events
349
* IN-ARITHMETIC-THEORY:: designate ``current'' theory for some rewriting done in linear arithmetic
351
* IN-THEORY:: designate ``current'' theory (enabling its rules)
353
* INCLUDE-BOOK:: load the events in a file
355
* INVISIBLE-FNS-TABLE:: functions that are invisible to the loop-stopper algorithm
357
* LOCAL:: hiding an event in an encapsulation or book
359
* LOGIC:: to set the default defun-mode to :logic
361
* MACRO-ALIASES-TABLE:: a table used to associate function names with macro names
363
* MAKE-EVENT:: evaluate (expand) a given form and then evaluate the result
365
* MUTUAL-RECURSION:: define some mutually recursive functions
367
* NTH-ALIASES-TABLE:: a table used to associate names for nth/update-nth printing
369
* PROGN:: evaluate some events
371
* PROGN!:: evaluate some forms, not necessarily events
373
* PROGRAM:: to set the default defun-mode to :program
375
* PUSH-UNTOUCHABLE:: add name or list of names to the list of untouchable symbols
377
* REDO-FLAT:: redo up through a failure in an encapsulate or progn
379
* REMOVE-BINOP:: remove the association of a binary function name with a macro name
381
* REMOVE-DEFAULT-HINTS:: remove from the default hints
383
* REMOVE-DEFAULT-HINTS!:: remove from the default hints non-locally
385
* REMOVE-DIVE-INTO-MACRO:: removes association of proof-checker diving function with macro name
387
* REMOVE-INVISIBLE-FNS:: make some unary functions no longer invisible
389
* REMOVE-MACRO-ALIAS:: remove the association of a function name with a macro name
391
* REMOVE-NTH-ALIAS:: remove the association of one symbol with another for printing of nth/update-nth terms
393
* REMOVE-UNTOUCHABLE:: remove name or list of names to the list of untouchable symbols
395
* RESET-PREHISTORY:: reset the prehistory
397
* SET-BACKCHAIN-LIMIT:: Sets the backchain-limit used by the rewriter
399
* SET-BODY:: set the definition body
401
* SET-BOGUS-MUTUAL-RECURSION-OK:: allow unnecessary ``mutual recursion''
403
* SET-CASE-SPLIT-LIMITATIONS:: set the case-split-limitations
405
* SET-COMPILE-FNS:: have each function compiled as you go along.
407
* SET-DEFAULT-BACKCHAIN-LIMIT:: sets the default backchain-limit used when admitting a rule
409
* SET-DEFAULT-HINTS:: set the default hints
411
* SET-DEFAULT-HINTS!:: set the default hints non-locally
413
* SET-ENFORCE-REDUNDANCY:: require most events to be redundant
415
* SET-IGNORE-OK:: allow unused formals and locals without an ignore or ignorable declaration
417
* SET-INHIBIT-WARNINGS:: control warnings
419
* SET-INVISIBLE-FNS-TABLE:: set the invisible functions table
421
* SET-IRRELEVANT-FORMALS-OK:: allow irrelevant formals in definitions
423
* SET-LET*-ABSTRACTIONP:: to shorten many prettyprinted clauses
425
* SET-MATCH-FREE-DEFAULT:: provide default for :match-free in future rules
427
* SET-MATCH-FREE-ERROR:: control error vs. warning when :match-free is missing
429
* SET-MEASURE-FUNCTION:: set the default measure function symbol
431
* SET-NON-LINEARP:: to turn on or off non-linear arithmetic reasoning
433
* SET-NU-REWRITER-MODE:: to turn on and off the nu-rewriter
435
* SET-REWRITE-STACK-LIMIT:: Sets the rewrite stack depth used by the rewriter
437
* SET-STATE-OK:: allow the use of STATE as a formal parameter
439
* SET-VERIFY-GUARDS-EAGERNESS:: the eagerness with which guard verification is tried.
441
* SET-WELL-FOUNDED-RELATION:: set the default well-founded relation
443
* TABLE:: user-managed tables
445
* TERM-TABLE:: a table used to validate meta rules
447
* THEORY-INVARIANT:: user-specified invariants on theories
449
* USER-DEFINED-FUNCTIONS-TABLE:: an advanced table used to replace certain system functions
451
* VERIFY-GUARDS:: verify the guards of a function
453
* VERIFY-TERMINATION:: convert a function from :program mode to :logic mode
455
* WITH-OUTPUT:: suppressing or turning on specified output for an event
457
Any extension of the syntax of ACL2 (i.e., the definition of a new
458
constant or macro), the axioms (i.e., the definition of a function), or
459
the rule data base (i.e., the proof of a theorem), constitutes a
460
logical "event." Events change the ACL2 logical world (see *note
461
WORLD::). Indeed, the only way to change the ACL2 world is via the
462
successful evaluation of an event function. Every time the world is
463
changed by an event, a landmark is left on the world and it is thus
464
possible to identify the world "as of" the evaluation of a given event.
465
An event may introduce new logical names. Some events introduce no
466
new names (e.g., verify-guards), some introduce exactly one (e.g.,
467
defmacro and defthm), and some may introduce many (e.g., encapsulate ).
470
File: acl2-doc-emacs.info, Node: ADD-BINOP, Next: ADD-DEFAULT-HINTS, Prev: EVENTS, Up: EVENTS
472
ADD-BINOP associate a binary function name with a macro name
475
(add-binop append binary-append)
477
This example associates the function symbol binary-append with the
478
macro name append. As a result, theory functions will understand that
479
append refers to binary-append -- see *note ADD-MACRO-ALIAS:: -- and
480
moreover, proof output will be printed using append rather than
481
binary-append, e.g., (append x y z w) is printed rather than
482
(binary-append x (binary-append y (binary-append z w))).
485
(add-binop macro-name function-name)
487
This is a convenient way to add an entry to macro-aliases-table and at
488
the same time extend the :binop-table. See *Note
489
MACRO-ALIASES-TABLE::, see *note REMOVE-MACRO-ALIAS::, see *note
490
BINOP-TABLE::, and see *note REMOVE-BINOP::.
493
File: acl2-doc-emacs.info, Node: ADD-DEFAULT-HINTS, Next: ADD-DEFAULT-HINTS!, Prev: ADD-BINOP, Up: EVENTS
495
ADD-DEFAULT-HINTS add to the default hints
499
(add-default-hints '((computed-hint-1 clause)
500
(computed-hint-2 clause
501
stable-under-simplificationp)))
503
Note: This is an event! It does not print the usual event summary but
504
nevertheless changes the ACL2 logical world and is so recorded. It is
505
local to the book or encapsulate form in which it occurs (see *note
506
ADD-DEFAULT-HINTS!:: for a corresponding non-local event).
509
(add-default-hints lst)
511
where lst is a list. Generally speaking, the elements of lst should be
512
suitable for use as computed-hints.
514
This event is completely analogous to set-default-hints, the difference
515
being that add-default-hints appends the indicated hints to the list of
516
default hints, rather than *replacing* the default hints with the
519
Finally, note that the effects of set-default-hints, add-default-hints,
520
and remove-default-hints are local to the book in which they appear.
521
Thus, users who include a book with such forms will not have their
522
default hints affected by such forms. In order to export the effect of
523
setting the default hints, use set-default-hints!, add-default-hints!,
524
or remove-default-hints!.
527
File: acl2-doc-emacs.info, Node: ADD-DEFAULT-HINTS!, Next: ADD-DIVE-INTO-MACRO, Prev: ADD-DEFAULT-HINTS, Up: EVENTS
529
ADD-DEFAULT-HINTS! add to the default hints non-locally
531
Please see *note ADD-DEFAULT-HINTS::, which is the same as
532
add-default-hints! except that the latter is not local to the
533
encapsulate or the book in which it occurs. Probably add-default-hints
534
is to be preferred unless you have a good reason for wanting to export
535
the effect of this event outside the enclosing encapsulate or book.
538
File: acl2-doc-emacs.info, Node: ADD-DIVE-INTO-MACRO, Next: ADD-INCLUDE-BOOK-DIR, Prev: ADD-DEFAULT-HINTS!, Up: EVENTS
540
ADD-DIVE-INTO-MACRO associate proof-checker diving function with macro name
543
(add-dive-into-macro cat expand-address-cat)
545
This feature is used so that the proof-checker's DV command and numeric
546
diving commands (e.g., 3) will dive properly into subterms. Please see
547
*note DIVE-INTO-MACROS-TABLE::.
550
File: acl2-doc-emacs.info, Node: ADD-INCLUDE-BOOK-DIR, Next: ADD-INVISIBLE-FNS, Prev: ADD-DIVE-INTO-MACRO, Up: EVENTS
552
ADD-INCLUDE-BOOK-DIR associate directory to keyword for include-book's :dir argument
555
(add-include-book-dir :smith "/u/smith/")
556
; For (include-book "foo" :dir :smith), prepend "/u/smith/" to "foo".
559
(add-include-book-dir kwd dir)
561
where kwd is a keywordp and dir is the absolute pathname (see *note
562
PATHNAME::) of a directory. The effect of this event is to modify the
563
meaning of the :dir keyword argument of include-book as indicated by
564
the examples above, namely by associating the indicated directory with
565
the indicated keyword for purposes of the include-book :dir argument.
566
See *Note DELETE-INCLUDE-BOOK-DIR:: for how to undo this effect.
568
Caveat: The keyword :system cannot be redefined. It will always point
569
to the absolute pathname of the distributed books directory, which by
570
default is immediately under the directory where the ACL2 executable
571
was originally built (see *note INCLUDE-BOOK::, in particular the
572
discussion there of "books directory").
574
Note: This is an event! It does not print the usual event summary but
575
nevertheless changes the ACL2 logical world and is so recorded.
577
This macro generates a call (table acl2-defaults-table
578
:include-book-dir-alist ...) and hence is local to any books and
579
encapsulate events in which it occurs. See *Note ACL2-DEFAULTS-TABLE::.
582
File: acl2-doc-emacs.info, Node: ADD-INVISIBLE-FNS, Next: ADD-MACRO-ALIAS, Prev: ADD-INCLUDE-BOOK-DIR, Up: EVENTS
584
ADD-INVISIBLE-FNS make some unary functions invisible to the loop-stopper algorithm
587
(add-invisible-fns binary-+ unary-- foo)
589
The setting above has makes unary functions unary- and foo "invisible"
590
for the purposes of applying permutative :rewrite rules to binary-+
591
trees. Thus, arg and (unary- arg) will be given the same weight and
592
will be permuted so as to be adjacent.
595
(add-invisible-fns top-fn unary-fn1 ... unary-fnk)
597
where top-fn is a function symbol and the unary-fni are unary function
600
For more information see *note INVISIBLE-FNS-TABLE::. Also see *note
601
SET-INVISIBLE-FNS-TABLE::, which explains how to set the entire table
602
in a single event, and see *note REMOVE-INVISIBLE-FNS::.
605
File: acl2-doc-emacs.info, Node: ADD-MACRO-ALIAS, Next: ADD-MATCH-FREE-OVERRIDE, Prev: ADD-INVISIBLE-FNS, Up: EVENTS
607
ADD-MACRO-ALIAS associate a function name with a macro name
610
(add-macro-alias append binary-append)
612
This example associates the function symbol binary-append with the
613
macro name append. As a result, the name append may be used as a runic
614
designator (see *note THEORIES::) by the various theory functions. See
615
*Note MACRO-ALIASES-TABLE:: for more details.
618
(add-macro-alias macro-name function-name)
620
This is a convenient way to add an entry to macro-aliases-table. See
621
*Note MACRO-ALIASES-TABLE:: and also see *note REMOVE-MACRO-ALIAS::.
624
File: acl2-doc-emacs.info, Node: ADD-MATCH-FREE-OVERRIDE, Next: ADD-NTH-ALIAS, Prev: ADD-MACRO-ALIAS, Up: EVENTS
626
ADD-MATCH-FREE-OVERRIDE set :match-free value to :once or :all in existing rules
629
(add-match-free-override :once t)
630
; Try only the first binding of free variables when relieving hypotheses
631
; of any rule of class :rewrite, :linear, or :forward-chaining.
632
(add-match-free-override :all (:rewrite foo) (:rewrite bar))
633
; For rewrite rules foo and bar, try all bindings of free variables when
634
; relieving hypotheses.
635
(add-match-free-override :clear)
636
; Restore :match-free to what was originally stored for each rule (either
639
As described elsewhere (see *note FREE-VARIABLES::), a rewrite, linear,
640
or forward-chaining rule may have free variables in its hypotheses, and
641
ACL2 can be directed either to try all bindings (":all") or just the
642
first (":once") when relieving a hypothesis, as a basis for relieving
643
subsequent hypotheses. This direction is generally provided by
644
specifying either :match-free :once or :match-free :all in the
645
:rule-classes of the rule, or by using the most recent
646
set-match-free-default event. Also see *note RULE-CLASSES::.
648
However, if a proof is going slowly, you may want to modify the
649
behavior of some such rules so that they use only the first match for
650
free variables in a hypothesis when relieving subsequent hypotheses,
651
rather than backtracking and trying additional matches as necessary.
652
The event (add-match-free-override :once t) has that effect. Or at the
653
other extreme, perhaps you want to specify all rules as :all rules
654
except for a some specific exceptions. Then you can execute
655
(add-match-free-override :all t) followed by, say,
656
(add-match-free-override :once (:rewrite foo) (:linear bar)).
659
(add-match-free-override :clear)
660
(add-match-free-override flg t)
661
(add-match-free-override flg rune1 rune2 ... runek)
663
where flg is :once or :all and the runei are runes. If :clear is
664
specified then all rules will have the :all/:once behavior from when
665
they were first stored. The second general form causes all rewrite
666
linear, and forward-chaining rules to have the behavior specified by
667
flg (:all or :once). Finally, the last of these, where runes are
668
specified, is additive in the sense that only the indicated rules are
669
affected; all others keep the behavior they had just before this event
670
was executed (possible because of earlier add-match-free-override
673
At the conclusion of this event, ACL2 prints out the list of all
674
:linear, :rewrite, and :forward-chaining runes whose rules contain free
675
variables in hypotheses that are to be bound :once, except that if
676
there are no overrides (value :clear was used), then :clear is printed.
678
This event only affects rules that exist at the time it is executed.
679
Future rules are not affected by the override.
681
Note: This is an event! It does not print the usual event summary but
682
nevertheless changes the ACL2 logical world and is so recorded. It
683
uses the acl2-defaults-table, and hence its effect is local to the book
684
or encapsulate form in which it occurs.
688
Lists of the :rewrite, :linear, and :forward-chaining runes whose
689
behavior was originally :once or :all are returned by the following
692
(free-var-runes :once (w state))
693
(free-var-runes :all (w state))
697
(match-free-override (w state))
699
evaluates to a pair, whose car is a number used by ACL2 to determine
700
whether a rune is sufficiently old to be affected by the override, and
701
whose cdr is the list of runes whose behavior is specified as :once by
702
add-match-free-override; except, if no runes have been overridden, then
703
the keyword :clear is returned.
706
File: acl2-doc-emacs.info, Node: ADD-NTH-ALIAS, Next: ASSERT-EVENT, Prev: ADD-MATCH-FREE-OVERRIDE, Up: EVENTS
708
ADD-NTH-ALIAS associate one symbol with another for printing of nth/update-nth terms
711
(add-nth-alias st0 st)
713
This example associates the symbol st0 with the symbol st for purposes
714
of printing certain terms of the form (nth n st0) and (update-nth n val
718
(add-nth-alias alias-name name)
720
This is a convenient way to add an entry to nth-aliases-table. See
721
*Note NTH-ALIASES-TABLE:: and also see *note REMOVE-NTH-ALIAS::.
724
File: acl2-doc-emacs.info, Node: ASSERT-EVENT, Next: BINOP-TABLE, Prev: ADD-NTH-ALIAS, Up: EVENTS
726
ASSERT-EVENT assert that a given form returns a non-nil value
729
(assert-event (equal (+ 3 4) 7))
730
(assert-event (equal (+ 3 4) 7) :on-skip-proofs t)
734
(assert-event form :on-skip-proofs t)
736
Assert-event takes a ground form, i.e., one with no free variables;
737
stobjs are allowed but only a single non-stobj value can be returned.
738
The form is then evaluated and if the result is nil, then a so-called
739
hard error (see *note ER::) results. This evaluation is however not
740
done if proofs are being skipped, as during include-book (also see
741
*note SKIP-PROOFS:: and see *note LD-SKIP-PROOFSP::), unless
742
:on-skip-proofs t is supplied.
744
This form may be put into a book to be certified (see *note BOOKS::),
745
because assert-event is a macro whose calls expand to calls of
746
value-triple (see *note EMBEDDED-EVENT-FORM::).
749
File: acl2-doc-emacs.info, Node: BINOP-TABLE, Next: COMP, Prev: ASSERT-EVENT, Up: EVENTS
751
BINOP-TABLE associates binary function with the corresponding macro
754
ACL2 !>(binop-table (w state))
757
(binary-append . append)
758
(binary-logand . logand)
759
(binary-logior . logior)
760
(binary-logxor . logxor)
761
(binary-logeqv . logeqv))
763
See *Note TABLE:: for a general discussion of tables.
765
See *Note ADD-BINOP:: for a more general discussion of this table.
768
File: acl2-doc-emacs.info, Node: COMP, Next: DEFABBREV, Prev: BINOP-TABLE, Up: EVENTS
770
COMP compile some ACL2 functions
773
:comp t ; compile all uncompiled ACL2 functions
774
(comp t) ; same as above, but can be put into a book
775
(comp :exec) ; compile all uncompiled logic (``*1*'') definitions
776
:comp foo ; compile the defined function foo
777
:comp (:raw foo) ; compile the raw Lisp version of the defined function foo
778
but not the corresponding logic definition
779
:comp (foo bar) ; compile the defined functions foo and bar
780
:comp (foo (:raw bar)) ; compile the defined functions foo and bar, but for
781
; bar do not compile the corresponding logic definition
785
where specifier is one of the following:
787
t compile all user-defined ACL2 functions that are
788
currently uncompiled (redefined built-in functions
790
:exec same as t, except that only logic versions are
791
compiled (see below), not raw Lisp definitions
792
:raw same as t, except that only raw Lisp definitions are
793
compiled, not logic version (see below)
794
(name-1 ... name-k) a non-empty list of names of functions defined by
795
DEFUN in ACL2, except that each name-i can be of
796
the form (:raw sym) or (:exec sym), where sym is
797
the name of such a function
800
When you define a function in ACL2, you are really causing two
801
definitions to be made "under the hood" in Common Lisp: the definition
802
is submitted explicitly to raw Lisp, but so is a corresponding "logic
803
definition". If guards have not been verified, then only the logic
804
definition will be evaluated; see *note GUARDS-AND-EVALUATION::, in
805
particular the section titled "Guards and evaluation V: efficiency
808
Thus, if you are not verifying guards and you want the benefit of Lisp
809
compilation for speed and space efficiency, then you may want to place
810
the form (comp :exec) in your books.
812
Generally it is not necessary to place the form (comp t), or the form
813
(comp :raw), in a book, because certify-book compiles the raw Lisp
814
definitions anyhow, by default. But you may wish to put (comp t) or
815
(comp fn1 fn2 ... fnk) in a book when such a form precedes expensive
816
calls of functions, for example for proofs involving calls of functions
817
on large constants, or to support computationally expensive
820
As suggested by the examples above, if a function specifier is of the
821
form (:raw fn), then fn will be compiled in raw Common Lisp but its
822
corresponding logic definition will not be compiled; and for (:exec fn),
823
it's the other way around.
825
The use of :comp creates various files whose names start with "TMP*",
826
but then deletes them. If you want to keep these files around for some
827
reason, evaluate (assign keep-tmp-files t).
831
* COMP-GCL:: compile some ACL2 functions leaving .c and .h files
833
Also see *note SET-COMPILE-FNS:: for a way to compile each function as
834
it is defined. But note that set-compile-fns is ignored during
837
:cited-by Programming
840
File: acl2-doc-emacs.info, Node: COMP-GCL, Prev: COMP, Up: COMP
842
COMP-GCL compile some ACL2 functions leaving .c and .h files
844
Comp-gcl is for use by experts who want to examine the results of GCL
845
compilation, and it may only be used with ACL2 implementations built on
846
top of GCL. It takes exactly the same arguments as comp, and has the
847
same basic functionality (see *note COMP::), but has two additional
848
effects. First, files "TMP.lisp" and "TMP1.lisp" are always created,
849
even when a single function is specified. Second, comp-gcl always
850
leaves files "TMP.c", "TMP.h", "TMP1.c", and "TMP1.h" when compilation
854
File: acl2-doc-emacs.info, Node: DEFABBREV, Next: DEFAULT-HINTS-TABLE, Prev: COMP, Up: EVENTS
856
DEFABBREV a convenient form of macro definition for simple expansions
859
(defabbrev snoc (x y) (append y (list x)))
860
(defabbrev sq (x) (declare (type (signed-byte 8) x)) (* x x))
863
(defabbrev name (v1 ... vn) doc-string decl1 ... declk body)
865
where name is a new function symbol, the vi are distinct variable
866
symbols, and body is a term. The decli, if supplied, should be legal
867
declare forms; see *note DECLARE::. Doc-string is an optional
868
documentation string; see *note DOC-STRING::.
870
Roughly speaking, the defabbrev event is akin to defining f so that (f
871
v1 ... vn) = body. But rather than do this by adding a new axiom,
872
defabbrev defines f to be a macro so that (f a1 ... an) expands to
873
body, with the "formals," vi, replaced by the "actuals," ai.
875
For example, if snoc is defined as shown in the first example above,
876
then (snoc (+ i j) temp) is just an abbreviation for
878
(append temp (list (+ i j))).
880
In order to generate efficiently executable Lisp code, the macro that
881
defabbrev introduces uses a let to bind the "formals" to the "actuals."
882
Consider the second example above. Logically speaking, (sq (ack i j))
883
is an abbreviation for (* (ack i j) (ack i j)). But in fact the macro
884
for sq introduced by defabbrev actually arranges for (sq (ack i j)) to
890
which executes more efficiently than (* (ack i j) (ack i j)).
892
In the theorem prover, the let above expands to
894
((lambda (x) (* x x)) (ack i j))
896
and thence to (* (ack i j) (ack i j)).
898
It is important to note that the term in body should not contain a call
899
of name -- i.e., defabbrev should not be used in place of defun when
900
the function is recursive. ACL2 will not complain when the defabbrev
901
form is processed, but instead ACL2 will more than likely go into an
902
infinite loop during macroexpansion of any form that has a call of name.
904
It is also important to note that the parameters of any call of a macro
905
defined by defabbrev will, as is the case for the parameters of a
906
function call, be evaluated before the body is evaluated, since this is
907
the evaluation order of let. This may lead to some errors or
908
unexpected inefficiencies during evaluation if the body contains any
909
conditionally evaluted forms like cond, case, or if. Consider the
913
(if (test x) (bar y) nil))
915
Notice a typical one-step expansion of a call of foo (see *note
918
ACL2 !>:trans1 (foo expr1 expr2)
919
(LET ((X EXPR1) (Y EXPR2))
920
(IF (TEST X) (BAR Y) NIL))
923
Now imagine that expr2 is a complicated expression whose evaluation is
924
intended only when the predicate test holds of expr1. The expansion
925
above suggests that expr2 will always be evaluated by the call (foo
926
expr1 expr2), which may be inefficient (since perhaps we only need that
927
value when test is true of expr1). The evaluation of expr2 may even
928
cause an error, for example in :program mode if the expression expr2 has
929
been constructed in a manner that could cause a guard violation unless
933
File: acl2-doc-emacs.info, Node: DEFAULT-HINTS-TABLE, Next: DEFAXIOM, Prev: DEFABBREV, Up: EVENTS
935
DEFAULT-HINTS-TABLE a table used to provide hints for proofs
937
Please see *note SET-DEFAULT-HINTS::, see *note ADD-DEFAULT-HINTS::, and
938
see *note REMOVE-DEFAULT-HINTS:: for how to use this table. For
939
completeness, we mention here that under the hood, these events all
940
update the default-hints-table by updating its unique key, t, for
943
(table default-hints-table t
944
'((computed-hint-1 clause)
945
(computed-hint-2 clause
946
stable-under-simplificationp)))
948
The use of default hints is explained elsewhere; see *note
952
File: acl2-doc-emacs.info, Node: DEFAXIOM, Next: DEFCHOOSE, Prev: DEFAULT-HINTS-TABLE, Up: EVENTS
954
DEFAXIOM add an axiom
956
WARNING: We strongly recommend that you not add axioms. If at all
957
possible you should use defun or mutual-recursion to define new
958
concepts recursively or use encapsulate to constrain them
959
constructively. If your goal is to defer a proof by using a top-down
960
style, consider using skip-proofs; see the discussion on "Top-Down
961
Proof" in Section B.1.2 of "Computer-Aided Reasoning: An Approach."
962
Adding new axioms frequently renders the logic inconsistent.
965
(defaxiom sbar (equal t nil)
967
:doc ":Doc-Section ...")
971
:rule-classes rule-classes
974
where name is a new symbolic name (see *note NAME::), term is a term
975
intended to be a new axiom, and rule-classes and doc-string are as
976
described in the corresponding documentation topics . The two keyword
977
arguments are optional. If :rule-classes is not supplied, the list
978
(:rewrite) is used; if you wish the axiom to generate no rules, specify
982
File: acl2-doc-emacs.info, Node: DEFCHOOSE, Next: DEFCONG, Prev: DEFAXIOM, Up: EVENTS
984
DEFCHOOSE define a Skolem (witnessing) function
987
(defchoose choose-x-for-p-and-q (x) (y z)
991
(defchoose choose-x-for-p-and-q x (y z) ; equivalent to the above
995
; The following is as above, but strengthens the axiom added to pick a sort
996
; of canonical witness, as described below.
997
(defchoose choose-x-for-p-and-q x (y z)
1002
(defchoose choose-x-and-y-for-p-and-q (x y) (z)
339
* HIDDEN-DEATH-PACKAGE:: handling defpkg events that are local
341
* HIDDEN-DEFPKG:: handling defpkg events that are local
345
(defpkg "name" term doc-string)
348
where "name" is a non-empty string consisting of standard characters
349
(see *Note STANDARD-CHAR-P::), none of which is lower case, that names
350
the package to be created; term is a variable-free expression that
351
evaluates to a list of symbols, where no two distinct symbols in the
352
list may have the same symbol-name, to be imported into the newly
353
created package; and doc-string is an optional documentation string; see
354
*Note DOC-STRING::. The name of the new package must be "new": the host
355
lisp must not contain any package of that name. There are two
356
exceptions to this newness rule, discussed at the end of this
359
(There is actually an additional argument, book-path, that is used for
360
error reporting but has no logical content. Users should generally
361
ignore this argument, as well as the rest of this sentence: a book-path
362
will be specified for defpkg events added by ACL2 to the portcullis of a
363
book's certificate; see *Note HIDDEN-DEATH-PACKAGE::.)
365
Defpkg forms can be entered at the top-level of the ACL2 command loop.
366
They should not occur in books (see *Note CERTIFY-BOOK::).
368
After a successful defpkg it is possible to "intern" a string into the
369
package using intern-in-package-of-symbol. The result is a symbol that
370
is in the indicated package, provided the imports allow it. For
371
example, suppose 'my-pkg::abc is a symbol whose symbol-package-name is
372
"MY-PKG". Suppose further that the imports specified in the defpkg for
373
"MY-PKG" do not include a symbol whose symbol-name is "XYZ". Then
375
(intern-in-package-of-symbol "XYZ" 'my-pkg::abc)
377
returns a symbol whose symbol-name is "XYZ" and whose
378
symbol-package-name is "MY-PKG". On the other hand, if the imports to
379
the defpkg does include a symbol with the name "XYZ", say in the package
382
(intern-in-package-of-symbol "XYZ" 'my-pkg::abc)
384
returns that symbol (which is uniquely determined by the restriction on
385
the imports list above). See *Note INTERN-IN-PACKAGE-OF-SYMBOL::.
387
Defpkg is the only means by which an ACL2 user can create a new package
388
or specify what it imports. That is, ACL2 does not support the Common
389
Lisp functions make-package or import. Currently, ACL2 does not support
392
The Common Lisp function intern is weakly supported by ACL2. See *Note
395
We now explain the two exceptions to the newness rule for package names.
396
The careful experimenter will note that if a package is created with a
397
defpkg that is subsequently undone, the host lisp system will contain
398
the created package even after the undo. Because ACL2 hangs onto worlds
399
after they have been undone, e.g., to implement :oops but, more
400
importantly, to implement error recovery, we cannot actually destroy a
401
package upon undoing it. Thus, the first exception to the newness rule
402
is that name is allowed to be the name of an existing package if that
403
package was created by an undone defpkg and the newly proposed set of
404
imports is identical to the old one. See *Note
405
PACKAGE-REINCARNATION-IMPORT-RESTRICTIONS::. This exception does not
406
violate the spirit of the newness rule, since one is disinclined to
407
believe in the existence of undone packages. The second exception is
408
that name is allowed to be the name of an existing package if the
409
package was created by a defpkg with identical set of imports. That is,
410
it is permissible to execute "redundant" defpkg commands. The
411
redundancy test is based on the values of the two import forms
412
(comparing them after sorting and removing duplicates), not on the forms
415
Finally, we explain why we require the package name to contain standard
416
characters, none of which is lower case. We have seen at least one
417
implementation that handled lower-case package names incorrectly. Since
418
we see no need for lower-case characters in package names, which can
419
lead to confusion anyhow (note for example that foo::bar is a symbol
420
whose symbol-package-name is "FOO", not "foo"), we simply disallow them.
421
Since the notion of "lower case" is only well-specified in Common Lisp
422
for standard characters, we restrict to these.
427
File: acl2-doc-emacs.info, Node: HIDDEN-DEATH-PACKAGE, Next: HIDDEN-DEFPKG, Prev: DEFPKG, Up: DEFPKG
429
HIDDEN-DEATH-PACKAGE handling defpkg events that are local
431
This documentation topic explains a little bit about certain errors
432
users may see when attempting to evaluate a defpkg event. In brief, if
433
you see an error that refers you to this topic, you are probably trying
434
to admit a defpkg event, and you should change the name of the package
435
to be introduced by that event.
437
Recall that defpkg events introduce axioms, for example as follows.
439
ACL2 !>(defpkg "PKG0" '(a b))
442
Form: ( DEFPKG "PKG0" ...)
445
Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
449
Rune: (:REWRITE PKG0-PACKAGE)
451
Lhs: (SYMBOL-PACKAGE-NAME (INTERN-IN-PACKAGE-OF-SYMBOL X Y))
453
Hyps: (AND (STRINGP X)
454
(NOT (MEMBER-SYMBOL-NAME X '(A B)))
456
(EQUAL (SYMBOL-PACKAGE-NAME Y) "PKG0"))
458
Backchain-limit-lst: NIL
463
Now, a defpkg event may be executed underneath an encapsulate or
464
include-book form that is marked local. In that case, traces of the
465
added axiom will disappear after the surrounding encapsulate or
466
include-book form is admitted. This can cause inconsistencies. (You
467
can take our word for it, or you can look at the example shown in the
468
"Essay on Hidden Packages" in source file axioms.lisp.)
470
In order to prevent unsoundness, then, ACL2 maintains the following
471
invariant. Let us say that a defpkg event is "hidden" if it is in
472
support of the current logical world but is not present in that world as
473
an event, because it is local as indicated above. We maintain the
474
invariant that all defpkg events, even if "hidden", are tracked
475
under-the-hood in the current logical world. Sometimes this property
476
causes defpkg events to be written to the portcullis of a book's
477
certificate (see *Note BOOKS::). At any rate, if you then try to define
478
the package in a manner inconsistent with the earlier such definition,
479
that is, with a different imports list, you will see an error because of
480
the above-mentioned tracking.
482
(By the way, this topic's name comes from Holly Bell, who heard "hidden
483
death package" instead of "hidden defpkg". The description seemed to
491
File: acl2-doc-emacs.info, Node: HIDDEN-DEFPKG, Prev: HIDDEN-DEATH-PACKAGE, Up: DEFPKG
493
HIDDEN-DEFPKG handling defpkg events that are local
495
See *Note HIDDEN-DEATH-PACKAGE::
502
File: acl2-doc-emacs.info, Node: DEFREFINEMENT, Next: DEFSTOBJ, Prev: DEFPKG, Up: EVENTS
504
DEFREFINEMENT prove that equiv1 refines equiv2
508
(defrefinement equiv1 equiv2)
510
is an abbreviation for
511
(defthm equiv1-refines-equiv2
512
(implies (equiv1 x y) (equiv2 x y))
513
:rule-classes (:refinement))
515
See *Note REFINEMENT::.
519
(defrefinement equiv1 equiv2
520
:rule-classes rule-classes
521
:instructions instructions
524
:event-name event-name
527
where equiv1 and equiv2 are known equivalence relations, event-name, if
528
supplied, is a symbol and all other arguments are as specified in the
529
documentation for defthm. The defrefinement macro expands into a call
530
of defthm. The name supplied is equiv1-refines-equiv2, unless
531
event-name is supplied, in which case it is used as the name. The term
532
supplied states that equiv1 refines equiv2. The rule-class :refinement
533
is added to the rule-classes specified, if it is not already there. All
534
other arguments to the generated defthm form are as specified by the
535
other keyword arguments above.
540
File: acl2-doc-emacs.info, Node: DEFSTOBJ, Next: DEFSTUB, Prev: DEFREFINEMENT, Up: EVENTS
542
DEFSTOBJ define a new single-threaded object
547
(reg :type (array (unsigned-byte 31) (8))
549
(p-c :type (unsigned-byte 31)
551
halt ; = (halt :type t :initially nil)
552
(mem :type (array (unsigned-byte 31) (64))
553
:initially 0 :resizable t))
557
(field1 :type type1 :initially val1 :resizable b1)
559
(fieldk :type typek :initially valk :resizable bk)
564
where name is a new symbol, each fieldi is a symbol, each typei is
565
either a type-spec or (ARRAY type-spec (max)), each vali is an object
566
satisfying typei, and each bi is t or nil. Each pair :initially vali
567
and :resizable bi may be omitted; more on this below. The alist
568
argument is optional and allows the user to override the default
569
function names introduced by this event. The doc-string is also
570
optional. The inline-flag Boolean argument is also optional and
571
declares to ACL2 that the generated access and update functions for the
572
stobj should be implemented as macros under the hood (which has the
573
effect of inlining the function calls). We describe further
574
restrictions on the fieldi, typei, vali, and on alist below. We
575
recommend that you read about single-threaded objects (stobjs) in ACL2
576
before proceeding; see *Note STOBJ::.
578
The effect of this event is to introduce a new single-threaded object
579
(i.e., a "stobj"), named name, and the associated recognizers, creator,
580
accessors, updaters, constants, and, for fields of ARRAY type, length
581
and resize functions.
584
*The Single-Threaded Object Introduced*
586
The defstobj event effectively introduces a new global variable, named
587
name, which has as its initial logical value a list of k elements, where
588
k is the number of "field descriptors" provided. The elements are
589
listed in the same order in which the field descriptors appear. If the
590
:type of a field is (ARRAY type-spec (max)) then the corresponding
591
element of the stobj is initially a list of length max containing the
592
value, val, specified by :initially val. Otherwise, the :type of the
593
field is a type-spec and the corresponding element of the stobj is the
594
specified initial value val. (The actual representation of the stobj in
595
the underlying Lisp may be quite different; see *Note STOBJ-EXAMPLE-2::.
596
For the moment we focus entirely on the logical aspects of the object.)
598
In addition, the defstobj event introduces functions for recognizing and
599
creating the stobj and for recognizing, accessing, and updating its
600
fields. For fields of ARRAY type, length and resize functions are also
601
introduced. Constants are introduced that correspond to the accessor
604
*Restrictions on the Field Descriptions in Defstobj*
606
Each field descriptor is of the form:
608
(fieldi :TYPE typei :INITIALLY vali)
610
Note that the type and initial value are given in "keyword argument"
611
format and may be given in either order. The typei and vali "arguments"
612
are not evaluated. If omitted, the type defaults to t (unrestricted)
613
and the initial value defaults to nil.
615
Each typei must be either a type-spec or else a list of the form (ARRAY
616
type-spec (max)). The latter forms are said to be "array types."
617
Examples of legal typei are:
621
(ARRAY (SIGNED-BYTE 31) (16))
624
The typei describes the objects which are expected to occupy the given
625
field. Those objects in fieldi should satisfy typei. We are more
626
precise below about what we mean by "expected." We first present the
627
restrictions on typei and vali.
631
When typei is a type-spec it restricts the contents,
632
x, of fieldi according to the "meaning" formula given in
633
the table for type-spec. For example, the first typei
634
above restricts the field to be an integer between 0 and 31,
635
inclusive. The second restricts the field to be an integer between
636
-2^30 and (2^30)-1, inclusive.
638
The initial value, vali, of a field description may be any ACL2 object
639
but must satisfy typei. Note that vali is not a form to be evaluated
640
but an object. A form that evaluates to vali could be written 'vali,
641
but defstobj does not expect you to write the quote mark. For example,
642
the field description
644
(days-off :initially (saturday sunday))
646
describes a field named days-off whose initial value is the list
647
consisting of the two symbols SATURDAY and SUNDAY. In particular, the
648
initial value is NOT obtained by applying the function saturday to the
649
variable sunday! Had we written
651
(days-off :initially '(saturday sunday))
653
it would be equivalent to writing
655
(days-off :initially (quote (saturday sunday)))
657
which would initialize the field to a list of length two, whose first
658
element is the symbol quote and whose second element is a list
659
containing the symbols saturday and sunday.
663
When typei is of the form (ARRAY type-spec (max)), the field is supposed
664
to be a list of items, initially of length max, each of which satisfies
665
the indicated type-spec. Max must be a non-negative integer less than
666
(2^28)-1. We discuss this limitation below. Thus,
668
(ARRAY (SIGNED-BYTE 31) (16))
670
restricts the field to be a list of integers, initially of length 16,
671
where each integer in the list is a (SIGNED-BYTE 31). We sometimes call
672
such a list an "array" (because it is represented as an array in the
673
underlying Common Lisp). The elements of an array field are indexed by
674
position, starting at 0. Thus, the maximum legal index of an array
677
Note that the ARRAY type requires that the max be enclosed in
678
parentheses. This makes ACL2's notation consistent with the Common Lisp
679
convention of describing the (multi-)dimensionality of arrays. But ACL2
680
currently supports only single dimensional arrays in stobjs.
682
For array fields, the initial value vali must be an object satisfying
683
the type-spec of the ARRAY description. The initial value of the field
684
is a list of max repetitions of vali.
686
Array fields can be "resized," that is, their lengths can be changed, if
687
:resizable t is supplied as shown in the example and General Form above.
688
The new length must satisfy the same restriction as does max, as
689
described above. Each array field in a defstobj event gives rise to a
690
length function, which gives the length of the field, and a resize
691
function, which modifies the length of the field if :resizable t was
692
supplied with the field when the defstobj was introduced and otherwise
695
Array resizing is relatively slow, so we recommend using it somewhat
698
*The Default Function Names*
703
(field1 :type type1 :initially val1)
705
(fieldk :type typek :initially valk)
710
name must be a new symbol, each fieldi must be a symbol, each typei must
711
be a type-spec or (ARRAY type-spec (max)), and each vali must be an
712
object satisfying typei.
714
Roughly speaking, for each fieldi, a defstobj introduces a recognizer
715
function, an accessor function, and an updater function. The accessor
716
function, for example, takes the stobj and returns the indicated
717
component; the updater takes a new component value and the stobj and
718
return a new stobj with the component replaced by the new value. But
719
that summary is inaccurate for array fields.
721
The accessor function for an array field does not take the stobj and
722
return the indicated component array, which is a list of length max.
723
Instead, it takes an additional index argument and returns the indicated
724
element of the array component. Similarly, the updater function for an
725
array field takes an index, a new value, and the stobj, and returns a
726
new stobj with the indicated element replaced by the new value.
728
These functions -- the recognizer, accessor, and updater, and also
729
length and resize functions in the case of array fields -- have "default
730
names." The default names depend on the field name, fieldi, and on
731
whether the field is an array field or not. For clarity, suppose fieldi
732
is named c. The default names are shown below in calls, which also
733
indicate the arities of the functions. In the expressions, we use x as
734
the object to be recognized by field recognizers, i as an array index, v
735
as the "new value" to be installed by an updater, and name as the
736
single-threaded object.
739
non-array field array field
740
recognizer (cP x) (cP x)
741
accessor (c name) (cI i name)
742
updater (UPDATE-c v name) (UPDATE-cI i v name)
743
length (c-LENGTH name)
744
resize (RESIZE-c k name)
747
Finally, a recognizer and a creator for the entire single-threaded
748
object are introduced. The creator returns the initial stobj, but may
749
only be used in limited contexts; see *Note WITH-LOCAL-STOBJ::. If the
750
single-threaded object is named name, then the default names and arities
753
top recognizer (nameP x)
754
creator (CREATE-name)
757
For example, the event
760
(X :TYPE INTEGER :INITIALLY 0)
761
(A :TYPE (ARRAY (INTEGER 0 9) (3)) :INITIALLY 9))
763
introduces a stobj named $S. The stobj has two fields, X and A. The A
764
field is an array. The X field contains an integer and is initially 0.
765
The A field contains a list of integers, each between 0 and 9,
766
inclusively. Initially, each of the three elements of the A field is 9.
768
This event introduces the following sequence of definitions:
770
(DEFUN XP (X) ...) ; recognizer for X field
771
(DEFUN AP (X) ...) ; recognizer of A field
772
(DEFUN $SP ($S) ...) ; top-level recognizer for stobj $S
773
(DEFUN CREATE-$S () ...) ; creator for stobj $S
774
(DEFUN X ($S) ...) ; accessor for X field
775
(DEFUN UPDATE-X (V $S) ...) ; updater for X field
776
(DEFUN A-LENGTH ($S) ...) ; length of A field
777
(DEFUN RESIZE-A (K $S) ...) ; resizer for A field
778
(DEFUN AI (I $S) ...) ; accessor for A field at index I
779
(DEFUN UPDATE-AI (I V $S) ...) ; updater for A field at index I
782
*Avoiding the Default Function Names*
784
If you do not like the default names listed above you may use the
785
optional :renaming alist to substitute names of your own choosing. Each
786
element of alist should be of the form (fn1 fn2), where fn1 is a default
787
name and fn2 is your choice for that name.
792
(X :TYPE INTEGER :INITIALLY 0)
793
(A :TYPE (ARRAY (INTEGER 0 9) (3)) :INITIALLY 9)
794
:renaming ((X XACCESSOR) (CREATE-$S MAKE$S)))
796
introduces the following definitions
798
(DEFUN XP (X) ...) ; recognizer for X field
799
(DEFUN AP (X) ...) ; recognizer of A field
800
(DEFUN $SP ($S) ...) ; top-level recognizer for stobj $S
801
(DEFUN MAKE$S () ...) ; creator for stobj $S
802
(DEFUN XACCESSOR ($S) ...) ; accessor for X field
803
(DEFUN UPDATE-X (V $S) ...) ; updater for X field
804
(DEFUN A-LENGTH ($S) ...) ; length of A field
805
(DEFUN RESIZE-A (K $S) ...) ; resizer for A field
806
(DEFUN AI (I $S) ...) ; accessor for A field at index I
807
(DEFUN UPDATE-AI (I V $S) ...) ; updater for A field at index I
809
Note that even though the renaming alist substitutes "XACCESSOR" for "X"
810
the updater for the X field is still called "UPDATE-X." That is because
811
the renaming is applied to the default function names, not to the field
812
descriptors in the event.
814
Use of the :renaming alist may be necessary to avoid name clashes
815
between the default names and and pre-existing function symbols.
819
Defstobj events also introduce constant definitions (see *Note
820
DEFCONST::). One constant is introduced for each accessor function by
821
prefixing and suffixing a `*' character on the function name. The value
822
of that constant is the position of the field being accessed. For
823
example, if the accessor functions are a, b, and c, in that order, then
824
the following constant definitions are introduced.
830
These constants are used for certain calls of nth and update-nth that
831
are displayed to the user in proof output. For example, for stobj st
832
with accessor functions a, b, and c, in that order, the term (nth '2 st)
833
would be printed during a proof as (nth *c* st). Also see *Note TERM::,
834
in particular the discussion there of untranslated terms, and see *Note
837
*Inspecting the Effects of a Defstobj*
839
Because the stobj functions are introduced as "sub-events" of the
840
defstobj the history commands :pe and :pc will not print the definitions
841
of these functions but will print the superior defstobj event. To see
842
the definitions of these functions use the history command :pcb!.
844
To see an s-expression containing the definitions what constitute the
845
raw Lisp implementation of the event, evaluate the form
847
(nth 4 (global-val 'cltl-command (w state)))
849
*immediately after* the defstobj event has been processed.
851
A defstobj is considered redundant only if the name, field descriptors,
852
renaming alist, and inline flag are identical to a previously executed
855
*Inlining and Performance*
857
The :inline keyword argument controls whether or not accessor, updater,
858
and length functions are inlined (as macros under the hood, in raw
859
Lisp). If :inline t is provided then these are inlined; otherwise they
860
are not. The advantage of inlining is potentially better performance;
861
there have been contrived examples, doing essentially nothing except
862
accessing and updating array fields, where inlining reduced the time by
863
a factor of 10 or more; and inlining has sped up realistic examples by a
864
factor of at least 2. Inlining may get within a factor of 2 of C
865
execution times for such contrived examples, and within a few percent of
866
C execution times on realistic examples.
868
A drawback to inlining is that redefinition may not work as expected,
869
much as redefinition may not work as expected for macros: defined
870
functions that call a macro, or inlined stobj function, will not see a
871
subsequent redefinition of the macro or inlined function. Another
872
drawback to inlining is that because inlined functions are implemented
873
as macros in raw Lisp, tracing (see *Note TRACE$::) will not show their
874
calls. These drawbacks are avoided by default, but the user who is not
875
concerned about them is advised to specify :inline t.
880
File: acl2-doc-emacs.info, Node: DEFSTUB, Next: DEFTHEORY, Prev: DEFSTOBJ, Up: EVENTS
882
DEFSTUB stub-out a function symbol
886
ACL2 !>(defstub subr1 (* * state) => (mv * state))
887
ACL2 !>(defstub add-hash (* * hash-table) => hash-table)
890
(defstub name args-sig => output-sig)
891
(defstub name args-sig => output-sig :doc doc-string)
894
Name is a new function symbol and (name . args-sig) => output-sig) is a
895
signature. If the optional doc-string is supplied it should be a
896
documentation string. See also the "Old Style" heading below.
898
Defstub macro expands into an encapsulate event (see *Note
899
ENCAPSULATE::). Thus, no axioms are available about name but it may be
900
used wherever a function of the given signature is permitted.
904
Old Style General Form:
905
(defstub name formals output)
906
(defstub name formals output :doc doc-string)
908
where name is a new function symbol, formals is its list of formal
909
parameters, and output is either a symbol (indicating that the function
910
returns one result) or a term of the form (mv s1 ... sn), where each si
911
is a symbol (indicating that the function returns n results). Whether
912
and where the symbol state occurs in formals and output indicates how
913
the function handles state. It should be the case that (name formals
914
output) is in fact a signature (see *Note SIGNATURE::).
916
Note that with the old style notation it is impossible to stub-out a
917
function that uses any single-threaded object other than state. The old
918
style is preserved for compatibility with earlier versions of ACL2.
923
File: acl2-doc-emacs.info, Node: DEFTHEORY, Next: DEFTHM, Prev: DEFSTUB, Up: EVENTS
925
DEFTHEORY define a theory (to enable or disable a set of rules)
929
(deftheory interp-theory
930
(set-difference-theories
931
(universal-theory :here)
932
(universal-theory 'interp-section)))
935
(deftheory name term :doc doc-string)
937
where name is a new symbolic name (see *Note NAME::), term is a term
938
that when evaluated will produce a theory (see *Note THEORIES::), and
939
doc-string is an optional documentation string (see *Note DOC-STRING::).
940
Except for the variable world, term must contain no free variables.
941
Term is evaluated with world bound to the current world (see *Note
942
WORLD::) and the resulting theory is then converted to a *runic theory*
943
(see *Note THEORIES::) and associated with name. Henceforth, this runic
944
theory is returned as the value of the theory expression (theory name).
946
The value returned is the length of the resulting theory. For example,
947
in the following, the theory associated with 'FOO has 54 runes:
949
ACL2 !>(deftheory foo (union-theories '(binary-append)
950
(theory 'minimal-theory)))
953
Form: ( DEFTHEORY FOO ...)
956
Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
964
File: acl2-doc-emacs.info, Node: DEFTHM, Next: DEFTHMD, Prev: DEFTHEORY, Up: EVENTS
966
DEFTHM prove and name a theorem
971
(equal (app (app a b) c)
974
The following nonsensical example illustrates all the optional arguments
975
but is illegal because not all combinations are permitted. See *Note
976
HINTS:: for a complete list of hints.
979
(implies (hyps x y z) (concl x y z))
980
:rule-classes (:REWRITE :GENERALIZE)
981
:instructions (induct prove promote (dive 1) x
982
(dive 2) = top (drop 2) prove)
984
:do-not '(generalize fertilize)
985
:in-theory (set-difference-theories
986
(current-theory :here)
988
:induct (and (nth n a) (nth n b))
989
:use ((:instance assoc-of-append
991
(:functional-instance
992
(:instance p-f (x a) (y b))
996
:doc "#0[one-liner/example/details]")
1000
:rule-classes rule-classes
1001
:instructions instructions
1006
where name is a new symbolic name (see *Note NAME::), term is a term
1007
alleged to be a theorem, and rule-classes, instructions, hints, otf-flg
1008
and doc-string are as described in their respective documentation. The
1009
five keyword arguments above are all optional, however you may not
1010
supply both :instructions and :hints, since one drives the proof checker
1011
and the other drives the theorem prover. If :rule-classes is not
1012
specified, the list (:rewrite) is used; if you wish the theorem to
1013
generate no rules, specify :rule-classes nil.
1015
When ACL2 processes a defthm event, it first tries to prove the term
1016
using the indicated hints (see *Note HINTS::) or instructions (see *Note
1017
PROOF-CHECKER::). If it is successful, it stores the rules described by
1018
the rule-classes (see *Note RULE-CLASSES::), proving the necessary
1024
File: acl2-doc-emacs.info, Node: DEFTHMD, Next: DEFUN, Prev: DEFTHM, Up: EVENTS
1026
DEFTHMD prove and name a theorem and then disable it
1028
Use defthmd instead of defthm when you want to disable a theorem
1029
immediately after proving it. This macro has been provided for users
1030
who prefer working in a mode where theorems are only enabled when
1031
explicitly directed by :in-theory. Specifically, the form
1033
(defthmd NAME TERM ...)
1038
(defthmd NAME TERM ...)
1041
(in-theory (disable NAME)))
1045
Note that defthmd commands are never redundant (see *Note
1046
REDUNDANT-EVENTS::). Even if the defthm event is redundant, then the
1047
in-theory event will still be executed.
1049
The summary for the in-theory event is suppressed. See *Note DEFTHM::
1050
for documentation of defthm.
1055
File: acl2-doc-emacs.info, Node: DEFUN, Next: DEFUN-SK, Prev: DEFTHMD, Up: EVENTS
1057
DEFUN define a function symbol
1063
(cons (car x) (app (cdr x) y))
1067
(declare (xargs :guard (and (integerp n)
1071
(* n (fact (1- n)))))
1074
(defun fn (var1 ... varn) doc-string dcl ... dcl body),
1008
* CONSERVATIVITY-OF-DEFCHOOSE:: proof of conservativity of defchoose
1012
(bound-var1 ... bound-varn)
1013
(free-var1 ... free-vark)
1076
1018
where fn is the symbol you wish to define and is a new symbolic name
1077
(see *Note NAME::), (var1 ... varn) is its list of formal parameters
1078
(see *Note NAME::), and body is its body. The definitional axiom is
1079
logically admissible provided certain restrictions are met. These are
1082
Note that ACL2 does not support the use of lambda-list keywords (such as
1083
&optional) in the formals list of functions. We do support some such
1084
keywords in macros and often you can achieve the desired syntax by
1085
defining a macro in addition to the general version of your function.
1086
See *Note DEFMACRO::. The documentation string, doc-string, is
1087
optional; for a description of its form, see *Note DOC-STRING::.
1089
The *declarations* (see *Note DECLARE::), dcl, are also optional. If
1090
more than one dcl form appears, they are effectively grouped together as
1091
one. Perhaps the most commonly used ACL2 specific declaration is of the
1092
form (declare (xargs :guard g :measure m)). This declaration in the
1093
defun of some function fn has the effect of making the "guard" for fn be
1094
the term g and the "measure" be the term m. The notion of "measure" is
1095
crucial to ACL2's definitional principle. The notion of "guard" is not,
1096
and is discussed elsewhere; see *Note VERIFY-GUARDS:: and see *Note
1097
SET-VERIFY-GUARDS-EAGERNESS::.
1099
We now briefly discuss the ACL2 definitional principle, using the
1100
following definition form which is offered as a more or less generic
1104
(declare (xargs :guard (g x y)
1108
(step (fn (d x) y))))
1110
Note that in our generic example, fn has just two arguments, x and y,
1111
the guard and measure terms involve both of them, and the body is a
1112
simple case split on (test x y) leading to a "non-recursive" branch,
1113
(stop x y), and a "recursive" branch. In the recursive branch, fn is
1114
called after "decrementing" x to (d x) and some step function is applied
1115
to the result. Of course, this generic example is quite specific in
1116
form but is intended to illustrate the more general case.
1118
Provided this definition is admissible under the logic, as outlined
1119
below, it adds the following axiom to the logic.
1126
(step (fn (d x) y)))
1128
Note that the guard of fn has no bearing on this logical axiom.
1130
This defining axiom is actually implemented in the ACL2 system by a
1131
:definition rule, namely
1136
(step (fn (d a) b)))).
1138
See *Note DEFINITION:: for a discussion of how definition rules are
1139
applied. Roughly speaking, the rule causes certain instances of (fn x
1140
y) to be replaced by the corresponding instances of the body above.
1141
This is called "opening up" (fn x y). The instances of (fn x y) opened
1142
are chosen primarily by heuristics which determine that the recursive
1143
calls of fn in the opened body (after simplification) are more desirable
1144
than the unopened call of fn.
1146
This discussion has assumed that the definition of fn was admissible.
1147
Exactly what does that mean? First, fn must be a previously
1148
unaxiomatized function symbol (however, see *Note
1149
LD-REDEFINITION-ACTION::). Second, the formal parameters must be
1150
distinct variable names. Third, the guard, measure, and body should all
1151
be terms and should mention no free variables except the formal
1152
parameters. Thus, for example, body may not contain references to
1153
"global" or "special" variables; ACL2 constants or additional formals
1154
should be used instead.
1156
The final conditions on admissibility concern the termination of the
1157
recursion. Roughly put, all applications of fn must terminate. In
1158
particular, there must exist a binary relation, rel, and some unary
1159
predicate mp such that rel is well-founded on objects satisfying mp, the
1160
measure term m must always produce something satisfying mp, and the
1161
measure term must decrease according to rel in each recursive call,
1162
under the hypothesis that all the tests governing the call are
1163
satisfied. By the meaning of well-foundedness, we know there are no
1164
infinitely descending chains of successively rel-smaller mp-objects.
1165
Thus, the recursion must terminate.
1167
The only primitive well-founded relation in ACL2 is o< (see *Note O<::),
1168
which is known to be well-founded on the o-ps (see *Note O-P::). For
1169
the proof of well-foundedness, see *Note PROOF-OF-WELL-FOUNDEDNESS::.
1170
However it is possible to add new well-founded relations. For details,
1171
see *Note WELL-FOUNDED-RELATION::. We discuss later how to specify
1172
which well-founded relation is selected by defun and in the present
1173
discussion we assume, without loss of generality, that it is o< on the
1176
For example, for our generic definition of fn above, with measure term
1177
(m x y), two theorems must be proved. The first establishes that m
1178
produces an ordinal:
1182
The second shows that m decreases in the (only) recursive call of fn:
1184
(implies (not (test x y))
1185
(o< (m (d x) y) (m x y))).
1187
Observe that in the latter formula we must show that the "m-size" of (d
1188
x) and y is "smaller than" the m-size of x and y, provided the test,
1189
(test x y), in the body fails, thus leading to the recursive call (fn (d
1192
See *Note O<:: for a discussion of this notion of "smaller than." It
1193
should be noted that the most commonly used ordinals are the natural
1194
numbers and that on natural numbers, o< is just the familiar "less than"
1195
relation (<). Thus, it is very common to use a measure m that returns a
1196
nonnegative integer, for then (o-p (m x y)) becomes a simple conjecture
1197
about the type of m and the second formula above becomes a conjecture
1198
about the less-than relationship of nonnegative integer arithmetic.
1200
The most commonly used measure function is acl2-count, which computes a
1201
nonnegative integer size for all ACL2 objects. See *Note ACL2-COUNT::.
1203
Probably the most common recursive scheme in Lisp programming is when
1204
some formal is supposed to be a list and in the recursive call it is
1205
replaced by its cdr. For example, (test x y) might be simply (atom x)
1206
and (d x) might be (cdr x). In that case, (acl2-count x) is a suitable
1207
measure because the acl2-count of a cons is strictly larger than the
1208
acl2-counts of its car and cdr. Thus, "recursion by car" and "recursion
1209
by cdr" are trivially admitted if acl2-count is used as the measure and
1210
the definition protects every recursive call by a test insuring that the
1211
decremented argument is a consp. Similarly, "recursion by 1-" in which
1212
a positive integer formal is decremented by one in recursion, is also
1213
trivially admissible. See *Note BUILT-IN-CLAUSES:: to extend the class
1214
of trivially admissible recursive schemes.
1216
We now turn to the question of which well-founded relation defun uses.
1217
It should first be observed that defun must actually select both a
1218
relation (e.g., o<) and a domain predicate (e.g., o-p) on which that
1219
relation is known to be well-founded. But, as noted elsewhere (see
1220
*Note WELL-FOUNDED-RELATION::), every known well-founded relation has a
1221
unique domain predicate associated with it and so it suffices to
1222
identify simply the relation here.
1224
The xargs field of a declare permits the explicit specification of any
1225
known well-founded relation with the keyword :well-founded-relation. An
1226
example is given below. If the xargs for a defun specifies a
1227
well-founded relation, that relation and its associated domain predicate
1228
are used in generating the termination conditions for the definition.
1230
If no :well-founded-relation is specified, defun uses the
1231
:well-founded-relation specified in the acl2-defaults-table. See *Note
1232
SET-WELL-FOUNDED-RELATION:: to see how to set the default well-founded
1233
relation (and, implicitly, its domain predicate). The initial default
1234
well-founded relation is o< (with domain predicate o-p).
1236
This completes the brief sketch of the ACL2 definitional principle.
1238
On very rare occasions ACL2 will seem to "hang" when processing a
1239
definition, especially if there are many subexpressions of the body
1240
whose function symbol is if (or which macroexpand to such an
1241
expression). In those cases you may wish to supply the following to
1242
xargs: :normalize nil. This is an advanced feature that turns off
1243
ACL2's usual propagation upward of if tests.
1245
The following example illustrates all of the available declarations, but
1246
is completely nonsensical. For documentation, see *Note XARGS:: and see
1249
(defun example (x y z a b c i j)
1250
(declare (ignore a b c)
1252
(xargs :guard (symbolp x)
1254
:well-founded-relation my-wfr
1257
:do-not '(generalize fertilize)
1258
:expand ((assoc x a) (member y z))
1259
:restrict ((<-trans ((x x) (y (foo x)))))
1260
:hands-off (length binary-append)
1261
:in-theory (set-difference-theories
1262
(current-theory :here)
1264
:induct (and (nth n a) (nth n b))
1266
:use ((:instance assoc-of-append
1268
(:functional-instance
1269
(:instance p-f (x a) (y b))
1272
:guard-hints (("Subgoal *1/3'"
1273
:use ((:instance assoc-of-append
1274
(x a) (y b) (z c)))))
1278
(example-body x y z i j))
1019
(see *note NAME::), (bound-var1 ... bound-varn) is a list of distinct
1020
`bound' variables (see below), (free-var1 ... free-vark) is the list of
1021
formal parameters of fn and is disjoint from the bound variables, and
1022
body is a term. The use of lambda-list keywords (such as &optional) is
1023
not allowed. The documentation string argument, :doc doc-string, is
1024
optional; for a description of the form of doc-string see *note
1025
DOC-STRING::. The :strengthen keyword argument is optional; if
1026
supplied, it must be t or nil.
1028
The system treats fn very much as though it were declared in the
1029
signature of an encapsulate event, with a single axiom exported as
1030
described below. If you supply a :use hint (see *note HINTS::), :use
1031
fn, it will refer to that axiom. No rule (of class :rewrite or
1032
otherwise; see *note RULE-CLASSES::) is created for fn.
1034
Defchoose is only executed in defun-mode :logic; see *note
1035
DEFUN-MODE::. Also see *note DEFUN-SK::.
1037
In the most common case, where there is only one bound variable, it is
1038
permissible to omit the enclosing parentheses on that variable. The
1039
effect is the same whether or not those parentheses are omitted. We
1040
describe this case first, where there is only one bound variable, and
1041
then address the other case. Both cases are discussed assuming
1042
:strengthen is nil, which is the default. We deal with the case
1043
:strengthen t at the end.
1045
The effect of the form
1047
(defchoose fn bound-var (free-var1 ... free-vark)
1050
is to introduce a new function symbol, fn, with formal parameters
1051
(free-var1 ... free-vark). Now consider the following axiom, which
1052
states that fn picks a value of bound-var so that the body will be
1053
true, if such a value exists:
1056
(let ((bound-var (fn free-var1 ... free-vark)))
1059
This axiom is "clearly conservative" under the conditions expressed
1060
above: the function fn simply picks out a "witnessing" value of
1061
bound-var if there is one. For a rigorous statement and proof of this
1062
conservativity claim, see *note CONSERVATIVITY-OF-DEFCHOOSE::.
1064
Next consider the case that there is more than one bound variable, i.e.,
1065
there is more than one bound-var in the following.
1068
(bound-var1 ... bound-varn)
1069
(free-var1 ... free-vark)
1072
Then fn returns a multiple value with n componenets, and formula (1)
1073
above is expressed using mv-let as follows:
1076
(mv-let (bound-var1 ... bound-varn)
1077
(fn free-var1 ... free-vark)
1080
We now discuss the case that :strengthen t is supplied. For simplicity
1081
we return to our first example, with a single free variable, y. The
1082
idea is that if we pick the "smallest" witnessing bound-var for two
1083
different free variables y and y1, then either those two witnesses are
1084
the same, or else one is less than the other, in which case the smaller
1085
one is a witness for its free variable but not for the other. (See
1086
comments in source function defchoose-constraint-extra for more
1087
details.) Below, body1 is the result of replacing y by y1 in body.
1089
(2) (or (equal (fn y) (fn y1))
1090
(let ((bound-var (fn y)))
1093
(let ((bound-var (fn y1)))
1097
An important application of this additional axiom is to be able to
1098
define a "fixing" function that picks a canonical representative of
1099
each equivalence class, for a given equivalence relation. The
1100
following events illustrate this point.
1104
(local (defun equiv (x y) (equal x y)))
1107
(defchoose efix (x) (y)
1111
(defthm equiv-implies-equal-efix-1
1112
(implies (equiv y y1)
1113
(equal (efix y) (efix y1)))
1114
:hints (("Goal" :use efix))
1115
:rule-classes (:congruence))
1119
:hints (("Goal" :use ((:instance efix (y x))))))
1121
If there is more than one bound variable, then (2) is modified in
1122
complete analogy to (1) to use mv-let in place of let.
1124
Comment for logicians: As we point out in the documentation for
1125
defun-sk, defchoose is "appropriate," by which we mean that it is
1126
conservative, even in the presence of epsilon-0 induction. For a
1127
proof, See *Note CONSERVATIVITY-OF-DEFCHOOSE::.
added
removed
doc/EMACS/acl2-doc-emacs.info-8
