Make-termination-theorem
Create a copy of a function's termination theorem that calls stubs.
The :termination-theorem lemma-instance
provides a way to re-use a recursive definition's termination (measure)
theorem. You might find it convenient, however, to create a defthm event
for that theorem. Moreover, a termination theorem can mention the function
symbol that is being defined, but it may be convenient to have a version of
that theorem that instead mentions an unconstrained function symbol, which can
support the use of functional-instantiation.
The form (make-termination-theorem f) will create such a defthm
event, named F$TTHM, with :rule-classes nil, whose body
is the termination-theorem for f, but modified to replace calls of
f. Here is a small example; for more extensive examples see community-book
kestrel/utilities/make-termination-theorem-tests.lisp. Suppose we submit
the following definition.
(defun f (x)
(if (consp x)
(and (f (caar x))
(f (cddr x)))
x))
Here is the termination-theorem for f.
ACL2 !>:tthm f
(AND (O-P (ACL2-COUNT X))
(OR (NOT (CONSP X))
(O< (ACL2-COUNT (CAR (CAR X)))
(ACL2-COUNT X)))
(OR (NOT (CONSP X))
(NOT (F (CAR (CAR X))))
(O< (ACL2-COUNT (CDDR X))
(ACL2-COUNT X))))
ACL2 !>
We now create the corresponding defthm event shown below.
ACL2 !>(make-termination-theorem f)
Summary
Form: ( MAKE-EVENT (ER-LET* ...))
Rules: NIL
Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
(DEFTHM F$TTHM
(AND (O-P (ACL2-COUNT X))
(OR (NOT (CONSP X))
(O< (ACL2-COUNT (CAR (CAR X)))
(ACL2-COUNT X)))
(OR (NOT (CONSP X))
(NOT (F$STUB (CAR (CAR X))))
(O< (ACL2-COUNT (CDDR X))
(ACL2-COUNT X))))
:HINTS (("Goal" :USE (:TERMINATION-THEOREM F ((F F$STUB)))
:IN-THEORY (THEORY 'MINIMAL-THEORY)))
:RULE-CLASSES NIL)
ACL2 !>
Notice that the call of f in the termination-theorem has been
replaced, in the defthm form above, by a new function symbol,
f$stub. That new symbol was introduced using defstub, which has
no constraints, thus easing the application of functional-instantiation
to this theorem.
General Form:
(make-termination-theorem Fun
:subst S ; default described below
:thm-name N ; default Fun$TTHM
:rule-classes R ; default nil
:verbose Vflg ; default nil
:show-only Sflg ; default nil
)
where no keyword argument is evaluated unless wrapped in :eval, as
make-termination-theorem is defined with defmacroq; see defmacroq. Evaluation of this form produces a defthm event based
on the termination-theorem of Fun, taking into account the
arguments as follows.
- Fun is a function symbol defined by recursion (possibly mutual-recursion).
- S is a functional substitution, that is, a list of 2-element lists of
symbols (fi gi). For each symbol gi that is not a function symbol
in the current world, a suitable defstub event will be
introduced for gi. If Fun is singly recursive then there will be a
single such pair (Fun g); otherwise Fun is defined by mutual-recursion and each fi must have been defined together with
Fun, in the same mutual-recursion form. If :subst is omitted
then each suitable function symbol f — that is, Fun as well
as, in the case of mutual recursion, the others defined with Fun —
is paired with the result of adding the suffix "$STUB" to the symbol-name of f.
- R is the :rule-classes argument of the generated
defthm event.
- Output is mostly suppressed by default, but is enabled when Vflg is
not nil.
- If Sflg is not nil, then the generated defthm event EV
will not be submitted; instead, it will be returned in an error-triple (mv
nil EV state).
