How to use a previously-proved measure theorem

See lemma-instance for a discussion of

The following very simple example is contrived but should get the main idea
across. Suppose that the following event was previously executed, for example
when including a book, in order to define the log base 10 of

(encapsulate () (local (include-book "arithmetic-5/top" :dir :system)) (defun log10 (x) ; log base 10 of x (if (or (zp x) (< x 10)) 0 (1+ (log10 (floor x 10))))))

Now suppose we want to admit the following definition, whose recursion
pattern is similar to that above. The simplest way might be to include the
same book as above, but perhaps that is impossible because the formula
for some name in that book conflicts with the formula for that name in the
current session. Without that book, it could be challenging to develop lemmas
that allow the termination proof to succeed for this proposed definition. So
we provide a hint, specifying the use of the termination theorem already
proved for

(defun base10-digits (x) (declare (xargs :hints (("Goal" :use ((:termination-theorem log10)))))) (if (or (zp x) (< x 10)) (list x) (append (base10-digits (floor x 10)) (list (mod x 10)))))

With this hint, the termination proof succeeds, printing the following line in the event summary.

Hint-events: ((:USE LOG10))

This line says that the only

:use ((:rewrite car-cons) (:termination-theorem log10))

then the

Hint-events: ((:USE CAR-CONS) (:USE LOG10))

Similarly, proof output for a

We augment the goal with the hypothesis provided by the :USE hint. The hypothesis can be obtained from LOG10. We are left with the following subgoal.

Again, perhaps one would expect to see ``

These hypotheses can be obtained from CAR-CONS and LOG10.

Next, we consider an example where a function symbol being defined occurs in the measure theorem.

(defun left (x) (car x)) (defun right (x) (car x)) (defun first-natp (x) (if (atom x) (if (natp x) x nil) (or (first-natp (left x)) (first-natp (right x)))))

The measure (termination) theorem for

(AND (IMPLIES (NOT (ATOM X)) (O< (ACL2-COUNT (LEFT X)) (ACL2-COUNT X))) (IMPLIES (AND (NOT (ATOM X)) (NOT (FIRST-NATP (LEFT X)))) (O< (ACL2-COUNT (RIGHT X)) (ACL2-COUNT X))))

Now suppose the functions

(in-theory (disable left right)) (defun first-symbolp (x) (if (atom x) (if (symbolp x) x nil) (or (first-symbolp (left x)) (first-symbolp (right x)))))

This time the termination theorem is as follows.

(AND (IMPLIES (NOT (ATOM X)) (O< (ACL2-COUNT (LEFT X)) (ACL2-COUNT X))) (IMPLIES (AND (NOT (ATOM X)) (NOT (FIRST-SYMBOLP (LEFT X)))) (O< (ACL2-COUNT (RIGHT X)) (ACL2-COUNT X))))

Notice that this theorem is not an immediate consequence of the termination
theorem for

(defun first-symbolp (x) (declare (xargs :hints (("Goal" :by (:termination-theorem first-natp))))) (if (atom x) (if (symbolp x) x nil) (or (first-symbolp (left x)) (first-symbolp (right x)))))

Such a substitution is made provided the old and new function symbols each
have the same number of formal parameters. In general a

The functional substitution can be provided explicitly. The following example has identical behavior to that above.

(defun first-symbolp (x) (declare (xargs :hints (("Goal" :by (:termination-theorem first-natp ((first-natp first-symbolp))))))) (if (atom x) (if (symbolp x) x nil) (or (first-symbolp (left x)) (first-symbolp (right x)))))

Finally, note that a

We conclude with a remark about what happens when the termination theorem
does not exist, even though (as required) the indicated function symbol is in
logic mode. (For example, imagine that you are generating such hints
programmatically, without analyzing whether the indicated function symbol was
defined using recursion.) In that case, using

ACL2 !>(defun g (x) (declare (xargs :hints (("Goal" :use ((:termination-theorem f)))))) (if (consp x) (g (cddr x)) x)) ACL2 Error in ( DEFUN G ...): The object (:TERMINATION-THEOREM F) is an ill-formed lemma instance because there is no termination theorem for F. The function F is not recursive. See :DOC lemma-instance. Summary Form: ( DEFUN G ...) Rules: NIL Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) ACL2 Error in ( DEFUN G ...): See :DOC failure. ******** FAILED ******** ACL2 !>

The alternative,

ACL2 !>(defun g (x) (declare (xargs :hints (("Goal" :use ((:termination-theorem! f)))))) (if (consp x) (g (cddr x)) x)) For the admission of G we will use the relation O< (which is known to be well-founded on the domain recognized by O-P) and the measure (ACL2-COUNT X). The non-trivial part of the measure conjecture is Goal (IMPLIES (CONSP X) (O< (ACL2-COUNT (CDDR X)) (ACL2-COUNT X))). [Note: A hint was supplied for our processing of the goal above. Thanks!] We augment the goal with the hypothesis provided by the :USE hint. The hypothesis can be obtained from F. We are left with the following subgoal. Goal' (IMPLIES T (OR (NOT (CONSP X)) (O< (ACL2-COUNT (CDDR X)) (ACL2-COUNT X)))). By case analysis we reduce the conjecture to [[.. output elided ..]] Hint-events: ((:USE F)) Time: 0.02 seconds (prove: 0.01, print: 0.01, other: 0.00) Prover steps counted: 1121 G ACL2 !>