Defthm-domain
Prove termination on a given domain
This utility can be useful after executing a call of defpm;
see def-partial-measure. Indeed, we assume that you have read the
example in that documentation topic describing this call:
(defpm fact-test fact-step
fact-measure fact-terminates fact-theory)
Introduction By Way of an Example
Consider the following form.
(defthm-domain trfact-terminates-holds-on-natp
(implies (natp x)
(trfact-terminates x acc))
:test trfact-test ; optional test name: can be deduced by the tool ;
:step trfact-step ; optional step name: can be deduced by the tool ;
:measure (nfix x) ; required argument ;
)
This call produces a proof of the indicated formula, where the first
argument of implies, (natp x), provides a ``domain hypothesis.''
You can use :trans1 to see the macroexpansion of this
defthm-domain call. In short, hints are supplied to automate all
``boilerplate'' reasoning. The :measure is used to guide a proof by
induction. At this stage of development, the best way to use this macro is
probably to submit the form in the hope that the proof will complete
automatically; but if it doesn't, then use :trans1 to see what
the form generates, and modify that event manually in order to fix the failed
proofs.
Detailed Documentation
General form:
(defthm-domain NAME
(implies DOMAIN-TERM
(TERMINATES FORMAL-1 ... FORMAL-K))
:test TEST
:step STEP
:measure MEASURE
:verbose VERBOSE
:root ROOT
)
where there is no output unless VERBOSE is non-nil. It is
allowed to replace the implies call above by its second argument (the
TERMINATES call) if DOMAIN-TERM is t. The remaining arguments
are as follows.
The keywords :test and :step both have value nil by default.
So does :root, unless TERMINATES has a symbol-name of the
form "root-TERMINATES", in which case :root is the symbol in the
package of TERMINATES whose name is that string, root. If
:root has a value of nil, even after taking this default into
account, then both :test and :step must have a non-nil value.
The reason for this requirement is that when :test and/or :step is
omitted, the value is computed from the root by adding the suffix
"-TEST" or "-STEP" to the root (respectively). The functions
introduced for :test and :step are exactly as for defpm; see
def-partial-measure. Note however that the formals are those from the
call of TERMINATES.
See the discussion above about ``boilerplate'' reasoning for hints on how
to deal with failures of defthm-domain calls.
More Information
The community book misc/defpm.lisp illustrates how to use defpm
and defthm-domain to define ``partial'' functions. Search for calls of
my-test in that book to see examples.
