The guard theorem for a given function symbol
This utility (pronounced ``gee-thumb'') generates the guard proof
obligation for a given function symbol.
(gthm 'FN) ; equivalent to the above
(gthm 'FN t nil) ; equivalent to the above
(gthm 'FN nil t) ; avoid any simplification and include guard-debug info
:gthm FN ; equivalent to (gthm 'FN)
(gthm x &optional simp-p guard-debug)
where FN is a function symbol and x evaluates to a function
symbol. Evaluation returns the user-level (untranslated) version of that
guard theorem. The optional argument simp-p, described below, is t
by default. The optional argument guard-debug is nil by default;
when non-nil, the guard theorem is modified as with the option
:guard-debug for verify-guards; see guard-debug.
See lemma-instance for how to provide the result of :gthm as a
:guard-theorem prover hint. Also see guard-formula-utilities for
Normally one will evaluate :gthm FN or equivalently (see keyword-commands), the form (gthm 'FN). In this case the guard theorem
may be simplified before it is returned, by using a form of ``subsumption'' to
eliminate redundancy and by deleting tautologies as well as instances of built-in-clause rules that come with ACL2. The simp-p argument should
be nil to avoid such simplification; that is, use (gthm 'FN nil).
The simp-p argument bears some resemblance to the :guard-simplify
option to verify-guards; but somewhat less simplification is done by
gthm with simp-p = T than is done when generating guard
obligations (by defun or verify-guards) with
:guard-simplify = T.
Note that the result from evaluating (gthm x simp-p guard-debug) is an
untranslated term, that is, a user-level term; see termp. The
corresponding call (guard-theorem x simp-p guard-debug (w state) state)
returns a translated term.