Major Section: RULE-CLASSES

See rule-classes for a general discussion of rule classes and
how they are used to build rules from formulas. An example
`:`

`corollary`

formula from which a `:refinement`

rule might be built is:

Example: (implies (bag-equal x y) (set-equal y x)).Also see defrefinement.

General Form: (implies (equiv1 x y) (equiv2 x y))

`Equiv1`

and `equiv2`

must be known equivalence relations. The effect
of such a rule is to record that `equiv1`

is a refinement of `equiv2`

.
This means that `equiv1`

`:`

`rewrite`

rules may be used while trying to
maintain `equiv2`

. See equivalence for a general discussion of
the issues.
The macro form `(defrefinement equiv1 equiv2)`

is an abbreviation for
a `defthm`

of rule-class `:refinement`

that establishes that `equiv1`

is a
refinement of `equiv2`

. See defrefinement.

Suppose we have the `:`

`rewrite`

rule

(bag-equal (append a b) (append b a))which states that

`append`

is commutative modulo bag-equality.
Suppose further we have established that bag-equality refines
set-equality. Then when we are simplifying `append`

expressions while
maintaining set-equality we use `append`

's commutativity property,
even though it was proved for bag-equality.
Equality is known to be a refinement of all equivalence relations.
The transitive closure of the refinement relation is maintained, so
if `set-equality`

, say, is shown to be a refinement of some third
sense of equivalence, then `bag-equality`

will automatially be known
as a refinement of that third equivalence.

`:refinement`

lemmas cannot be disabled. That is, once one
equivalence relation has been shown to be a refinement of another,
there is no way to prevent the system from using that information.
Of course, individual `:`

`rewrite`

rules can be disabled.

More will be written about this as we develop the techniques.

`:rewrite`

rules (possibly conditional ones)
Major Section: RULE-CLASSES

See rule-classes for a general discussion of rule classes and
how they are used to build rules from formulas. Example `:`

`corollary`

formulas from which `:rewrite`

rules might be built are:

Example: (equal (+ x y) (+ y x)) replace (+ a b) by (+ b a) provided certain heuristics approve the permutation.Note: One(implies (true-listp x) replace (append a nil) by a, if (equal (append x nil) x)) (true-listp a) rewrites to t

(implies replace (member a (append b c)) by (and (eqlablep e) (member a (append c b)) in contexts (true-listp x) in which propositional equivalence (true-listp y)) is sufficient, provided (eqlablep a) (iff (member e (append x y)) (true-listp b) and (true-listp c) (member e (append y x)))) rewrite to t and the permutative heuristics approve

General Form: (and ... (implies (and ...hi...) (implies (and ...hk...) (and ... (equiv lhs rhs) ...))) ...)

`:rewrite`

rule class object might create many rewrite
rules from the `:`

`corollary`

formula. To create the rules, we first
translate the formula (expanding all macros; also see trans).
Next, we eliminate all `lambda`

s; one may think of this step as
simply substituting away every `let`

, `let*`

, and `mv-let`

in the
formula. We then flatten the `and`

and `implies`

structure of the
formula, transforming it into a conjunction of formulas, each of the
form
(implies (and h1 ... hn) concl)where no hypothesis is a conjunction and

`concl`

is neither a
conjunction nor an implication. If necessary, the hypothesis of
such a conjunct may be vacuous. We then further coerce each `concl`

into the form `(equiv lhs rhs)`

, where `equiv`

is a known equivalence
relation, by replacing any `concl`

not of that form by `(iff concl t)`

.
A `concl`

of the form `(not term)`

is considered to be of the form
`(iff term nil)`

. By these steps we reduce the given `:`

`corollary`

to
a sequence of conjuncts, each of which is of the form
(implies (and h1 ... hn) (equiv lhs rhs))where

`equiv`

is a known equivalence relation. See equivalence
for a general discussion of the introduction of new equivalence
relations.
We create a `:rewrite`

rule for each such conjunct, if possible, and
otherwise cause an error. It is possible to create a rewrite rule
from such a conjunct provided `lhs`

is not a variable, a quoted
constant, or an `if`

-expression.

A `:rewrite`

rule is used when any instance of the `lhs`

occurs in a
context in which the equivalence relation is operative. First, we
find a substitution that makes `lhs`

equal to the target term. Then
we attempt to relieve the instantiated hypotheses of the rule.
Hypotheses that are fully instantiated are relieved by recursive
rewriting. Hypotheses that contain ``free variables'' (variables
not assigned by the unifying substitution) are relieved by
attempting to guess a suitable instance so as to make the hypothesis
equal to some known assumption in the context of the target. If the
hypotheses are relieved, and certain restrictions that prevent some
forms of infinite regress are met (see loop-stopper), the
target is replaced by the instantiated `rhs`

