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
|
<html>
<head><title>ACL2-PC_colon__colon_EQUIV.html -- ACL2 Version 3.1</title></head>
<body text=#000000 bgcolor="#FFFFFF">
<h3>ACL2-PC::EQUIV</h3>(primitive)
<code> </code>attempt an equality (or congruence-based) substitution
<pre>Major Section: <a href="PROOF-CHECKER-COMMANDS.html">PROOF-CHECKER-COMMANDS</a>
</pre><p>
<pre>
Examples:
(equiv (* x y) 3) -- replace (* x y) by 3 everywhere inside the
current subterm, if their equality is among the
top-level hypotheses or the governors
(equiv x t iff) -- replace x by t everywhere inside the current
subterm, where only propositional equivalence
needs to be maintained at each occurrence of x
<p>
General form:
(equiv old new &optional relation)
</pre>
Substitute new for old everywhere inside the current subterm,
provided that either (relation old new) or (relation new old) is
among the top-level hypotheses or the governors (possibly by way of
backchaining and/or refinement; see below). If relation is <code>nil</code> or
is not supplied, then it defaults to <code>equal</code>. See also the command <code>=</code>,
which is much more flexible. Note that this command fails if no
substitution is actually made.<p>
<strong>Note:</strong> No substitution takes place inside explicit values. So for
example, the instruction <code>(equiv 3 x)</code> will cause <code>3</code> to be replaced by
<code>x</code> if the current subterm is, say, <code>(* 3 y)</code>, but not if the current
subterm is <code>(* 4 y)</code> even though <code>4 = (1+ 3)</code>.<p>
The following remarks are quite technical and mostly describe a
certain weak form of ``backchaining'' that has been implemented for
<code>equiv</code> in order to support the <code>=</code> command. In fact neither the term
<code>(relation old new)</code> nor the term <code>(relation new old)</code> needs to be
<strong>explicitly</strong> among the current ``assumptions'', i.e., the top-level
hypothesis or the governors. Rather, there need only be such an
assumption that ``tells us'' <code>(r old new)</code> or <code>(r new old)</code>, for <strong>some</strong>
equivalence relation <code>r</code> that <strong>refines</strong> <code>relation</code>. Here, ``tells us''
means that either one of the indicated terms is among those
assumptions, or else there is an assumption that is an implication
whose conclusion is one of the indicated terms and whose hypotheses
(gathered up by appropriately flattening the first argument of the
<code>implies</code> term) are all among the current assumptions.
<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>
|
