File: NOTE5.html

package info (click to toggle)
acl2 3.1-1
  • links: PTS
  • area: main
  • in suites: etch, etch-m68k
  • size: 36,712 kB
  • ctags: 38,396
  • sloc: lisp: 464,023; makefile: 5,470; sh: 86; csh: 47; cpp: 25; ansic: 22
file content (250 lines) | stat: -rw-r--r-- 18,314 bytes parent folder | download
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
<html>
<head><title>NOTE5.html  --  ACL2 Version 3.1</title></head>
<body text=#000000 bgcolor="#FFFFFF">
<h2>NOTE5</h2>Acl2 Version 1.5 Notes
<pre>Major Section:  <a href="RELEASE-NOTES.html">RELEASE-NOTES</a>
</pre><p>

Acl2 now allows ``complex rationals,'' which are complex numbers
whose real parts are rationals and whose imaginary parts are
non-zero rationals.  See <a href="COMPLEX.html">complex</a>.<p>

A new way of handling <code><a href="FORCE.html">force</a></code>d hypotheses has been implemented.
Rather than cause a case split at the time the <code><a href="FORCE.html">force</a></code> occurs, we
complete the main proof and then embark on one or more ``forcing
rounds'' in which we try to prove the <a href="FORCE.html">force</a>d hypotheses.
See <a href="FORCING-ROUND.html">forcing-round</a>.  To allow us to compare the new handling of
<code><a href="FORCE.html">force</a></code> with the old, Version 1.5 implements both and uses a flag in
<code><a href="STATE.html">state</a></code> to determine which method should be used.  Do
<code>(assign old-style-forcing t)</code> if you want <code><a href="FORCE.html">force</a></code> to be handled
as it was in Version 1.4.  However, we expect to eliminate the
old-style forcing eventually because we think the new style is more
effective.  To see the difference between the two approaches to
forcing, try proving the associativity of <a href="APPEND.html">append</a> under both settings
of <code>old-style-forcing</code>.  To get the new behavior invoke:

<pre>
(thm (implies (and (true-listp a) (true-listp b))
              (equal (append (append a b) c)
                     (append a (append b c)))))
</pre>

Then <code>(assign old-style-forcing t)</code> and invoke the <code>thm</code> <a href="COMMAND.html">command</a> above
again.<p>

A new <code>:cases</code> <a href="HINTS.html">hints</a> allows proof by cases.  See <a href="HINTS.html">hints</a>.<p>

<code><a href="INCLUDE-BOOK.html">Include-book</a></code> and <code><a href="ENCAPSULATE.html">encapsulate</a></code> now restore the <code><a href="ACL2-DEFAULTS-TABLE.html">acl2-defaults-table</a></code>
when they complete.  See <a href="INCLUDE-BOOK.html">include-book</a> and see <a href="ENCAPSULATE.html">encapsulate</a>.<p>

The <a href="GUARD.html">guard</a>s on many Acl2 primitives defined in <code>axioms.lisp</code> have been
weakened to permit them to be used in accordance with lisp custom
and tradition.<p>

It is possible to attach heuristic filters to <code>:</code><code><a href="REWRITE.html">rewrite</a></code> rules to
limit their applicability.  See <a href="SYNTAXP.html">syntaxp</a>.<p>

A tutorial has been added; see <a href="ACL2-TUTORIAL.html">acl2-tutorial</a>.<p>

<a href="EVENTS.html">Events</a> now print the Summary paragraph listing <a href="RUNE.html">rune</a>s used, time,
etc., whether they succeed or fail.  The format of the ``<a href="FAILURE.html">failure</a>
banner'' has been changed but still has multiple asterisks in it.
<code>Thm</code> also prints a Summary, whether it succeeds or fails; but <code>thm</code> is
not an event.<p>

A new event form <code><a href="SKIP-PROOFS.html">skip-proofs</a></code> has been added; see <a href="SKIP-PROOFS.html">skip-proofs</a>.<p>

