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
|
<html>
<head><title>FUNCTIONAL-INSTANTIATION-EXAMPLE.html -- ACL2 Version 3.1</title></head>
<body text=#000000 bgcolor="#FFFFFF">
<h4>FUNCTIONAL-INSTANTIATION-EXAMPLE</h4>a small proof demonstrating functional instantiation
<pre>Major Section: <a href="TUTORIAL5-MISCELLANEOUS-EXAMPLES.html">TUTORIAL5-MISCELLANEOUS-EXAMPLES</a>
</pre><p>
The example below demonstrates the use of functional instantiation,
that is, the use of a generic result in proving a result about
specific functions. In this example we constrain a function to be
associative and commutative, with an identity or ``root,'' on a
given domain. Next, we define a corresponding function that applies
the constrained associative-commutative function to successive
elements of a list. We then prove that the latter function gives
the same value when we first reverse the elements of the list.
Finally, we use functional instantiation to derive the corresponding
result for the function that multiplies successive elements of a
list.<p>
Also see <a href="CONSTRAINT.html">constraint</a> for more about <code>:functional-instance</code> and
see <a href="LEMMA-INSTANCE.html">lemma-instance</a> for general information about the use of
previously-proved lemmas.
<p>
<pre>
(in-package "ACL2")<p>
(encapsulate
(((ac-fn * *) => *)
((ac-fn-domain *) => *)
((ac-fn-root) => *))
(local (defun ac-fn (x y) (+ x y)))
(local (defun ac-fn-root () 0))
(local (defun ac-fn-domain (x) (acl2-numberp x)))
(defthm ac-fn-comm
(equal (ac-fn x y)
(ac-fn y x)))
(defthm ac-fn-assoc
(equal (ac-fn (ac-fn x y) z)
(ac-fn x (ac-fn y z))))
(defthm ac-fn-id
(implies (ac-fn-domain x)
(equal (ac-fn (ac-fn-root) x)
x)))
(defthm ac-fn-closed
(and (ac-fn-domain (ac-fn x y))
(ac-fn-domain (ac-fn-root)))))<p>
(defun ac-fn-list (x)
(if (atom x)
(ac-fn-root)
(ac-fn (car x)
(ac-fn-list (cdr x)))))<p>
(in-theory (disable (ac-fn-list)))<p>
(defun ac-fn-domain-list (x)
(if (atom x)
t
(and (ac-fn-domain (car x))
(ac-fn-domain-list (cdr x)))))<p>
(defun rev (x)
(if (atom x)
nil
(append (rev (cdr x))
(list (car x)))))<p>
(defthm ac-fn-list-closed
(ac-fn-domain (ac-fn-list x)))<p>
(defthm ac-fn-list-append
(implies (and (ac-fn-domain-list x)
(ac-fn-domain-list y))
(equal (ac-fn-list (append x y))
(ac-fn (ac-fn-list x)
(ac-fn-list y)))))<p>
(defthm ac-fn-domain-list-rev
(equal (ac-fn-domain-list (rev x))
(ac-fn-domain-list x)))<p>
(defthm ac-fn-list-rev
(implies (ac-fn-domain-list x)
(equal (ac-fn-list (rev x))
(ac-fn-list x))))<p>
(defun times-list (x)
(if (atom x)
1
(* (car x)
(times-list (cdr x)))))<p>
(defun acl2-number-listp (x)
(if (atom x)
t
(and (acl2-numberp (car x))
(acl2-number-listp (cdr x)))))<p>
(defthm times-list-rev
(implies (acl2-number-listp x)
(equal (times-list (rev x))
(times-list x)))
:hints (("Goal"
:use
((:functional-instance
ac-fn-list-rev
;; Instantiate the generic functions:
(ac-fn (lambda (x y) (* x y)))
(ac-fn-root (lambda () 1))
(ac-fn-domain acl2-numberp)
;; Instantiate the other relevant functions:
(ac-fn-list times-list)
(ac-fn-domain-list acl2-number-listp))))))
</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>
|
