← Back to branch summary

~ubuntu-branches/ubuntu/gutsy/acl2/gutsy

« back to all changes in this revision

Viewing changes to doc/HTML/DEFUN-SK.html

  • Committer: Bazaar Package Importer
  • Author(s): Camm Maguire
  • Date: 2006-12-04 10:35:42 UTC
  • mfrom: (1.1.5 upstream) (3.1.1 etch)
  • Revision ID: james.westby@ubuntu.com-20061204103542-68nf4pkilci0018n
Tags: 3.1-1
New upstream release

Show diffs side-by-side

added added

removed removed

Lines of Context:
doc/HTML/DEFUN-SK.html
1
1
<html>
2
 
<head><title>DEFUN-SK.html  --  ACL2 Version 3.0.1</title></head>
 
2
<head><title>DEFUN-SK.html  --  ACL2 Version 3.1</title></head>
3
3
<body text=#000000 bgcolor="#FFFFFF">
4
4
<h2>DEFUN-SK</h2>define a function whose body has an outermost quantifier
5
5
<pre>Major Section:  <a href="EVENTS.html">EVENTS</a>
44
44
 
45
45
General Form:
46
46
(defun-sk fn (var1 ... varn) body
47
 
  &amp;key doc quant-ok skolem-name thm-name witness-dcls)
 
47
  &amp;key rewrite doc quant-ok skolem-name thm-name witness-dcls)
48
48
</pre>
49
49
 
50
50
where <code>fn</code> is the symbol you wish to define and is a new symbolic
129
129
indeed does introduce the quantified notions that it claims to
130
130
introduce.<p>
131
131
 
 
132
Notice that the <code><a href="DEFTHM.html">defthm</a></code> event just above, <code>forall-x-y-p0-and-q0-necc</code>,
 
133
may not be of optimal form as a rewrite rule.  Users sometimes find that when
 
134
the quantifier is <code>forall</code>, it is useful to state this rule in a form where
 
135
the new quantified predicate is a hypothesis instead.  In this case that form
 
136
would be as follows:
 
137
 
 
138
<pre>
 
139
(defthm forall-x-y-p0-and-q0-necc
 
140
  (implies (forall-x-y-p0-and-q0 z)
 
141
           (and (p0 x y z) (q0 x y z))))
 
142
</pre>
 
143
 
 
144
ACL2 will turn this into one <code>:</code><code><a href="REWRITE.html">rewrite</a></code> rule for each conjunct,
 
145
<code>(p0 x y z)</code> and <code>(q0 x y z)</code>, with hypothesis
 
146
<code>(forall-x-y-p0-and-q0 z)</code> in each case.  In order to get this effect, use
 
147
<code>:rewrite :direct</code>, in this case as follows.
 
148
 
 
149
<pre>
 
150
(defun-sk forall-x-y-p0-and-q0 (z)
 
151
  (forall (x y)
 
152
          (and (p0 x y z)
 
153
               (q0 x y z)))
 
154
  :rewrite :direct)
 
155
</pre>
 
156
<p>
 
157
 
132
158
We now turn to a detailed description <code>defun-sk</code>, starting with a
133
159
discussion of its arguments as shown in the "General Form" above.<p>
134
160
 
170
196
  (implies (not term)
171
197
           (not (fn var1 ... varn))))
172
198
</pre>
 
199
<p>
 
200
 
 
201
In the <code>forall</code> case, however, the keyword pair <code>:rewrite :direct</code> may be
 
202
supplied after the body of the <code>defun-sk</code> form, in which case the
 
203
contrapositive of the above form is used instead:
 
204
 
 
205
<pre>
 
206
(defthm fn-necc ;in case the quantifier is FORALL
 
207
  (implies (fn var1 ... varn)
 
208
           term))
 
209
</pre>
 
210
 
 
211
This is often a better choice for the "-NECC" rule, provided ACL2 can parse
 
212
<code>term</code> as a <code>:</code><code><a href="REWRITE.html">rewrite</a></code> rule.  A second possible value of the
 
213
<code>:rewrite</code> argument of <code>defun-sk</code> is <code>:default</code>, which gives the same
 
214
behavior as when <code>:rewrite</code> is omitted.  Otherwise, the value of
 
215
<code>:rewrite</code> should be the term to use as the body of the <code>fn-necc</code> theorem
 
