ACL2-pc::apply-linear
(primitive)
apply a linear rule
Examples:
(apply-linear foo)
-- apply the linear rule `foo'
(apply-linear (:linear foo))
-- same as above
(apply-linear 2)
-- apply the second linear rule, as displayed by show-linears
rewrite
-- apply the first rewrite rule, as displayed by show-rewrites
(apply-linear foo ((y 7)))
-- apply the linear rule foo with the substitution
that associates 7 to the ``free variable'' y
(apply-linear foo ((x 2) (y 3)) t)
-- apply the linear rule foo by substituting 2 and 3 for free
variables x and y, respectively, and also binding all other
free variables possible by using the current context
(hypotheses and governors)
General Form:
(apply-linear &optional rule-id substitution instantiate-free)
Add a new top-level hypothesis by applying a linear rule to the
current subterm. The new hypothesis will be created according to the
information provided by the show-linears (sls) command.
A short name for this command is al.
We assume familiarity with the interactive proof-builder's
rewrite (r) command (see ACL2-pc::rewrite). In brief, the
apply-linear command is an analogue of the rewrite command, but for
linear rules in place of rewrite rules. There is a significant
difference: for the apply-linear command, instead of rewriting the
current subterm as is done by the rewrite command, the conclusion of the
applicable linear rule, suitably instantiated, is added as a new (and last)
top-level hypothesis of the goal. There is another significant difference:
the automatic application of linear rules in the theorem prover is
somewhat more complex than the automatic application of rewrite rules,
so the apply-linear command may not correspond as closely to the prover's
automatic use of a linear rule as the rewrite command corresponds to the
prover's automatic use of a rewrite rule.
Below, we refer freely to the documentation for the interactive
proof-builder's rewrite command (see ACL2-pc::rewrite).
The rule-id is treated just as it is by the rewrite command. If
rule-id is a positive integer n, then the nth rule as displayed
by show-linears is the one that is applied. If rule-id is nil
or is not supplied, then it is treated as the number 1. Otherwise,
rule-id should be either a symbol or else a :linear rune. If
a symbol is supplied, then any linear rule of that name may be
used.
Consider the following example. Suppose that the current subterm is (<
(g (h y)) y) and that foo is the name of the following linear rule.
(implies (true-listp x)
(< (g x) 15))
Then the instruction (apply-linear foo) applies foo by adding a
new hypothesis (< (g (h y)) 15). In addition, a new goal with conclusion
(true-listp y) is created unless the current context (top-level
hypotheses and governors) implies (true-listp y) using only ``trivial
reasoning'', just as for the rewrite command.
If the rule-id argument is a number or is not supplied, then the
system will store an instruction of the form (apply-linear name ...),
where name is the name of a linear rule; this is in order to make
it easier to replay instructions when there have been changes to the history.
Except: instead of the name (whether the name is supplied or calculated), the
system stores the rune if there is any chance of ambiguity. (Formally,
``ambiguity'' here means that the rune being applied is of the form
(:rewrite name . index), where index is not nil.)
Speaking in general, then, an apply-linear instruction works as
follows.
First, a linear rule is selected according to the arguments of the
instruction. The selection is made as explained under ``General Form''
above.
Next, a trigger term of the rule (see linear) is matched with the
current subterm, i.e., a substitution unify-subst is found such that if
one instantiates that trigger term of the rule with unify-subst, then one
obtains the current subterm. If this match fails, then the instruction
fails.
Next, an attempt is made to relieve (discharge) the hypotheses, possibly
handling free variables (see free-variables), exactly as is done with
hypotheses when applying the interactive proof-builder command,
rewrite (r).
Finally, the instruction is applied exactly as the rewrite instruction
is applied, except instead of replacing the current subterm, the rule's
instantiated conclusion is added to the end of the list of top-level
hypotheses of the goal.
Note that as for the rewrite command, the substitution argument should
be a list whose elements have the form (variable term), where term
may contain abbreviations.