, which is then
recursively rewritten.

At the moment, the best description of how ACL2 `:rewrite`

rules are
used may be found in the discussion of ``Replacement Rules'' pp 234
of A Computational Logic Handbook.

Major Section: RULE-CLASSES

See rule-classes for a general discussion of rule classes and
how they are used to build rules from formulas. Some example
`:`

`corollary`

formulas from which `:type-prescription`

rules might be
built are:

Examples: (implies (nth n lst) is of type characterp (and (character-listp lst) provided the two hypotheses can (< n (length lst))) be established by type reasoning (characterp (nth n lst))).To specify the term whose type (see type-set) is described by the rule, provide that term as the value of the(implies (demodulize a lst 'value ans) is (and (atom a) either a nonnegative integer or (true-listp lst) of the same type as ans, provided (member-equal a lst)) the hyps can be established by type (or (and reasoning (integerp (demodulize a lst 'value ans)) (>= (demodulize a lst 'value ans) 0)) (equal (demodulize a lst 'value ans) ans))).

`:typed-term`

field
of the rule class object.

General Form: (implies hyps (or type-restriction1-on-pat ... type-restrictionk-on-pat (equal pat var1) ... (equal pat varj)))where

`pat`

is the application of some function symbol to some
arguments, each `type-restrictioni-on-pat`

is a term involving `pat`

and
containing no variables outside of the occurrences of `pat`

, and each
`vari`

is one of the variables of `pat`

. Generally speaking, the
`type-restriction`

terms ought to be terms that inform us as to the
type of `pat`

. Ideally, they should be ``primitive recognizing
expressions'' about `pat`

; see compound-recognizer.
If the `:typed-term`

is not provided in the rule class object, it is
computed heuristically by looking for a term in the conclusion whose
type is being restricted. An error is caused if no such term is
found.

Roughly speaking, the effect of adding such a rule is to inform the
ACL2 typing mechanism that `pat`

has the type described by the
conclusion, when the hypotheses are true. In particular, the type
of `pat`

is within the union of the types described by the several
disjuncts. The ``type described by'' `(equal pat vari)`

is the type
of `vari`

.

More operationally, when asked to determine the type of a term that
is an instance of `pat`

, ACL2 will first attempt to establish the
hypotheses. **This is done by type reasoning alone, not rewriting!**
Of course, if some hypothesis is to be forced, it is so
treated; see force and see case-split. Provided the
hypotheses are established by type reasoning, ACL2 then unions the
types described by the `type-restrictioni-on-pat`

terms together
with the types of those subexpressions of `pat`

identified by the
`vari`

. The final type computed for a term is the intersection of
the types implied by each applicable rule. Type prescription rules
may be disabled.

Because only type reasoning is used to establish the hypotheses of
`:type-prescription`

rules, some care must be taken with the
hypotheses. Suppose, for example, that the non-recursive function
`my-statep`

is defined as

(defun my-statep (x) (and (true-listp x) (equal (length x) 2)))and suppose

`(my-statep s)`

occurs as a hypothesis of a
`:type-prescription`

rule that is being considered for use in the
proof attempt for a conjecture with the hypothesis `(my-statep s)`

.
Since the hypothesis in the conjecture is rewritten, it will become
the conjunction of `(true-listp s)`

and `(equal (length s) 2)`

.
Those two terms will be assumed to have type `t`

in the context in
which the `:type-prescription`

rule is tried. But type reasoning will
be unable to deduce that `(my-statep s)`

has type `t`

in this
context. Thus, either `my-statep`

should be disabled
(see disable) during the proof attempt or else the occurrence
of `(my-statep s)`

in the `:type-prescription`

rule should be
replaced by the conjunction into which it rewrites.
While this example makes it clear how non-recursive predicates can
cause problems, non-recursive functions in general can cause
problems. For example, if `(mitigate x)`

is defined to be
`(if (rationalp x) (1- x) x)`

then the hypothesis
`(pred (mitigate s))`

in the conjecture will rewrite, opening
`mitigate`

and splitting the conjecture into two subgoals, one in
which `(rationalp s)`

and `(pred (1- x))`

are assumed and the
other in which `(not (rationalp s))`

and `(pred x)`

are assumed.
But `(pred (mitigate s))`

will not be typed as `t`

in either of
these contexts. The moral is: beware of non-recursive functions
occuring in the hypotheses of `:type-prescription`

rules.

Because of the freedom one has in forming the conclusion of a
type-prescription, we have to use heuristics to recover the pattern,
`pat`

, whose type is being specified. In some cases our heuristics
may not identify the intended term and the `:type-prescription`

