Major Section: RULE-CLASSES

See rule-classes for a general discussion of rule classes, including how they are used to build rules from formulas and a discussion of the various keywords in a rule class description.

Example: (defthm length-member-leq-length If inequality reasoning begins to (implies (and (eqlablep e) consider how (length (member a b)) (true-listp x)) compares to any other term, add to (<= (length (member e x)) the set of known inequalities the fact (length x))) that it is no larger than (length b), :rule-classes :linear) provided (eqlablep a) and (true-listp b) rewrite to t. General Form: (and ... (implies (and ...hi...) (implies (and ...hk...) (and ... (rel lhs rhs) ...))) ...)

Note: One `:linear`

rule class object might create many linear arithmetic
rules from the `:`

`corollary`

formula. To create the rules, we first
flatten the `and`

and `implies`

structure of the formula,
transforming it into a conjunction of formulas, each of the form

(implies (and h1 ... hn) (rel lhs rhs))where no hypothesis is a conjunction and

`rel`

is one of the inequality
relations `<`

, `<=`

, `=`

, `>`

, or `>=`

. If necessary,
the hypothesis of such a conjunct may be vacuous. We create a `:linear`

rule for each such conjunct, if possible, and otherwise cause an error.
Each rule has one or more ``trigger terms'' which may be specified by the
user using the `:trigger-terms`

field of the rule class or which may be
defaulted to values chosen by the system. We discuss the determination of
trigger terms after discussing how linear rules are used.

`:Linear`

rules are used by an arithmetic decision procedure during
rewriting. See linear-arithmetic and see non-linear-arithmetic. Here we
assume that the reader is familiar with the material described in
`linear-arithmetic`

.

Recall that we eliminate the unknowns of an inequality in term-order, largest
unknowns first. (See term-order.) In order to facilitate this strategy, we
store the inequalities in ``linear pots''. For purposes of the present
discussion, let us say that an inequality is ``about'' its largest unknown.
Then, all of the inequalities about a particular unknown are stored in the
same linear pot, and the pot is said to be ``labeled'' with that unknown.
This storage layout groups all of the inequalities which are potential
candidates for cancellation with each other into one place. It is also key
to the efficient operation of `:linear`

rules.

If the arithmetic decision procedure has stabilized and not yielded a
contradiction, we scan through the list of linear pots examining each label
as we go. If the trigger term of some `:linear`

rule can be instantiated
to match the label, we so instantiate that rule and attempt to relieve the
hypotheses with general-purpose rewriting. If we are successful, we add the
rule's instantiated conclusion to our set of inequalities. This may let
cancellation continue.

Note: Problems may arise if you explicitly store a linear lemma under a
trigger term that, when instantiated, is not the largest unknown in the
instantiated concluding inequality. Suppose for example you store the linear
rule `(<= (fn i j) (/ i (* j j)))`

under the trigger term `(fn i j)`

.
Then when the system ``needs'' an inequality about `(fn a b)`

, (i.e.,
because `(fn a b)`

is the label of some linear pot, and hence the largest
unknown in some inequality), it will appeal to the rule and deduce
`(<= (fn a b) (/ a (* b b)))`

. However, the largest unknown in this
inequality is `(/ a (* b b))`

and hence it will be stored in a linear pot
labeled with `(/ a (* b b))`

. The original, triggering inequality which is
in a pot about `(fn a b)`

will therefore not be cancelled against the new
one. It is generally best to specify as a trigger term one of the
``maximal'' terms of the polynomial, as described below.

We now describe how the trigger terms are determined. Most of the time, the
trigger terms are not specified by the user and are instead selected by the
system. However, the user may specify the terms by including an explicit
`:trigger-terms`

field in the rule class, e.g.,

General Form of a Linear Rule Class: (:LINEAR :COROLLARY formula :TRIGGER-TERMS (term1 ... termk))Each

`termi`

must be a term and must not be a variable, quoted constant,
lambda application, `let-expression`

or `if-expression`

. In addition,
each `termi`

must be such that if all the variables in the term are
instantiated and then the hypotheses of the corollary formula are relieved
(possibly instantiating additional free variables), then all the variables in
the concluding inequality are instantiated. We generate a linear rule for
each conjuctive branch through the corollary and store each rule under each
of the specified triggers. Thus, if the corollary formula contains several
conjuncts, the variable restrictions on the `termi`

must hold for each
conjunct.If `:trigger-terms`

is omitted the system computes a set of trigger terms.
Each conjunct of the corollary formula may be given a unique set of triggers
depending on the variables that occur in the conjunct and the addends that
occur in the concluding inequality. In particular, the trigger terms for a
conjunct is the list of all ``maximal addends'' in the concluding inequality.

The ``addends'' of `(+ x y)`

and `(- x y)`

are the union of the addends
of `x`

and `y`

. The addends of `(- x)`

and `(* n x)`

, where `n`

is
a rational constant, is just `{x}`

. The addends of an inequality are the
union of the addends of the left- and right-hand sides. The addends of any
other term, `x`

, is `{x}`

.

A term is maximal for a conjunct `(implies hyps concl)`

of the corollary if
(a) the term is a non-variable, non-quote, non-lambda application,
non-`let`

and non-`if`

expression, (b) the term contains enough
variables so that when they are instantiated and the hypotheses are relieved
(which may bind some free variables; see free-variables) then all the
variables in `concl`

are instantiated, and (c) no other addend is always
``bigger'' than the term, in the technical sense described below.

The technical notion referenced above depends on the notion of *fn-count*,
the number of function symbols in a term, and *pseudo-fn-count*, which is
essentially the number of function symbols implicit in a constant
(see term-order, specifically the discussion of ``pseudo-function
application count'' at the end). We say `term1`

is always bigger than
`term2`

if all instances of `term1`

have a larger fn-count (actually
lexicographic order of fn-count and pseudo-fn-count) than the corresponding
instances of `term2`

. This is equivalent to saying that the fn-count of
`term1`

is larger than that of `term2`

(by ``fn-count'' here we mean the
lexicographic order of fn-count and pseudo-fn-count) and the variable bag for
`term2`

is a subbag of that for `term1`

. For example, `(/ a (* b b))`

is always bigger than `(fn a b)`

because the first has two function
applications and `{a b}`

is a subbag of `a b b`

, but `(/ a (* b b))`

is
not always bigger than `(fn a x)`

.