A user-specific customization facility has been added in the form of
a book that is automatically included, if it exists on the current
directory.  See <a href="ACL2-CUSTOMIZATION.html">acl2-customization</a>.<p>

A facility for conditional metalemmas has been implemented;
see <a href="META.html">meta</a>.<p>

The acceptable values for <code><a href="LD-SKIP-PROOFSP.html">ld-skip-proofsp</a></code> have changed.  In the old
version (Version 1.4), a value of <code>t</code> meant that proofs and <code><a href="LOCAL.html">local</a></code>
<a href="EVENTS.html">events</a> are to be skipped.  In Version 1.5, a value of <code>t</code> means proofs
(but not <code><a href="LOCAL.html">local</a></code> <a href="EVENTS.html">events</a>) are to be skipped.  A value of <code>'</code><code><a href="INCLUDE-BOOK.html">include-book</a></code>
means proofs and <code><a href="LOCAL.html">local</a></code> <a href="EVENTS.html">events</a> are to be skipped.  There are two
other, more obscure, acceptable values.  See <a href="LD-SKIP-PROOFSP.html">ld-skip-proofsp</a>.<p>

In order to turn off the forcing of assumptions, one should now
<a href="DISABLE.html">disable</a> the <code>:</code><code><a href="EXECUTABLE-COUNTERPART.html">executable-counterpart</a></code> of <code><a href="FORCE.html">force</a></code> (rather than the
<code>:</code><code><a href="DEFINITION.html">definition</a></code> of <code><a href="FORCE.html">force</a></code>, as in the previous release); see <a href="FORCE.html">force</a>.<p>

The macros <code><a href="ENABLE-FORCING.html">enable-forcing</a></code> and <code><a href="DISABLE-FORCING.html">disable-forcing</a></code> make it convenient to
<a href="ENABLE.html">enable</a> or <a href="DISABLE.html">disable</a> forcing.  See <a href="ENABLE-FORCING.html">enable-forcing</a> and
see <a href="DISABLE-FORCING.html">disable-forcing</a>.<p>

The new commands <code>:</code><code><a href="PR.html">pr</a></code> and <code>:</code><code><a href="PR_bang_.html">pr!</a></code> print the rules created by an event or
command.  See <a href="PR.html">pr</a> and see <a href="PR_bang_.html">pr!</a>.<p>

The new <a href="HISTORY.html">history</a> <a href="COMMAND.html">command</a>s <code>:</code><code><a href="PUFF.html">puff</a></code> and <code>:</code><code><a href="PUFF_star_.html">puff*</a></code> will replace a compound
<a href="COMMAND.html">command</a> such as an <code><a href="ENCAPSULATE.html">encapsulate</a></code> or <code><a href="INCLUDE-BOOK.html">include-book</a></code> by the sequence of
<a href="EVENTS.html">events</a> in it.  That is, they ``<a href="PUFF.html">puff</a> up'' or ``lift'' the subevents
of a <a href="COMMAND.html">command</a> to the <a href="COMMAND.html">command</a> level, eliminating the formerly superior
<a href="COMMAND.html">command</a> and lengthening the <a href="HISTORY.html">history</a>.  This is useful if you want to
``partially undo'' an <code><a href="ENCAPSULATE.html">encapsulate</a></code> or book or other compound <a href="COMMAND.html">command</a>
so you can experiment.  See <a href="PUFF.html">puff</a> and see <a href="PUFF_star_.html">puff*</a>.<p>

Theory expressions now are allowed to use the free variable <code><a href="WORLD.html">world</a></code>
and prohibited from using the free variable <code><a href="STATE.html">state</a></code>.
See <a href="THEORIES.html">theories</a>, although it is essentially the same as before
except it mentions <code><a href="WORLD.html">world</a></code> instead of <code><a href="STATE.html">state</a></code>.  See <a href="WORLD.html">world</a> for a
discussion of the Acl2 logical <a href="WORLD.html">world</a>.  Allowing <code><a href="IN-THEORY.html">in-theory</a></code> <a href="EVENTS.html">events</a> to
be state-sensitive violated an important invariant about how <a href="BOOKS.html">books</a>
behaved.<p>

