ACL2-pc::prove-termination
(macro)
Prove termination efficiently by using a previous termination theorem.
Example:
(prove-termination f1 (disable h))
Example of typical usage:
(defun f2 (x)
(declare
(xargs :hints
(("Goal"
:instructions
((prove-termination
f1
(disable h)))))))
(f2-body x))
General Forms:
(prove-termination fn)
(prove-termination fn thy)
(prove-termination fn thy alt-thy)
(prove-termination fn thy alt-thy verbose)
where fn is a known function symbol and thy and alt-thy,
when supplied and non-nil, are theory expressions.
This proof-builder macro attempts to prove a theorem, typically a
termination proof obligation, by applying the hint :termination-theorem
fn in a carefully controlled, efficient manner (using the :fancy-use
proof-builder macro). This proof is attempted in the theory, thy,
if supplied and non-nil, else in the current-theory. If that
proof fails, then a single, ordinary prover call is made with that :use
hint and in the following theory: alt-thy if supplied and non-nil,
else thy if supplied and non-nil, else the current-theory.
If the proof has not yet succeeded and the original theory is not nil or
(current-theory :here), then a final proof is attempted in the same
careful manner as the first proof attempt.
Output is inhibited by default. However, if verbose is t then
output is as specified by the enclosing environment; and if verbose is
any other non-nil value, then output is mostly inhibited for that attempt
by use of the proof-builder command, :quiet. In all of those
non-nil cases for the verbose input, a little message will be
started at the beginning of the second and third proof attempts, if any.
For a few small examples, see community book
kestrel/utilities/proof-builder-macros-tests.lisp.
For a way to use lemma instances other than termination theorems, see ACL2-pc::fancy-use.
Hacker tip: Invoke (trace$ acl2::pc-fancy-use-fn) to see the
proof-builder instruction created when invoking prove-termination.
