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
|
<html>
<head><title>ACL2-PC_colon__colon_=.html -- ACL2 Version 3.1</title></head>
<body text=#000000 bgcolor="#FFFFFF">
<h3>ACL2-PC::=</h3>(atomic macro)
<code> </code>attempt an equality (or equivalence) substitution
<pre>Major Section: <a href="PROOF-CHECKER-COMMANDS.html">PROOF-CHECKER-COMMANDS</a>
</pre><p>
<pre>
Examples:
= -- replace the current subterm by a term equated to it in
one of the hypotheses (if such a term exists)
(= x) -- replace the current subterm by x, assuming that the prover
can show that they are equal
(= (+ x y) z)
-- replace the term (+ x y) by the term z inside the current
subterm, assuming that the prover can prove
(equal (+ x y) z) from the current top-level hypotheses
or that this term or (equal z (+ x y)) is among the
current top-level hypotheses or the current governors
(= & z)
-- exactly the same as above, if (+ x y) is the current
subterm
(= (+ x y) z :hints :none)
-- same as (= (+ x y) z), except that a new subgoal is
created with the current goal's hypotheses and governors
as its top-level hypotheses and (equal (+ x y) z) as its
conclusion
(= (+ x y) z 0)
-- exactly the same as immediately above
(= (p x)
(p y)
:equiv iff
:otf-flg t
:hints (("Subgoal 2" :BY FOO) ("Subgoal 1" :use bar)))
-- same as (= (+ x y) z), except that the prover uses
the indicated values for otf-flg and hints, and only
propositional (iff) equivalence is used (however, it
must be that only propositional equivalence matters at
the current subterm)
<p>
General Form:
(= &optional x y &rest keyword-args)
</pre>
If terms <code>x</code> and <code>y</code> are supplied, then replace <code>x</code> by <code>y</code> inside the
current subterm if they are ``known'' to be ``equal''. Here
``known'' means the following: the prover is called as in the <code>prove</code>
command (using <code>keyword-args</code>) to prove <code>(equal x y)</code>, except that a
keyword argument <code>:equiv</code> is allowed, in which case <code>(equiv x y)</code> is
proved instead, where <code>equiv</code> is that argument. (See below for how
governors are handled.)<p>
Actually, <code>keyword-args</code> is either a single non-keyword or is a list
of the form <code>((kw-1 x-1) ... (kw-n x-n))</code>, where each <code>kw-i</code> is one of
the keywords <code>:equiv</code>, <code>:otf-flg</code>, <code>:hints</code>. Here <code>:equiv</code> defaults to
<code>equal</code> if the argument is not supplied or is <code>nil</code>, and otherwise
should be the name of an ACL2 equivalence relation. <code>:Otf-flg</code> and
<code>:hints</code> give directives to the prover, as explained above and in the
documentation for the <code>prove</code> command; however, no prover call is made
if <code>:hints</code> is a non-<code>nil</code> atom or if <code>keyword-args</code> is a single
non-keyword (more on this below).<p>
<em>Remarks on defaults</em><p>
(1) If there is only one argument, say <code>a</code>, then <code>x</code> defaults to the
current subterm, in the sense that <code>x</code> is taken to be the current
subterm and <code>y</code> is taken to be <code>a</code>.<p>
(2) If there are at least two arguments, then <code>x</code> may be the symbol
<code>&</code>, which then represents the current subterm. Thus, <code>(= a)</code> is
equivalent to <code>(= & a)</code>. (Obscure point: actually, <code>&</code> can be in any
package, except the keyword package.)<p>
(3) If there are no arguments, then we look for a top-level
hypothesis or a governor of the form <code>(equal c u)</code> or <code>(equal u c)</code>,
where <code>c</code> is the current subterm. In that case we replace the current
subterm by <code>u</code>.<p>
As with the <code>prove</code> command, we allow goals to be given ``bye''s in
the proof, which may be generated by a <code>:hints</code> keyword argument in
<code>keyword-args</code>. These result in the creation of new subgoals.<p>
A proof is attempted unless the <code>:hints</code> argument is a non-<code>nil</code>
atom other than :<code>none</code>, or unless there is one element of
<code>keyword-args</code> and it is not a keyword. In that case, if there are
any hypotheses in the current goal, then what is attempted is a
proof of the implication whose antecedent is the conjunction of the
current hypotheses and governors and whose conclusion is the
appropriate <code>equal</code> term.<p>
<strong>Notes:</strong> (1) It is allowed to use abbreviations in the hints.
(2) The keyword :<code>none</code> has the special role as a value of
:<code>hints</code> that is shown clearly in an example above. (3) If there
are governors, then the new subgoal has as additional hypotheses the
current governors.
<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>
|