rule will be rejected as illegal because the conclusion is not of
the correct form. When this happens you may wish to specify the `pat`

directly. This may be done by using a suitable rule class token.
In particular, when the token `:type-prescription`

is used it means
ACL2 is to compute pat with its heuristics; otherwise the token
should be of the form `(:type-prescription :typed-term pat)`

, where
`pat`

is the term whose type is being specified.

The defun event may generate a `:type-prescription`

rule. Suppose
`fn`

is the name of the function concerned. Then
`(:type-prescription fn)`

is the rune given to the
type-prescription, if any, generated for `fn`

by `defun`

. (The
trivial rule, saying `fn`

has unknown type, is not stored, but
`defun`

still allocates the rune and the corollary of this rune is
known to be `t`

.)

Major Section: RULE-CLASSES

See rule-classes for a general discussion of rule classes and how they are used to build rules from formulas.

Example Rule Class: (:type-set-inverter :corollary (equal (and (counting-number x) (not (equal x 0))) (and (integerp x) (< x 0))) :type-set 2)whereGeneral Forms of Rule Class: :type-set-inverter, or (:type-set-inverter :type-set n)

General Form of Theorem or Corollary: (EQUAL new-expr old-expr)

`n`

is a `type-set`

(see type-set) and `old-expr`

is the term
containing `x`

as a free variable that ACL2 currently uses to
recognize `type-set`

`n`

. For a given `n`

, the exact form of `old-expr`