<code><a href="TABLE.html">Table</a></code> keys and values now are allowed to use the free variable <code><a href="WORLD.html">world</a></code>
and prohibited from using the free variable <code><a href="STATE.html">state</a></code>.  See the note
above about theory expressions for some explanation.<p>

The macro for minus, <code><a href="_hyphen_.html">-</a></code>, used to expand <code>(- x 3)</code> to <code>(+ x -3)</code> and now
expands it to <code>(+ -3 x)</code> instead.  The old macro, if used in the
left-hand sides of rewrite rules, produced inapplicable rules
because the constant occurs in the second argument of the <code><a href="+.html">+</a></code>, but
potential target terms generally had the constant in the first
argument position because of the effect of <code>commutativity-of-+</code>.<p>

A new class of rule, <code>:linear-alias</code> rules, allows one to implement
the nqthm package and similar hacks in which a <a href="DISABLE.html">disable</a>d function is
to be known equivalent to an arithmetic function.<p>

A new class of rule, <code>:built-in-clause</code> rules, allows one to extend
the set of clauses proved silently by <code><a href="DEFUN.html">defun</a></code> during measure and <a href="GUARD.html">guard</a>
processing.  See <a href="BUILT-IN-CLAUSES.html">built-in-clauses</a>.<p>

The new command <code><a href="PCB_bang_.html">pcb!</a></code> is like <code><a href="PCB.html">pcb</a></code> but sketches the <a href="COMMAND.html">command</a> and then
prints its subsidiary <a href="EVENTS.html">events</a> in full.  See <a href="PCB_bang_.html">pcb!</a>.<p>

<code>:</code><code><a href="REWRITE.html">Rewrite</a></code> class rules may now specify the <code>:</code><code><a href="LOOP-STOPPER.html">loop-stopper</a></code> field.
See <a href="RULE-CLASSES.html">rule-classes</a> and see <a href="LOOP-STOPPER.html">loop-stopper</a>.<p>

The rules for how <a href="LOOP-STOPPER.html">loop-stopper</a>s control permutative rewrite rules
have been changed.  One effect of this change is that now when the
built-in commutativity rules for <code><a href="+.html">+</a></code> are used, the terms <code>a</code> and <code>(- a)</code>
are permuted into adjacency.  For example, <code>(+ a b (- a))</code> is now
normalized by the commutativity rules to <code>(+ a (- a) b)</code>; in Version
1.4, <code>b</code> was considered syntactically smaller than <code>(- a)</code> and so
<code>(+ a b (- a))</code> is considered to be in normal form.  Now it is
possible to arrange for unary functions be be considered
``invisible'' when they are used in certain contexts.  By default,
<code><a href="UNARY--.html">unary--</a></code> is considered invisible when its application appears in
the argument list of <code><a href="BINARY-+.html">binary-+</a></code>.  See <a href="LOOP-STOPPER.html">loop-stopper</a> and
see :DOC set-invisible-fns-table.<p>

Extensive documentation has been provided on the topic of Acl2's
``term ordering.''  See <a href="TERM-ORDER.html">term-order</a>.<p>

Calls of <code><a href="LD.html">ld</a></code> now default <code><a href="LD-ERROR-ACTION.html">ld-error-action</a></code> to <code>:return</code> rather than to
the current setting.<p>

The <a href="COMMAND.html">command</a> descriptor <code>:x</code> has been introduced and is synonymous with
<code>:</code><code><a href="MAX.html">max</a></code>, the most recently executed <a href="COMMAND.html">command</a>.  <a href="HISTORY.html">History</a> <a href="COMMAND.html">command</a>s such as
<code>:</code><code><a href="PBT.html">pbt</a></code> print a <code>:x</code> beside the most recent <a href="COMMAND.html">command</a>, simply to indicate
that it <strong>is</strong> the most recent one.<p>

