` `

apply a linear rule
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)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 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 `n`

th 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.