is
generated by
(convert-type-set-to-term 'x n (ens state) (w state) nil)].

If the `:`

`type-set`

field of the rule-class is omitted, we attempt to
compute it from the right-hand side, `old-expr`

, of the corollary.
That computation is done by `type-set-implied-by-term`

(see type-set). However, it is possible that the type-set we
compute from `lhs`

does not have the required property that when
inverted with `convert-type-set-to-term`

the result is `lhs`

. If you
omit `:`

`type-set`

and an error is caused because `lhs`

has the incorrect
form, you should manually specify both `:`

`type-set`

and the `lhs`

generated by `convert-type-set-to-term`

.

The rule generated will henceforth make `new-expr`

be the term used by
ACL2 to recognize type-set `n`

. If this rule is created by a `defthm`

event named `name`

then the rune of the rule is
`(:type-set-inverter name)`

and by disabling that rune you can
prevent its being used to decode type-sets.

Type-sets are inverted when forced assumptions are turned into
formulas to be proved. In their internal form, assumptions are
essentially pairs consisting of a context and a goal term, which was
forced. Abstractly a context is just a list of hypotheses which may
be assumed while proving the goal term. But actually contexts are
alists which pair terms with type-sets, encoding the current
hypotheses. For example, if the original conjecture contained the
hypothesis `(integerp x)`

then the context used while working on that
conjecture will include the assignment to `x`

of the type-set
`*ts-integer*`

.

Major Section: RULE-CLASSES

See rule-classes for a general discussion of rule classes and
how they are used to build rules from formulas. An example
`:`

`corollary`

formula from which a `:well-founded-relation`

rule might be
built is as follows. (Of course, the functions `pairp`

, `lex2p`

, and
`ordinate`

would have to be defined first.)

Example: (and (implies (pairp x) (e0-ordinalp (ordinate x))) (implies (and (pairp x) (pairp y) (lex2p x y)) (e0-ord-< (ordinate x) (ordinate y))))The above example establishes that

`lex2p`

is a well-founded
relation on `pairp`

s. We explain and give details below.
Exactly two general forms are recognized:

General Forms (AND (IMPLIES (mp x) (E0-ORDINALP (fn x))) ; Property 1 (IMPLIES (AND (mp x) ; Property 2 (mp y) (rel x y)) (E0-ORD-< (fn x) (fn y)))),or

(AND (E0-ORDINALP (fn x)) ; Property 1 (IMPLIES (rel x y) ; Property 2 (E0-ORD-< (fn x) (fn y))))where

`mp`

, `fn`

, and `rel`

are function symbols, `x`

and `y`

are distinct
variable symbols, and no other `:well-founded-relation`

theorem about
`fn`

has been proved. When the second general form is used, we act as
though the first form were used with `mp`

being the function that
ignores its argument and returns `t`

. The discussion below therefore
considers only the first general form.
Note: We are very rigid when checking that the submitted formula is
of one of these forms. For example, in the first form, we insist
that all the conjuncts appear in the order shown above. Thus,
interchanging the two properties in the top-level conjunct or
rearranging the hyptheses in the second conjunct both produce
unrecognized forms. The requirement that each `fn`

be proved
well-founded at most once insures that for each well-founded
relation, `fn`

, there is a unique `mp`

that recognizes the domain on
which `rel`

is well-founded. We impose this requirement simply so
that `rel`

can be used as a short-hand when specifying the
well-founded relations to be used in definitions; otherwise the
specification would have to indicate which `mp`

was to be used.

`Mp`

is a predicate that recognizes the objects that are supposedly
ordered in a well-founded way by `rel`

. We call such an object an
```mp`

-measure'' or simply a ``measure'' when `mp`

is understood.
Property 1 tells us that every measure can be mapped into an ACL2
ordinal. (See e0-ordinalp.) This mapping is performed by `fn`

.
Property 2 tells us that if the measure `x`

is smaller than the
measure `y`

according to `rel`

then the image of `x`

under `fn`

is a smaller
than that of `y`

, according to the well-founded relation `e0-ord-<`

.
(See e0-ord-<.) Thus, the general form of a
`:well-founded-relation`

formula establishes that there exists a
`rel`

-order preserving embedding (namely via `fn`

) of the `mp`

-measures
into the ordinals. We can thus conclude that `rel`

is well-founded on
`mp`

-measures.

Such well-founded relations are used in the admissibility test for recursive functions, in particular, to show that the recursion terminates. To illustrate how such information may be used, consider a generic function definition

(defun g (x) (if (test x) (g (step x)) (base x))).If

`rel`

has been shown to be well-founded on `mp`

-measures, then `g`

's
termination can be insured by finding a measure, `(m x)`

, with the
property that `m`

produces a measure:
(mp (m x)), ; Defun-goal-1and that the argument to

`g`

gets smaller (when measured by `m`

and
compared by `rel`

) in the recursion,
(implies (test x) (rel (m (step x)) (m x))). ; Defun-goal-2If

`rel`

is selected as the `:well-founded-relation`

to be used in the
definition of `g`

, the definitional principal will generate and
attempt to prove `defun-goal-1`

and `defun-goal-2`

to justify `g`

. We
show later why these two goals are sufficient to establish the
termination of `g`

. Observe that neither the ordinals nor the
embedding, `fn`

, of the `mp`

-measures into the ordinals is involved in
the goals generated by the definitional principal.
Suppose now that a `:well-founded-relation`

theorem has been proved
for `mp`

and `rel`

. How can `rel`

be ``selected as the
`:well-founded-relation`

'' by `defun`

? There are two ways.
First, an `xargs`

keyword to the `defun`

event allows the
specification of a `:well-founded-relation`

. Thus, the definition
of `g`

above might be written

(defun g (x) (declare (xargs :well-founded-relation (mp . rel))) (if (test x) (g (step x)) (base x)))Alternatively,

`rel`

may be specified as the
`:default-well-founded-relation`

in `acl2-defaults-table`

by
executing the event
(set-default-well-founded-relation rel).When a

`defun`

event does not explicitly specify the relation in its
`xargs`

the default relation is used. When ACL2 is initialized, the
default relation is `e0-ord-<`

.
Finally, though it is probably obvious, we now show that
`defun-goal-1`

and `defun-goal-2`

are sufficient to insure the
termination of `g`

provided `property-1`

and `property-2`

of `mp`

and `rel`

have been proved. To this end, assume we have proved `defun-goal-1`

and `defun-goal-2`

as well as `property-1`

and `property-2`

and we show
how to admit `g`

under the primitive ACL2 definitional principal
(i.e., using only the ordinals). In particular, consider the
definition event

(defun g (x) (declare (xargs :well-founded-relation e0-ord-< :measure (fn (m x)))) (if (test x) (g (step x)) (base x)))Proof that

`g`

is admissible: To admit the definition of `g`

above we
must prove
(e0-ordinalp (fn (m x))) ; *1and

(implies (test x) ; *2 (e0-ord-< (fn (m (step x))) (fn (m x)))).But *1 can be proved by instantiating

`property-1`

to get
(implies (mp (m x)) (e0-ordinalp (fn (m x)))),and then relieving the hypothesis with

`defun-goal-1`

, `(mp (m x))`

.
Similarly, *2 can be proved by instantiating `property-2`

to get

(implies (and (mp (m (step x))) (mp (m x)) (rel (m (step x)) (m x))) (e0-ord-< (fn (m (step x))) (fn (m x))))and relieving the first two hypotheses by appealing to two instances of

`defun-goal-1`

, thus obtaining
(implies (rel (m (step x)) (m x)) (e0-ord-< (fn (m (step x))) (fn (m x)))).By chaining this together with

`defun-goal-2`

,
(implies (test x) (rel (m (step x)) (m x)))we obtain *2. Q.E.D.