WELL-FOUNDED-RELATION

show that a relation is well-founded on a set
```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) (o-p (ordinate x)))
(implies (and (pairp x)
(pairp y)
(lex2p x y))
(o< (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) (O-P (fn x)))              ; Property 1
(IMPLIES (AND (mp x)                       ; Property 2
(mp y)
(rel x y))
(O< (fn x) (fn y)))),
```
or
```(AND (O-P (fn x))                               ; Property 1
(IMPLIES (rel x y)                         ; Property 2
(O< (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 o-p.) 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 `o<`. (See o<.) 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-1
```
and 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-2
```
If `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 `o<`.

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 o<
: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
```(o-p (fn (m x)))                        ; *1
```
and
```(implies (test x)                               ; *2
(o< (fn (m (step x))) (fn (m x)))).
```
But *1 can be proved by instantiating `property-1` to get
```(implies (mp (m x)) (o-p (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)))
(o< (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))
(o< (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.  