ACL2-PC::APPLY-LINEAR

Major Section:  PROOF-CHECKER-COMMANDS

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)

A short name for this command is al.

We assume familiarity with the proof-checker's rewrite (r) command. 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 proof-checker's rewrite command.

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 proof-checker 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.