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
|
<html>
<head><title>QUANTIFIERS-USING-RECURSION.html -- ACL2 Version 3.1</title></head>
<body text=#000000 bgcolor="#FFFFFF">
<h4>QUANTIFIERS-USING-RECURSION</h4>recursion for implementing quantification
<pre>Major Section: <a href="QUANTIFIERS.html">QUANTIFIERS</a>
</pre><p>
The following example illustrates the use of recursion as a means of
avoiding proof difficulties that can arise from the use of explicit
quantification (via <code><a href="DEFUN-SK.html">defun-sk</a></code>). See <a href="QUANTIFIERS.html">quantifiers</a> for more about
the context of this example.
<p>
<pre>
(in-package "ACL2")<p>
; We prove that if every member A of each of two lists satisfies the
; predicate (P A), then this holds of their append; and, conversely.<p>
; Here is a solution using recursively-defined functions.<p>
(defstub p (x) t)<p>
(defun all-p (x)
(if (atom x)
t
(and (p (car x))
(all-p (cdr x)))))<p>
(defthm all-p-append
(equal (all-p (append x1 x2))
(and (all-p x1) (all-p x2))))
</pre>
<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>
|
