1
This is acl2-doc-emacs.info, produced by makeinfo version 4.5 from
2
acl2-doc-emacs.texinfo.
4
This is documentation for ACL2 Version 3.1
5
Copyright (C) 2006 University of Texas at Austin
7
This program is free software; you can redistribute it and/or modify
8
it under the terms of the GNU General Public License as published by
9
the Free Software Foundation; either version 2 of the License, or
10
(at your option) any later version.
12
This program is distributed in the hope that it will be useful,
13
but WITHOUT ANY WARRANTY; without even the implied warranty of
14
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
15
GNU General Public License for more details.
17
You should have received a copy of the GNU General Public License
18
along with this program; if not, write to the Free Software
19
Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA.
21
Written by: Matt Kaufmann and J Strother Moore
22
Department of Computer Sciences
23
University of Texas at Austin
24
Austin, TX 78712-1188 U.S.A.
28
* acl2: (acl2-doc-emacs.info). Applicative Common Lisp
32
File: acl2-doc-emacs.info, Node: NOTE7, Next: NOTE8, Prev: NOTE6, Up: RELEASE-NOTES
34
NOTE7 ACL2 Version 1.7 (released October 1994) Notes
36
Include-book now takes (optionally) an additional keyword argument,
37
indicating whether a compiled file is to be loaded. The default
38
behavior is unchanged, except that a warning is printed when a compiled
39
file is not loaded. See *Note INCLUDE-BOOK::.
41
A markup language for documentation strings has been implemented, and
42
many of the source files have been marked up using this language
43
(thanks largely to the efforts of Laura Lawless). See *Note MARKUP::.
44
Moreover, there are translators that we have used to provide versions
45
of the ACL2 documentation in info (for use in emacs), html (for
46
Mosaic), and tex (for hardcopy) formats.
48
A new event defdoc has been implemented. It is like deflabel, but
49
allows redefinition of doc strings and has other advantages. See *Note
52
We used to ignore corollaries when collecting up the axioms introduced
53
about constrained functions. That bug has been fixed. We thank John
54
Cowles for bringing this bug to our attention.
56
The macro defstub now allows a :doc keyword argument, so that
57
documentation may be attached to the name being introduced.
59
A new command nqthm-to-acl2 has been added to help Nqthm users to make
60
the transition to ACL2. See *Note NQTHM-TO-ACL2::, which also includes
61
a complete listing of the relevant tables.
63
Many function names, especially of the form "foo-lst", have been
64
changed in order to support the following convention, for any "foo":
66
(foo-listp lst) represents the notion (for x in lst always foop x).
68
A complete list of these changes may be found at the end of this note.
69
All of them except symbolp-listp and list-of-symbolp-listp have the
70
string "-lst" in their names. Note also that keyword-listp has been
71
renamed keyword-value-listp.
73
Accumulated persistence has been implemented. It is not connected to
74
:brr or rule monitoring. See *Note ACCUMULATED-PERSISTENCE::.
76
:Trigger-terms has been added for :linear rule classes, so you can hang
77
a linear rule under any addend you want. See *Note LINEAR::, which has
78
been improved and expanded.
80
ACL2 now accepts 256 characters and includes the Common Lisp functions
81
code-char and char-code. However, ACL2 controls the lisp reader so
82
that #\c may only be used when c is a single standard character or one
83
of Newline, Space, Page, Rubout, Tab. If you want to enter other
84
characters use code-char, e.g., (coerce (list (code-char 7) (code-char
85
240) #a) 'string). See *Note CHARACTERS::. Note: our current
86
handling of characters makes the set of theorems different under
87
Macintosh Common Lisp (MCL) than under other Common Lisps. We hope to
88
rectify this situation before the final release of ACL2.
90
A new table, macro-aliases-table, has been implemented, that associates
91
macro names with function names. So for example, since append is
92
associated with binary-append, the form (disable append) it is
93
interpreted as though it were (disable binary-append). See *Note
94
MACRO-ALIASES-TABLE::, see *note ADD-MACRO-ALIAS:: and see *note
97
The implementation of conditional metalemmas has been modified so that
98
the metafunction is applied before the hypothesis metafunction is
99
applied. See *Note META::.
101
The Common Lisp functions acons and endp have been defined in the ACL2
104
We have added the symbol declare to the list *acl2-exports*, and hence
105
to the package "ACL2-USER".
107
A new hint, :restrict, has been implemented. See *Note HINTS::.
109
It used to be that if :ubt were given a number that is greater than the
110
largest current command number, it treated that number the same as
111
:max. Now, an error is caused.
113
The table :force-table has been eliminated.
115
A command :disabledp (and macro disabledp) has been added; see *note
118
Compilation via :set-compile-fns is now suppressed during include-book.
119
In fact, whenever the state global variable ld-skip-proofsp has value
122
Here are some less important changes, additions, and so on.
124
Unlike previous releases, we have not proved all the theorems in
125
axioms.lisp; instead we have simply assumed them. We have deferred
126
such proofs because we anticipate a fairly major changed in Version 1.8
127
in how we deal with guards.
129
We used to (accidentally) prohibit the "redefinition" of a table as a
130
function. That is no longer the case.
132
The check for whether a corollary follows tautologically has been sped
133
up, at the cost of making the check less "smart" in the following
134
sense: no longer do we expand primitive functions such as implies
135
before checking this propositional implication.
137
The command ubt! has been modified so that it never causes or reports
138
an error. See *Note UBT!::.
140
ACL2 now works in Harlequin Lispworks.
142
The user can now specify the :trigger-terms for :linear rules. See
145
The name of the system is now "ACL2"; no longer is it "Acl2".
147
The raw lisp counterpart of theory-invariant is now defined to be a
148
no-op as is consistent with the idea that it is just a call of table.
150
A bug was fixed that caused proof-checker instructions to be executed
151
when ld-skip-proofsp was t.
153
The function rassoc has been added, along with a corresponding function
154
used in its guard, r-eqlable-alistp.
156
The in-theory event and hint now print a warning not only when certain
157
"primitive" :definition rules are disabled, but also when certain
158
"primitive" :executable-counterpart rules are disabled.
160
The modified version of trace provided by ACL2, for use in raw Lisp,
161
has been modified so that the lisp special variable *trace-alist* is
162
consulted. This alist associates, using eq, values with their print
163
representations. For example, initially *trace-alist* is a one-element
164
list containing the pair (cons state '|*the-live-state*|).
166
The system now prints an observation when a form is skipped because the
167
default color is :red or :pink. (Technically: when-cool has been
170
Additional protection exists when you submit a form to raw Common Lisp
171
that should only be submitted inside the ACL2 read-eval-print loop.
173
Here is a complete list of the changes in function names described near
174
the top of this note, roughly of the form
176
foo-lst --> foo-listp
178
meaning: the name "foo-lst" has been changed to "foo-listp."
180
symbolp-listp --> symbol-listp
181
list-of-symbolp-listp --> symbol-list-listp
182
{for consistency with change to symbol-listp}
183
rational-lst --> rational-listp
184
{which in fact was already defined as well}
185
integer-lst --> integer-listp
186
character-lst --> character-listp
187
stringp-lst --> string-listp
188
32-bit-integer-lst --> 32-bit-integer-listp
189
typed-io-lst --> typed-io-listp
190
open-channel-lst --> open-channel-listp
191
readable-files-lst --> readable-files-listp
192
written-file-lst --> written-file-listp
193
read-file-lst --> read-file-listp
194
writeable-file-lst --> writable-file-listp
195
{note change in spelling of ``writable''}
196
writeable-file-lst1 --> writable-file-listp1
197
pseudo-termp-lst --> pseudo-term-listp
198
hot-termp-lst --> hot-term-listp {by analogy with pseudo-term-listp}
199
weak-termp-lst --> weak-term-listp
200
weak-termp-lst-lst --> weak-termp-list-listp
201
ts-builder-case-lstp -> ts-builder-case-listp
202
quotep-lst --> quote-listp
203
termp-lst --> term-listp
204
instr-lst --> instr-listp
205
spliced-instr-lst --> spliced-instr-listp
206
rewrite-fncallp-lst --> rewrite-fncallp-listp
207
every-occurrence-equiv-hittablep1-lst -->
208
every-occurrence-equiv-hittablep1-listp
209
some-occurrence-equiv-hittablep1-lst -->
210
some-occurrence-equiv-hittablep1-listp
211
{by analogy with the preceding, even though it's a
212
``some'' instead of ``all'' predicate]
213
almost-quotep1-lst --> almost-quotep1-listp
214
ffnnames-subsetp-lst --> ffnnames-subsetp-listp
215
boolean-lstp --> boolean-listp
216
subst-expr1-lst-okp --> subst-expr1-ok-listp
219
File: acl2-doc-emacs.info, Node: NOTE8, Next: NOTE8-UPDATE, Prev: NOTE7, Up: RELEASE-NOTES
221
NOTE8 ACL2 Version 1.8 (May, 1995) Notes
223
See *Note NOTE8-UPDATE:: for yet more recent changes.
225
Guards have been eliminated from the ACL2 logic. A summary is
226
contained in this brief note. Also see *note DEFUN-MODE:: and see
227
*note SET-GUARD-CHECKING::.
229
Guards may be included in defuns as usual but are ignored from the
230
perspective of admission to the logic: functions must terminate on all
233
As in Nqthm, primitive functions, e.g., + and car, logically default
234
unexpected arguments to convenient values. Thus, (+ 'abc 3) is 3 and
235
(car 'abc) is nil. See *Note PROGRAMMING::, and see the documentation
236
for the individual primitive functions.
238
In contrast to earlier versions of ACL2, Version 1.8 logical functions
239
are executed at Nqthm speeds even when guards have not been verified.
240
In versions before 1.8, such functions were interpreted by ACL2.
242
Colors have been eliminated. Two "defun-modes" are supported, :program
243
and :logic. Roughly speaking, :program does what :red used to do,
244
namely, allow you to prototype functions for execution without any
245
proof burdens. :Logic mode does what :blue used to do, namely, allow
246
you to add a new definitional axiom to the logic. A global
247
default-defun-mode is comparable to the old default color. The system
248
comes up in :logic mode. To change the global defun-mode, type
249
:program or :logic at the top-level. To specify the defun-mode of a
252
(declare (xargs :mode mode)).
254
The prompt has changed. The initial prompt, indicating :logic mode, is
258
If you change to :program mode the prompt becomes
262
Guards can be seen as having either of two roles: (a) they are a
263
specification device allowing you to characterize the kinds of inputs a
264
function "should" have, or (b) they are an efficiency device allowing
265
logically defined functions to be executed directly in Common Lisp. If
266
a guard is specified, as with xargs :guard, then it is "verified" at
267
defun-time (unless you also specify xargs :verify-guards nil). Guard
268
verification means what it always has: the input guard is shown to
269
imply the guards on all subroutines in the body. If the guards of a
270
function are verified, then a call of the function on inputs satisfying
271
the guard can be computed directly by Common Lisp. Thus, verifying the
272
guards on your functions will allow them to execute more efficiently.
273
But it does not affect their logical behavior and since you will
274
automatically get Nqthm speeds on unverified logical definitions, most
275
users will probably use guards either as a specification device or only
276
use them when execution efficiency is extremely important.
278
Given the presence of guards in the system, two issues are unavoidable.
279
Are guards verified as part of the defun process? And are guards
280
checked when terms are evaluated? We answer both of those questions
283
Roughly speaking, in its initial state the system will try to verify
284
the guards of a defun if a :guard is supplied in the xargs and will not
285
try otherwise. However, guard verification in defun can be inhibited
286
"locally" by supplying the xargs :verify-guards nil. "Global"
287
inhibition can be obtained via the :set-verify-guards-eagerness. If
288
you do not use the :guard xargs, you will not need to think about guard
291
We now turn to the evaluation of expressions. Even if your functions
292
contain no guards, the primitive functions do and hence you have the
293
choice: when you submit an expression for evaluation do you mean for
294
guards to be checked at runtime or not? Put another way, do you mean
295
for the expression to be evaluated in Common Lisp (if possible) or in
296
the logic? Note: If Common Lisp delivers an answer, it will be the
297
same as in the logic, but it might be erroneous to execute the form in
298
Common Lisp. For example, should (car 'abc) cause a guard violation
301
The top-level ACL2 loop has a variable which controls which sense of
302
execution is provided. To turn "guard checking on," by which we mean
303
that guards are checked at runtime, execute the top-level form
304
:set-guard-checking t. To turn it off, do :set-guard-checking nil.
305
The status of this variable is reflected in the prompt.
309
means guard checking is on and
313
means guard checking is off. The exclamation mark can be thought of as
314
"barring" certain computations. The absence of the mark suggests the
315
absence of error messages or unbarred access to the logical axioms.
320
will signal an error, while
326
Note that whether or not guards are checked at runtime is independent
327
of whether you are operating in :program mode or :logic mode and
328
whether theorems are being proved or not. (Although it must be added
329
that functions defined in :program mode cannot help but check their
330
guards because no logical definition exists.)
332
Version 1.8 permits the verification of the guards of theorems, thus
333
insuring that all instances of the theorem will evaluate without error
334
in Common Lisp. To verify the guards of a theorem named name execute
337
(verify-guards name).
339
If a theorem's guards have been verified, the theorem is guaranteed to
340
evaluate without error to non-nil in Common Lisp (provided resource
341
errors do not arise).
343
Caveat about verify-guards: implies is a function symbol, so in the
344
term (implies p q), p cannot be assumed true when q is evaluated; they
345
are both evaluated "outside." Hence, you cannot generally verify the
346
guards on a theorem if implies is used to state the hypotheses. Use if
347
instead. In a future version of ACL2, implies will likely be a macro.
349
See sum-list-example.lisp for a nice example of the use of Version 1.8.
350
This is roughly the same as the documentation for guard-example.
352
We have removed the capability to do "old-style-forcing" as existed
353
before Version 1.5. See *Note NOTE5::.
355
NOTE: Some low level details have, of course, changed. One such
356
change is that there are no longer two distinct type prescriptions
357
stored when a function is admitted with its guards verified. So for
358
example, the type prescription rune for binary-append is now
360
(:type-prescription binary-append)
362
while in Versions 1.7 and earlier, there were two such runes:
364
(:type-prescription binary-append . 1)
365
(:type-prescription binary-append . 2)
367
Nqthm-style forcing on linear arithmetic assumptions is no longer
368
executed when forcing is disabled.
370
Functional instantiation now benefits from a trick also used in Nqthm:
371
once a constraint generated by a :functional-instance lemma instance
372
(see *note LEMMA-INSTANCE::) has been proved on behalf of a successful
373
event, it will not have to be re-proved on behalf of a later event.
375
1+ and 1- are now macros in the logic, not functions. Hence, for
376
example, it is "safe" to use them on left-hand sides of rewrite rules,
377
without invoking the common warning about the presence of nonrecursive
380
A new documentation section file-reading-example illustrates how to
381
process forms in a file.
383
A new proof-checker command forwardchain has been added; see *note
384
ACL2-PC||FORWARDCHAIN::.
386
It is now possible to use quantifiers. See *Note DEFUN-SK:: and see
389
There is a new event set-inhibit-warnings, which allows the user to
390
turn off warnings of various types. see *note SET-INHIBIT-WARNINGS::.
392
An unsoundness relating encapsulate and :functional-instance hints has
393
been remedied, with a few small effects visible at the user level. The
394
main observable effect is that defaxiom and non-local include-book
395
events are no longer allowed in the scope of any encapsulate event that
396
has a non-empty signature.
398
When certify-book is called, we now require that the default defun-mode
399
(see *note DEFAULT-DEFUN-MODE::) be :logic. On a related note, the
400
default defun-mode is irrelevant to include-book; the mode is always
401
set to :logic initially, though it may be changed within the book and
402
reverts to its original value at the conclusion of the include-book. A
403
bug in include-book prevented it from acting this way even though the
404
documentation said otherwise.
406
The documentation has been substantially improved. A new section
407
"Programming" contains documentation of many useful functions provided
408
by ACL2; see *note PROGRAMMING::. Also, the documentation has been
409
"marked up" extensively. Thus in particular, users of Mosaic will find
410
many links in the documentation.
412
The symbols force, mv-nth, and acl2-count have been added to the list
415
We now permit most names from the main Lisp package to be used as
416
names, except for names that define functions, macros, or constants.
419
We have changed the list of imports from the Common Lisp package to
420
ACL2, i.e., the list *common-lisp-symbols-from-main-lisp-package*, to
421
be exactly those external symbols of the Common Lisp package as
422
specified by the draft Common Lisp standard. In order to accommodate
423
this change, we have renamed some ACL2 functions as shown below, but
424
these and other ramifications of this change should be transparent to
428
print-object --> print-object$
430
Proof trees are no longer enabled by default. To start them up,
433
We have added the capability of building smaller images. The easiest
434
way to do this on a Unix (trademark of AT&T) system is: make small.
436
Here we will put some less important changes, additions, and so on.
438
We have added definitions for the Common Lisp function position (for
439
the test eql), as well as corresponding versions position-equal and
440
position-eq that use tests equal and eq, respectively. See *Note
441
POSITION::, see *note POSITION-EQUAL::, and see *note POSITION-EQ::.
443
The defthm event rational-listp-implies-rationalp-car no longer exists.
445
We fixed a bug in the hint mechanism that applied :by, :cases, and :use
446
hints to the first induction goal when the prover reverted to proving
447
the original goal by induction.
449
We fixed a bug in the handling of (set-irrelevant-formals-ok :warn).
451
In support of removing the old-style forcing capability, we deleted the
452
initialization of state global old-style-forcing and deleted the
453
definitions of recover-assumptions, recover-assumptions-from-goal,
454
remove-assumptions1, remove-assumptions, and split-on-assumptions, and
455
we renamed split-on-assumptions1 to split-on-assumptions.
457
The special value 'none in the proof-checker commands claim and = has
458
been replaced by :none.
460
A bug in the handling of hints by subgoals has been fixed. For
461
example, formerly a :do-not hint could be "erased" by a :use hint on a
462
subgoal. Thanks go to Art Flatau for noticing the bug.
464
The functions weak-termp and weak-term-listp have been deleted, and
465
their calls have been replaced by corresponding calls of pseudo-termp
466
and pseudo-term-listp. The notion of pseudo-termp has been slightly
467
strenthened by requiring that terms of the form (quote ...) have length
470
Performance has been improved in various ways. At the prover level,
471
backchaining through the recognizer alist has been eliminated in order
472
to significantly speed up ACL2's rewriter. Among the other prover
473
changes (of which there are several, all technical): we no longer
474
clausify the input term when a proof is interrupted in favor of
475
inducting on the input term. At the IO level, we have improved
476
performance somewhat by suitable declarations and proclamations. These
477
include technical modifications to the macros mv and mv-let, and
478
introduction of a macro the-mv analogous to the macro the but for forms
479
returning multiple values.
481
The function spaces now takes an extra argument, the current column.
483
A bug in the proof-checker equiv command was fixed.
485
The function intersectp has been deleted, because it was essentially
486
duplicated by the function intersectp-equal.
488
We now proclaim functions in AKCL and GCL before compiling books. This
489
should result in somewhat increased speed.
491
The function repeat has been eliminated; use make-list instead.
493
The proof-checker command expand has been fixed so that it eliminates
494
let (lambda) expressions when one would expect it to.
496
A new primitive function, mv-nth, has been introduced. Mv-nth is
497
equivalent to nth and is used in place of nth in the translation of
498
mv-let expressions. This allows the user to control the simplification
499
of mv-let expressions without affecting how nth is treated. In that
500
spirit, the rewriter has been modified so that certain mv-nth
501
expressions, namely those produced in the translation of (mv-let (a b
502
c)(mv x y z) p), are given special treatment.
504
A minor bug in untranslate has been fixed, which for example will fix
505
the printing of conjunctions.
507
Translate now takes a logicp argument, which indicates whether it
508
enforces the restriction that :program mode functions do not occur in
511
The modified version of trace provided by ACL2, for use in raw Lisp,
512
has been modified so that the lisp special variable *trace-alist* has a
513
slightly different functionality. This alist associates, using eq,
514
symbols with the print representations of their values. For example,
515
initially *trace-alist* is a one-element list containing the pair (cons
516
'state '|*the-live-state*|). Thus, one may cons the pair (cons '*foo*
517
"It's a FOO!") on to *trace-alist*; then until *foo* is defined, this
518
change will have no effect, but after for example
522
then trace will print 17 as "It's a FOO!".
524
Trace also traces the corresponding logic function.
526
Proof-tree display has been improved slightly in the case of successful
527
proofs and certain event failures.
529
The function positive-integer-log2 has been deleted.
531
The macro skip-proofs now prints a warning message when it is
532
encountered in the context of an encapsulate event or a book. See
535
Some functions related to the-fn and wormhole1 now have defun-mode
536
:program, but this change is almost certain to be inconsequential to
540
File: acl2-doc-emacs.info, Node: NOTE8-UPDATE, Next: NOTE9, Prev: NOTE8, Up: RELEASE-NOTES
542
NOTE8-UPDATE ACL2 Version 1.8 (Summer, 1995) Notes
544
ACL2 can now use Ordered Binary Decision Diagram technology. See *Note
545
BDD::. There is also a proof-checker bdd command.
547
ACL2 is now more respectful of the intention of the function hide. In
548
particular, it is more careful not to dive inside any call of hide
549
during equality substitution and case splitting.
551
The ld special (see *note LD::) ld-pre-eval-print may now be used to
552
turn off printing of input forms during processing of encapsulate and
553
certify-book forms, by setting it to the value :never, i.e.,
554
(set-ld-pre-eval-print :never state). See *Note LD-PRE-EVAL-PRINT::.
556
The TUTORIAL documentation section has, with much help from Bill Young,
557
been substantially improved to a bona fide introduction, and has been
558
renamed acl2-tutorial.
560
The term pretty-printer has been modified to introduce (<= X Y) as an
561
abbreviation for (not (< Y X)).
563
Forward chaining and linear arithmetic now both benefit from the
564
evaluation of ground subterms.
566
A new macro set-inhibit-output-lst has been defined. This should be
567
used when setting the state global inhibit-output-lst; see *note
568
SET-INHIBIT-OUTPUT-LST:: and see *note PROOF-TREE::.
570
The test for redundancy in definitions includes the guard and type
571
declarations. See *Note REDUNDANT-EVENTS::.
573
See *Note GENERALIZED-BOOLEANS:: for a discussion of a potential
574
soundness problem for ACL2 related to the question: Which Common Lisp
575
functions are known to return Boolean values?
577
Here we will put some less important changes, additions, and so on.
579
A bug has been fixed so that now, execution of :comp t (see *note
580
COMP::) correctly handles non-standard characters.
582
A bug in digit-char-p has been fixed, so that the "default" is nil
585
True-listp now tests the final cdr against nil using eq instead of
586
equal, for improved efficiency. The logical meaning is, however,
589
Put-assoc-equal has been added to the logic (it used to have
590
:defun-mode :program, and has been documented.
593
File: acl2-doc-emacs.info, Node: NOTE9, Prev: NOTE8-UPDATE, Up: RELEASE-NOTES
595
NOTE9 ACL2 Version 1.9 (Fall, 1996) Notes
597
By default, when the system is started it is illegal to use the
598
variable STATE as a formal parameter of a function definition. The aim
599
is to prevent novice users from stumbling into the Byzantine syntactic
600
restrictions on that variable symbol. Use
608
to switch back to the old default mode. See *Note SET-STATE-OK::
610
Set-state-ok is an event that affects the ACL2 defaults table (see
611
*note ACL2-DEFAULTS-TABLE::). Recall that when books are included, the
612
defaults table is restored to its pre-inclusion state. Thus, while a
613
set-state-ok form will permit the book to define a state-using
614
function, it will not permit the user of the book to make such a
615
definition. We recommend putting (set-state-ok t) in any book that
616
defines a state using function.
618
Books certified under Version 1.8 must be recertified under Version
619
1.9. See :DOC version.
621
The simplifier has been made to look out for built-in clauses, whereas
622
in past versions such clauses were only noticed by the "preprocessor"
623
at the top of the waterfall. THIS CHANGE MAY PREVENT OLD SCRIPTS FROM
624
REPLAYING! The undesirable side-effect is caused by the fact that
625
:HINTS require you to refer to clauses by their exact name (see *note
626
GOAL-SPEC::) and because the new simplifier proves more clauses than
627
before, the goals produced have different names. Thus, if a script
628
uses :HINTS that refer to clauses other than "Goal", e.g., "Subgoal
629
1.3" then the hint may be applied to a different subgoal than
632
The use of built-in-clauses has been made more efficient. If a set of
633
clauses arise often in a piece of work, it might be advantageous to
634
build them in even if that results in a large set (hundreds?) of
635
built-in clauses. See *Note BUILT-IN-CLAUSES::
637
Wormholes can now be used in :logic mode functions. See *Note WORMHOLE::
639
It is now possible to provide "computed hints." For example, have you
640
ever wished to say "in all goals with a name like this, :use that" or
641
"if this term is in the subgoal, then :use that"? Well, see *note
642
COMPUTED-HINTS:: and the extraordinarily long example in see *note
643
USING-COMPUTED-HINTS::.
645
Hide terms may be rewritten with :rewrite rules about hide. See *Note
646
HIDE::, where we also now explain why hide terms are sometimes
647
introduced into your proof attempts.
649
A bug that sometimes caused the "non-lazy IF" hard error message was
652
A bug that sometimes caused a hard error in forward chaining was fixed.
654
A bug in print-rules (:pr) was fixed.
656
We report the use of :executable-counterparts in the evaluation of
659
Some documentation errors were fixed.
661
A bug in parent-tree tracking in add-literal-and-pt was fixed.
663
A bug in ok$, go$ and eval$ was fixed.
665
Clausify now optimizes (mv-nth 'k (list x0 ... xk ... xn)) to xk.
668
File: acl2-doc-emacs.info, Node: RULE-CLASSES, Next: STOBJ, Prev: RELEASE-NOTES, Up: Top
670
RULE-CLASSES adding rules to the data base
673
a true list of rule class objects as defined below
676
a symbol abbreviating a single rule class object
678
ACL2 provides users with the ability to create a number of different
679
kinds of rules, including (conditional) rewrite rules but also
680
including others. Don't be put off by the long description to follow;
681
usually, you'll probably want to use rewrite rules. More on this below.
683
A rule class object is either one of the :class keywords or else is a
684
list of the form shown below. Those fields marked with "(!)" are
685
required when the :class is as indicated.
689
:TRIGGER-FNS (fn1 ... fnk) ; provided :class = :META (!)
690
:TRIGGER-TERMS (t1 ... tk) ; provided :class = :FORWARD-CHAINING
691
; or :class = :LINEAR
692
:TYPE-SET n ; provided :class = :TYPE-SET-INVERTER
693
:TYPED-TERM term ; provided :class = :TYPE-PRESCRIPTION
694
:CLIQUE (fn1 ... fnk) ; provided :class = :DEFINITION
695
:CONTROLLER-ALIST alist ; provided :class = :DEFINITION
696
:INSTALL-BODY directive ; provided :class = :DEFINITION
697
:LOOP-STOPPER alist ; provided :class = :REWRITE
698
:PATTERN term ; provided :class = :INDUCTION (!)
699
:CONDITION term ; provided :class = :INDUCTION
700
:SCHEME term ; provided :class = :INDUCTION (!)
701
:MATCH-FREE all-or-once ; provided :class = :REWRITE
703
or :class = :FORWARD-CHAINING
704
:BACKCHAIN-LIMIT-LST limit ; provided :class = :REWRITE
707
:HINTS hints ; provided instrs = nil
708
:INSTRUCTIONS instrs ; provided hints = nil
711
When rule class objects are provided by the user, most of the fields
712
are optional and their values are computed in a context sensitive way.
713
When a :class keyword is used as a rule class object, all relevant
714
fields are determined contextually. Each rule class object in
715
:rule-classes causes one or more rules to be added to the data base.
716
The :class keywords are documented individually under the following
717
names. Note that when one of these names is used as a :class, it is
718
expected to be in the keyword package (i.e., the names below should be
719
preceded by a colon but the ACL2 documentation facilities do not permit
720
us to use keywords below).
724
* BUILT-IN-CLAUSES:: to build a clause into the simplifier
726
* COMPOUND-RECOGNIZER:: make a rule used by the typing mechanism
728
* CONGRUENCE:: the relations to maintain while simplifying arguments
730
* DEFINITION:: make a rule that acts like a function definition
732
* ELIM:: make a destructor elimination rule
734
* EQUIVALENCE:: mark a relation as an equivalence relation
736
* FORWARD-CHAINING:: make a rule to forward chain when a certain trigger arises
738
* FREE-VARIABLES:: free variables in rules
740
* GENERALIZE:: make a rule to restrict generalizations
742
* INDUCTION:: make a rule that suggests a certain induction
744
* LINEAR:: make some arithmetic inequality rules
746
* META:: make a :meta rule (a hand-written simplifier)
748
* REFINEMENT:: record that one equivalence relation refines another
750
* REWRITE:: make some :rewrite rules (possibly conditional ones)
752
* TYPE-PRESCRIPTION:: make a rule that specifies the type of a term
754
* TYPE-SET-INVERTER:: exhibit a new decoding for an ACL2 type-set
756
* WELL-FOUNDED-RELATION:: show that a relation is well-founded on a set
758
Before we get into the discussion of rule classes, let us return to an
759
important point. In spite of the large variety of rule classes
760
available, at present we recommend that new ACL2 users rely almost
761
exclusively on (conditional) rewrite rules. A reasonable but slightly
762
bolder approach is to use :type-prescription and :forward-chaining
763
rules for "type-theoretic" rules, especially ones whose top-level
764
function symbol is a common one like true-listp or consp; see *note
765
TYPE-PRESCRIPTION:: and see *note FORWARD-CHAINING::. However, the
766
rest of the rule classes are really not intended for widespread use,
767
but rather are mainly for experts.
769
We expect that we will write more about the question of which kind of
770
rule to use. For now: when in doubt, use a :rewrite rule.
772
:Rule-classes is an optional keyword argument of the defthm (and
773
defaxiom) event. In the following, let name be the name of the event
774
and let thm be the formula to be proved or added as an axiom.
776
If :rule-classes is not specified in a defthm (or defaxiom) event, it
777
is as though :rule-classes ((:rewrite)) had been used. Use
778
:rule-classes nil to specify that no rules are to be generated.
780
If :rule-classes class is specified, where class is a non-nil symbol,
781
it is as though :rule-classes ((class)) had been used. Thus,
782
:rule-classes :forward-chaining is equivalent to :rule-classes
783
((:forward-chaining)).
785
We therefore now consider :rule-classes as a true list. If any element
786
of that list is a keyword, replace it by the singleton list containing
787
that keyword. Thus, :rule-classes (:rewrite :elim) is the same as
788
:rule-classes ((:rewrite) (:elim)).
790
Each element of the expanded value of :rule-classes must be a true list
791
whose car is one of the rule class keyword tokens listed above, e.g.,
792
:rewrite, :elim, etc., and whose cdr is a "keyword alist" alternately
793
listing keywords and values. The keywords in this alist must be taken
794
from those shown below. They may be listed in any order and most may
795
be omitted, as specified below.
797
:Corollary -- its value, term, must be a term. If omitted, this
798
field defaults to thm. The :corollary of a rule class object is
799
the formula actually used to justify the rule created and thus
800
determines the form of the rule. Nqthm provided no similar
801
capability: each rule was determined by thm, the theorem or axiom
802
added. ACL2 permits thm to be stated "elegantly" and then allows
803
the :corollary of a rule class object to specify how that elegant
804
statement is to be interpreted as a rule. For the rule class
805
object to be well-formed, its (defaulted) :corollary, term, must
806
follow from thm. Unless term is trivially implied by thm, using
807
little more than propositional logic, the formula (implies thm
808
term) is submitted to the theorem prover and the proof attempt
809
must be successful. During that proof attempt the values of
810
:hints, :instructions, and :otf-flg, as provided in the rule class
811
object, are provided as arguments to the prover. Such auxiliary
812
proofs give the sort of output that one expects from the prover.
813
However, as noted above, corollaries that follow trivially are not
814
submitted to the prover; thus, such corollaries cause no prover
817
Note that before term is stored, all calls of macros in it are
818
expanded away. See *Note TRANS::.
820
:Hints, :instructions, :otf-flg -- the values of these fields must
821
satisfy the same restrictions placed on the fields of the same
822
names in defthm. These values are passed to the recursive call of
823
the prover used to establish that the :corollary of the rule class
824
object follows from the theorem or axiom thm.
826
:Type-set -- this field may be supplied only if the :class is
827
:type-set-inverter. When provided, the value must be a type-set,
828
an integer in a certain range. If not provided, an attempt is
829
made to compute it from the corollary. See *Note
832
:Typed-term -- this field may be supplied only if the :class is
833
:type-prescription. When provided, the value is the term for which
834
the :corollary is a type-prescription lemma. If no :typed-term is
835
provided in a :type-prescription rule class object, we try to
836
compute heuristically an acceptable term. See *Note
839
:Trigger-terms -- this field may be supplied only if the :class is
840
:forward-chaining or :linear. When provided, the value is a list
841
of terms, each of which is to trigger the attempted application of
842
the rule. If no :trigger-terms is provided, we attempt to compute
843
heuristically an appropriate set of triggers. See *Note
844
FORWARD-CHAINING:: or see *note LINEAR::.
846
:Trigger-fns -- this field must (and may only) be supplied if the
847
:class is :meta. Its value must be a list of function symbols.
848
Terms with these symbols trigger the application of the rule. See
851
:Clique and :controller-alist -- these two fields may only be
852
supplied if the :class is :definition. If they are omitted, then
853
ACL2 will attempt to guess them. Suppose the :corollary of the
854
rule is (implies hyp (equiv (fn a1 ... an) body)). The value of
855
the :clique field should be a true list of function symbols, and if
856
non-nil must include fn. These symbols are all the members of the
857
mutually recursive clique containing this definition of fn. That
858
is, a call of any function in :clique is considered a "recursive
859
call" for purposes of the expansion heuristics. The value of the
860
:controller-alist field should be an alist that maps each function
861
symbol in the :clique to a list of t's and nil's of length equal to
862
the arity of the function. For example, if :clique consists of
863
just two symbols, fn1 and fn2, of arities 2 and 3 respectively,
864
then ((fn1 t nil) (fn2 nil t t)) is a legal value of
865
:controller-alist. The value associated with a function symbol in
866
this alist is a "mask" specifying which argument slots of the
867
function "control" the recursion for heuristic purposes. Sloppy
868
choice of :clique or :controller-alist can result in infinite
869
expansion and stack overflow.
871
:Install-body -- this field may only be supplied if the :class is
872
:definition. Its value must be t, nil, or the default,
873
:normalize. A value of t or :normalize will cause ACL2 to install
874
this rule as the new body of the function being "defined" (fn in
875
the paragraph just above); hence this definition will be installed
876
for future :expand hints. Furthermore, if this field is omitted
877
or the value is :normalize, then this definition will be
878
simplified using the so-called "normalization" procedure that is
879
used when processing definitions made with defun. You must
880
explicitly specify :install-body nil in the following cases: fn
881
(as above) is a member of the value of constant
882
*definition-minimal-theory*, the arguments are not a list of
883
distinct variables, equiv (as above) is not equal, or there are
884
free variables in the hypotheses or right-hand side (see *note
885
FREE-VARIABLES::). However, supplying :install-body nil will not
886
affect the rewriter's application of the :definition rule, other
887
than to avoid using the rule to apply :expand hints. If a
888
definition rule equates (f a1 ... ak) with body but there are
889
hypotheses, hyps, then :expand hints will replace terms (f term1
890
... termk) by corresponding terms (if hyps body (hide (f term1 ...
893
:Loop-stopper -- this field may only be supplied if the class is
894
:rewrite. Its value must be a list of entries each consisting of
895
two variables followed by a (possibly empty) list of functions, for
896
example ((x y binary-+) (u v foo bar)). It will be used to
897
restrict application of rewrite rules by requiring that the list
898
of instances of the second variables must be "smaller" than the
899
list of instances of the first variables in a sense related to the
900
corresponding functions listed; see *note LOOP-STOPPER::. The
901
list as a whole is allowed to be nil, indicating that no such
902
restriction shall be made. Note that any such entry that contains
903
a variable not being instantiated, i.e., not occurring on the left
904
side of the rewrite rule, will be ignored. However, for
905
simplicity we merely require that every variable mentioned should
906
appear somewhere in the corresponding :corollary formula.
908
:Pattern, :Condition, :Scheme -- the first and last of these fields
909
must (and may only) be supplied if the class is :induction.
910
:Condition is optional but may only be supplied if the class is
911
:induction. The values must all be terms and indicate,
912
respectively, the pattern to which a new induction scheme is to be
913
attached, the condition under which the suggestion is to be made,
914
and a term which suggests the new scheme. See *Note INDUCTION::.
916
:Match-free -- this field must be :all or :once and may be
917
supplied only if the :class is either :rewrite, :linear, or
918
:forward-chaining. See *Note FREE-VARIABLES:: for a description
919
of this field. Note: Although this field is intended to be used
920
for controlling retries of matching free variables in hypotheses,
921
it is legal to supply it even if there are no such free variables.
922
This can simplify the automated generation of rules, but note
923
that when :match-free is supplied, the warning otherwise provided
924
for the presence of free variables in hypotheses will be
927
Backchain-limit-lst -- this field may be supplied only if the
928
:class is either :rewrite, :meta, or :linear and only one rule is
929
generated from the formula. Its value must be nil; a non-negative
930
integer; or, except in the case of :meta rules, a true list each
931
element of which is either nil or a non-negative integer. If it
932
is a list, its length must be equal to the number of hypotheses of
933
the rule and each item in the list is the "backchain limit"
934
associated with the corresponding hypothesis. If
935
backchain-limit-lst is a non-negative integer, it is defaulted to
936
a list of the appropriate number of repetions of that integer.
937
The backchain limit of a hypothesis is used to limit the effort
938
that ACL2 will expend when relieving the hypothesis. If it is
939
NIL, no new limits are imposed; if it is an integer, the
940
hypothesis will be limited to backchaining at most that many
941
times. Note that backchaining may be further limited by a global
942
backchain-limit; see *note BACKCHAIN-LIMIT:: for details. For a
943
different way to reign in the rewriter, see *note
944
REWRITE-STACK-LIMIT::. Jared Davis has pointed out that you can
945
set this field to 0 to avoid any attempt to relieve forced
946
hypotheses, which can lead to a significant speed-up in some cases.
948
Once thm has been proved (in the case of defthm) and each rule class
949
object has been checked for well-formedness (which might require
950
additional proofs), we consider each rule class object in turn to
951
generate and add rules. Let :class be the class keyword token of the
952
ith class object (counting from left to right). Generate the rune
953
(:class name . x), where x is nil if there is only one class and
954
otherwise x is i. Then, from the :corollary of that object, generate
955
one or more rules, each of which has the name (:class name . x). See
956
the :doc entry for each rule class to see how formulas determine rules.
957
Note that it is in principle possible for several rules to share the
958
same name; it happens whenever a :corollary determines more than one
959
rule. This in fact only occurs for :rewrite, :linear, and
960
:forward-chaining class rules and only then if the :corollary is
961
essentially a conjunction. (See the documentation for rewrite, linear,
962
or forward-chaining for details.)
965
File: acl2-doc-emacs.info, Node: BUILT-IN-CLAUSES, Next: COMPOUND-RECOGNIZER, Prev: RULE-CLASSES, Up: RULE-CLASSES
967
BUILT-IN-CLAUSES to build a clause into the simplifier
969
See *Note RULE-CLASSES:: for a general discussion of rule classes and
970
how they are used to build rules from formulas. A :built-in-clause
971
rule can be built from any formula other than propositional
972
tautologies. Roughly speaking, the system uses the list of built-in
973
clauses as the first method of proof when attacking a new goal. Any
974
goal that is subsumed by a built in clause is proved "silently."
976
ACL2 maintains a set of "built-in" clauses that are used to
977
short-circuit certain theorem proving tasks. We discuss this at length
978
below. When a theorem is given the rule class :built-in-clause ACL2
979
flattens the implies and and structure of the :corollary formula so as
980
to obtain a set of formulas whose conjunction is equivalent to the
981
given corollary. It then converts each of these to clausal form and
982
adds each clause to the set of built-in clauses.
984
For example, the following :corollary (regardless of the definition of
987
(and (implies (and (true-listp x)
989
(< (acl2-count (abl x))
991
(implies (and (true-listp x)
993
(< (acl2-count (abl x))
996
will build in two clauses,
998
{(not (true-listp x))
1000
(< (acl2-count (abl x)) (acl2-count x))}
1004
{(not (true-listp x))
1006
(< (acl2-count (abl x)) (acl2-count x))}.
1008
We now give more background.
1010
Recall that a clause is a set of terms, implicitly representing the
1011
disjunction of the terms. Clause c1 is "subsumed" by clause c2 if some
1012
instance of c2 is a subset c1.
1014
For example, let c1 be
1018
(< (acl2-count (cdr l)) (acl2-count l))}.
1020
Then c1 is subsumed by c2, shown below,
1023
; second term omitted here
1024
(< (acl2-count (cdr x)) (acl2-count x))}
1026
because we can instantiate x in c2 with l to obtain a subset of c1.
1028
Observe that c1 is the clausal form of
1030
(implies (and (consp l)
1031
(not (equal a (car l))))
1032
(< (acl2-count (cdr l)) (acl2-count l))),
1034
c2 is the clausal form of
1037
(< (acl2-count (cdr l)) (acl2-count l)))
1039
and the subsumption property just means that c1 follows trivially from
1040
c2 by instantiation.
1042
The set of built-in clauses is just a set of known theorems in clausal
1043
form. Any formula that is subsumed by a built-in clause is thus a
1044
theorem. If the set of built-in theorems is reasonably small, this
1045
little theorem prover is fast. ACL2 uses the "built-in clause check"
1046
in four places: (1) at the top of the iteration in the prover - thus if
1047
a built-in clause is generated as a subgoal it will be recognized when
1048
that goal is considered, (2) within the simplifier so that no built-in
1049
clause is ever generated by simplification, (3) as a filter on the
1050
clauses generated to prove the termination of recursively defun'd
1051
functions and (4) as a filter on the clauses generated to verify the
1052
guards of a function.
1054
The latter two uses are the ones that most often motivate an extension
1055
to the set of built-in clauses. Frequently a given formalization
1056
problem requires the definition of many functions which require
1057
virtually identical termination and/or guard proofs. These proofs can
1058
be short-circuited by extending the set of built-in clauses to contain
1059
the most general forms of the clauses generated by the definitional
1062
The attentive user might have noticed that there are some recursive
1063
schemes, e.g., recursion by cdr after testing consp, that ACL2 just
1064
seems to "know" are ok, while for others it generates measure clauses
1065
to prove. Actually, it always generates measure clauses but then
1066
filters out any that pass the built-in clause check. When ACL2 is
1067
initialized, the clause justifying cdr recursion after a consp test is
1068
added to the set of built-in clauses. (That clause is c2 above.)
1070
Note that only a subsumption check is made; no rewriting or
1071
simplification is done. Thus, if we want the system to "know" that cdr
1072
recursion is ok after a negative atom test (which, by the definition of
1073
atom, is the same as a consp test), we have to build in a second
1074
clause. The subsumption algorithm does not "know" about commutative
1075
functions. Thus, for predictability, we have built in commuted
1076
versions of each clause involving commutative functions. For example,
1082
(< (acl2-count (+ -1 x)) (acl2-count x))}
1084
and the commuted version
1089
(< (acl2-count (+ -1 x)) (acl2-count x))}
1091
so that the user need not worry whether to write (= x 0) or (= 0 x) in
1094
:built-in-clause rules added by the user can be enabled and disabled.
added
removed
doc/EMACS/acl2-doc-emacs.info-47
