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 ensures 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 ensured 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 ensure 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.