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
|
<html>
<head><title>QUANTIFIERS.html -- ACL2 Version 3.1</title></head>
<body text=#000000 bgcolor="#FFFFFF">
<h3>QUANTIFIERS</h3>issues about quantification in ACL2
<pre>Major Section: <a href="DEFUN-SK.html">DEFUN-SK</a>
</pre><p>
ACL2 supports first-order quantifiers <code><a href="EXISTS.html">exists</a></code> and <code><a href="FORALL.html">forall</a></code> by way of
the <code><a href="DEFUN-SK.html">defun-sk</a></code> event. However, proof support for quantification is
quite limited. Therefore, we recommend using recursion in place of
<code>defun-sk</code> when possible (following common ACL2 practice).
<p>
<ul>
<li><h3><a href="QUANTIFIERS-USING-DEFUN-SK.html">QUANTIFIERS-USING-DEFUN-SK</a> -- quantification example
</h3>
</li>
<li><h3><a href="QUANTIFIERS-USING-DEFUN-SK-EXTENDED.html">QUANTIFIERS-USING-DEFUN-SK-EXTENDED</a> -- quantification example with details
</h3>
</li>
<li><h3><a href="QUANTIFIERS-USING-RECURSION.html">QUANTIFIERS-USING-RECURSION</a> -- recursion for implementing quantification
</h3>
</li>
</ul>
For example, the notion ``every member of <code>x</code> has property <code>p</code>'' can be
defined either with recursion or explicit quantification, but proofs
may be simpler when recursion is used. We illustrate this point
with two proofs of the same informal claim, one of which uses
recursion which the other uses explicit quantification. Notice that
with recursion, the proof goes through fully automatically; but this
is far from true with explicit quantification (especially notable is
the ugly hint).<p>
The informal claim for our examples is: If every member <code>a</code> of each
of two lists satisfies the predicate <code>(p a)</code>, then this holds of their
<code><a href="APPEND.html">append</a></code>; and, conversely.<p>
See <a href="QUANTIFIERS-USING-RECURSION.html">quantifiers-using-recursion</a> for a solution to this example
using recursion.<p>
See <a href="QUANTIFIERS-USING-DEFUN-SK.html">quantifiers-using-defun-sk</a> for a solution to this example
using <code><a href="DEFUN-SK.html">defun-sk</a></code>. Also See <a href="QUANTIFIERS-USING-DEFUN-SK-EXTENDED.html">quantifiers-using-defun-sk-extended</a>
for an elaboration on that solution.
<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>
|
