:definition and :rewrite rules used in preprocessing
Major Section: MISCELLANEOUS
Example of simple rewrite rule: (equal (car (cons x y)) x) Examples of simple definition: (defun file-clock-p (x) (integerp x)) (defun naturalp (x) (and (integerp x) (>= x 0)))
The theorem prover output sometimes refers to ``simple'' definitions
and rewrite rules. These rules can be used by the preprocessor,
which is one of the theorem prover's ``processes'' understood by the
:do-not hint; see hints.
The preprocessor expands certain definitions and uses certain
rewrite rules that it considers to be ``fast''. There are two ways
to qualify as fast. One is to be an ``abbreviation'', where a
rewrite rule with no hypotheses or loop stopper is an
``abbreviation'' if the right side contains no more variable
occurrences than the left side, and the right side does not call the
functions if , not or implies . Definitions and rewrite rules can
both be abbreviations; the criterion for definitions is similar,
except that the definition must not be recursive. The other way to
qualify applies only to a non-recursive definition, and applies when
its body is a disjunction or conjunction, according to a perhaps
subtle criterion that is intended to avoid case splits.