ACL2-pc::=
(atomic macro)
attempt an equality (or equivalence) substitution
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 all occurrences of 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)
General Forms:
(= x)
(= x y)
(= x y :kwd1 val1 ... :kwdn valn)
(= x y atom :kwd1 val1 ... :kwdn valn)
where each :kwdi is one of :hints, :otf-flg, or :equiv,
without repetition. In the last form, atom is a non-keyword atom and no
kwdi may be :hints; that atom, if supplied, is equivalent to
:hints atom, which indicates that instead of performing a proof that the
two indicated terms (as described below) are suitably equivalent, a new such
goal is created.
If terms x and y are supplied, then replace x by y
everywhere inside the current subterm if they are ``known'' to be equal, or
more generally, equivalent in the sense described below. Here ``known'' means
the following: except in the cases that no arguments are provided or else
:hints atom is provided as described above, the prover is called as in
the prove command (using keyword arguments :otf and :hints, if
supplied, where the value of :hints is not an atom) to prove equivalence
of x and y under the current governors and top-level hypotheses. By
default, this equivalence is equality; however the keyword argument
:equiv can specify a known equivalence relation. In cases other than
equality, substitution only takes place where justified by the equivlance
maintained at the current subterm.
For the keyword arguments, :equiv defaults to equal if not
supplied or nil; if it is not equal (either explicitly or by
default), then it should be the name of a known ACL2 equivalence
relation, and substitution will only take place at subterm occurrences for
which the :equiv is among the equivalence relations being
maintained without the use of patterned-congruences.
Remarks on defaults
- If there are at least two arguments, then x may be the symbol
&, in any package except the keyword package, which represents the
current subterm.
- The one-argument command (= a) is equivalent to (= & a).
- If there are no arguments, then we look for a top-level hypothesis or a
governor of the form (equal c u) or (equal u c), where c is the
current subterm. In that case we replace the current subterm by u.
- As with the prove command, we allow goals to be given ``bye''s in the
proof, which may be generated by a :hints keyword argument in
keyword-args. These result in the creation of new subgoals.
- It is allowed to use abbreviations (see ACL2-pc::add-abbreviation)
in the hints.