The <a href="COMMAND.html">command</a> descriptor <code>:x-23</code> is synonymous with <code>(:x -23)</code>.  More
generally, every symbol in the keyword package whose first character
is <code>#\x</code> and whose remaining <a href="CHARACTERS.html">characters</a> parse as a negative integer
is appropriately understood.  This allows <code>:</code><code><a href="PBT.html">pbt</a></code> <code>:x-10</code> where <code>:</code><code><a href="PBT.html">pbt</a></code>
<code>(:max -10)</code> or <code>:</code><code><a href="PBT.html">pbt</a></code> <code>(:here -10)</code> were previously used.  The old forms
are still legal.<p>

The order of the arguments to <code><a href="DEFCONG.html">defcong</a></code> has been changed.<p>

The simplifier now reports the use of unspecified built-in type
information about the primitives with the phrase ``primitive type
reasoning.''  This phrase may sometimes occur in situations where
``propositional calculus'' was formerly credited with the proof.<p>

The function <code><a href="PAIRLIS.html">pairlis</a></code> has been replaced in the code by a new function
<code><a href="PAIRLIS$.html">pairlis$</a></code>, because Common Lisp does not adequately specify its
<code><a href="PAIRLIS.html">pairlis</a></code> function.<p>

Some new Common Lisp functions have been added, including <code><a href="LOGTEST.html">logtest</a></code>,
<code><a href="LOGCOUNT.html">logcount</a></code>, <code><a href="INTEGER-LENGTH.html">integer-length</a></code>, <code><a href="MAKE-LIST.html">make-list</a></code>, <code><a href="REMOVE-DUPLICATES.html">remove-duplicates</a></code>, <code><a href="STRING.html">string</a></code>, and
<code><a href="CONCATENATE.html">concatenate</a></code>.  The source file <code>/slocal/src/acl2/axioms.lisp</code> is the
ultimate reference regarding Common Lisp functions in Acl2.<p>

The functions <code><a href="DEFUNS.html">defuns</a></code> and <code><a href="THEORY-INVARIANT.html">theory-invariant</a></code> have been documented.
See <a href="DEFUNS.html">defuns</a> and see <a href="THEORY-INVARIANT.html">theory-invariant</a>.<p>

A few symbols have been added to the list <code>*acl2-exports*</code>.<p>

A new key has been implemented for the <code><a href="ACL2-DEFAULTS-TABLE.html">acl2-defaults-table</a></code>,
<code>:irrelevant-formals-ok</code>.  See <a href="SET-IRRELEVANT-FORMALS-OK.html">set-irrelevant-formals-ok</a>.<p>

The connected book directory, <code><a href="CBD.html">cbd</a></code>, must be nonempty and begin and
end with a slash.  It is set (and displayed) automatically upon your
first entry to <code><a href="LP.html">lp</a></code>.  You may change the setting with <code><a href="SET-CBD.html">set-cbd</a></code>.
See <a href="CBD.html">cbd</a>.<p>

<code>:</code><code><a href="OOPS.html">oops</a></code> will undo the last <code>:</code><code><a href="UBT.html">ubt</a></code>.  See <a href="OOPS.html">oops</a>.<p>