216
shown above; ACL2 will attempt to do the requisite proof in this case.  If
 
217
that term is weaker than the default, the properties introduced by
 
218
<code>defun-sk</code> may of course be weaker than they would be otherwise.  Finally,
 
219
note that the <code>:rewrite</code> keyword argument for <code>defun-sk</code> only makes sense
 
220
if the quantifier is <code>forall</code>; it is thus illegal if the quantifier is
 
221
<code>exists</code>.  Enough said about <code>:rewrite</code>!<p>
173
222
 
174
223
In the case that <code>bound-vars</code> is a list of at least two variables, say
175
 
<code>(bv1 ... bvk)</code>, the definition above is the following instead, but
176
 
the theorem remains unchanged.
 
224
<code>(bv1 ... bvk)</code>, the definition above (with no keywords) is the following
 
225
instead, but the theorem remains unchanged.
177
226
 
178
227
<pre>
179
228
(defun fn (var1 ... varn)
210
259
see <a href="DEFCHOOSE.html">defchoose</a>.<p>
211
260
 
212
261
If you find that the rewrite rules introduced with a particular use of
213
 
<code>defun-sk</code> are not ideal, then at least two reasonable courses of action
214
 
are available for you.  Perhaps the best option is to prove the <code><a href="REWRITE.html">rewrite</a></code>
215
 
rules you want.  If you see a pattern for creating rewrite rules from your
216
 
<code>defun-sk</code> events, you might want to write a macro that executes a
217
 
<code>defun-sk</code> followed by one or more <code><a href="DEFTHM.html">defthm</a></code> events.  Another option is
218
 
to write your own variant of the <code>defun-sk</code> macro, say, <code>my-defun-sk</code>,
219
 
for example by modifying a copy of the definition of <code>defun-sk</code> from the
220
 
ACL2 sources.<p>
 
262
<code>defun-sk</code> are not ideal, even when using the <code>:rewrite</code> keyword
 
263
discussed above (in the <code>forall</code> case), then at least two reasonable
 
264
courses of action are available for you.  Perhaps the best option is to prove
 
265
the <code><a href="REWRITE.html">rewrite</a></code> rules you want.  If you see a pattern for creating rewrite
 
266
rules from your <code>defun-sk</code> events, you might want to write a macro that
 
267
executes a <code>defun-sk</code> followed by one or more <code><a href="DEFTHM.html">defthm</a></code> events.  Another
 
268
option is to write your own variant of the <code>defun-sk</code> macro, say,
 
269
<code>my-defun-sk</code>, for example by modifying a copy of the definition of
 
270
<code>defun-sk</code> from the ACL2 sources.<p>
221
271
 
222
272
If you want to represent nested quantifiers, you can use more than one
223
273
<code>defun-sk</code> event.  For example, in order to represent
240
290
Some distracting and unimportant warnings are inhibited during
241
291
<code>defun-sk</code>.<p>
242
292
 
243
 
Note that this way of implementing quantifiers is not a new idea.
244
 
Hilbert was certainly aware of it 60 years ago!  A paper by ACL2
245
 
authors Kaufmann and Moore, entitled ``Structured Theory Development
246
 
for a Mechanized Logic'' (Journal of Automated Reasoning 26, no. 2 (2001),
247
 
pp. 161-203) explains why our use of <code><a href="DEFCHOOSE.html">defchoose</a></code> is appropriate, even in
248
 
the presence of <code>epsilon-0</code> induction.
 
293
Note that this way of implementing quantifiers is not a new idea.  Hilbert
 
294
was certainly aware of it 60 years ago!  Also
 
295
see <a href="CONSERVATIVITY-OF-DEFCHOOSE.html">conservativity-of-defchoose</a> for a technical argument that justifies the
 
296
logical conservativity of the <code><a href="DEFCHOOSE.html">defchoose</a></code> event in the sense of the paper
 
297
by Kaufmann and Moore entitled ``Structured Theory Development for a
 
298
Mechanized Logic'' (Journal of Automated Reasoning 26, no. 2 (2001),
 
299
pp. 161-203).
249
300
<br><br><br><a href="acl2-doc.html"><img src="llogo.gif"></a> <a href="acl2-doc-index.html"><img src="index.gif"></a>
250
301
</body>
251
302
</html>