Documentation has been written about the ordinals.  See :DOC <code>e0-ordinalp</code>
and see :DOC <code>e0-ord-&lt;</code>.  [Note added later: Starting with Version_2.8,
instead see <a href="O-P.html">o-p</a> and see <a href="O_lt_.html">o&lt;</a>.
<p>
The color <a href="EVENTS.html">events</a> -- (red), (pink), (blue), and (gold) -- may no
longer be enclosed inside calls of <code><a href="LOCAL.html">local</a></code>, for soundness reasons.  In
fact, neither may any event that sets the <code><a href="ACL2-DEFAULTS-TABLE.html">acl2-defaults-table</a></code>.
See <a href="EMBEDDED-EVENT-FORM.html">embedded-event-form</a>.<p>

See <a href="LD-KEYWORD-ALIASES.html">ld-keyword-aliases</a> for an example of how to change the exit
keyword from <code>:</code><code><a href="Q.html">q</a></code> to something else.<p>

The attempt to install a <a href="MONITOR.html">monitor</a> on <code>:</code><code><a href="REWRITE.html">rewrite</a></code> rules stored as simple
abbreviations now causes an error because the application of
abbreviations is not tracked.<p>

A new message is sometimes printed by the theorem prover, indicating
that a given simplification is ``specious'' because the subgoals it
produces include the input goal.  In Version 1.4 this was detected
but not reported, causing behavior some users found bizarre.
See <a href="SPECIOUS-SIMPLIFICATION.html">specious-simplification</a>.<p>

<code>:</code><code><a href="DEFINITION.html">Definition</a></code> rules are no longer always required to specify the
<code>:clique</code> and <code>:controller-alist</code> fields; those fields can be defaulted
to system-determined values in many common instances.
See <a href="DEFINITION.html">definition</a>.<p>

A warning is printed if a macro form with keyword arguments is given
duplicate keyword values.  Execute <code>(thm t :doc nil :doc "ignored")</code>
and read the warning printed.<p>

A new restriction has been placed on <code><a href="ENCAPSULATE.html">encapsulate</a></code>.  Non-<code><a href="LOCAL.html">local</a></code>
recursive definitions inside the <code><a href="ENCAPSULATE.html">encapsulate</a></code> may not use, in their
tests and recursive calls, the constrained functions introduced by
the <code><a href="ENCAPSULATE.html">encapsulate</a></code>.  See <a href="SUBVERSIVE-RECURSIONS.html">subversive-recursions</a>.  (Note added in
Version  2.3:  Subversive recursions were first recognized by us here
in Version 1.5, but our code for recognizing them was faulty and the
bug was not fixed until Version  2.3.) <p>

The <a href="EVENTS.html">events</a> <code><a href="DEFEQUIV.html">defequiv</a></code>, <code><a href="DEFCONG.html">defcong</a></code>, <code><a href="DEFREFINEMENT.html">defrefinement</a></code>, and <code><a href="DEFEVALUATOR.html">defevaluator</a></code> have
been reimplemented so that they are just macros that expand into
appropriate <code><a href="DEFTHM.html">defthm</a></code> or <code><a href="ENCAPSULATE.html">encapsulate</a></code> <a href="EVENTS.html">events</a>; they are no longer
primitive <a href="EVENTS.html">events</a>.  See the <a href="DOCUMENTATION.html">documentation</a> of each affected event.<p>

The <code>defcor</code> event, which was a shorthand for a <code><a href="DEFTHM.html">defthm</a></code> that
established a <a href="COROLLARY.html">corollary</a> of a named, previously proved event, has
been eliminated because its implementation relied on a technique we
have decided to ban from our code.  If you want the effect of a
<code>defcor</code> in Version 1.5 you must submit the corresponding <code><a href="DEFTHM.html">defthm</a></code> with
a <code>:by</code> hint naming the previously proved event.<p>

Error reporting has been improved for inappropriate <code><a href="IN-THEORY.html">in-theory</a></code> <a href="HINTS.html">hints</a>
and <a href="EVENTS.html">events</a>, and for syntax errors in rule classes, and for
non-existent filename arguments to <code><a href="LD.html">ld</a></code>.<p>

Technical Note:  We now maintain the Third Invariant on <code>type-alists</code>,
as described in the Essay on the Invariants on Type-alists, and
Canonicality.  This change will affect some proofs, for example, by
causing a to rewrite more quickly to <code>c</code> when <code>(equiv a b)</code> and
<code>(equiv b c)</code> are both known and <code>c</code> is the canonical
representative of the three.<p>


<br><br><br><a href="acl2-doc.html"><img src="llogo.gif"></a> <a href="acl2-doc-index.html"><img src="index.gif"></a>
</body>
</html>