Gthm
The guard theorem for a given function symbol
This utility (pronounced ``gee-thumb'') generates the guard
theorem (i.e., guard proof obligation) for a given function symbol, as would
be generated by a :guard-theorem lemma-instance in a
:use hint.
Example Forms:
:gthm FN
(gthm 'FN) ; equivalent to the above
(gthm 'FN :limited nil) ; equivalent to the above
(gthm 'FN :limited t) ; include guard-debug info
(gthm 'FN nil) ; avoid any simplification
General Forms:
:gthm FN ; equivalent to (gthm 'FN)
(gthm x &optional simplify guard-debug)
where FN is a function symbol and x evaluates to a function
symbol. Evaluation returns the guard theorem as a user-level (untranslated)
term. The optional argument simplify, described below, is
:limited 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
related utilities.
Normally one will evaluate :gthm FN or equivalently (see keyword-commands), the form (gthm 'FN). In this case the guard theorem
may be partially 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
simplify argument should be nil to avoid such simplification; that
is, use (gthm 'FN nil). See also guard-simplification for
discussion of simplification done for various guard formula utilities.
Note that the result from evaluating (gthm x simplify guard-debug) is
an untranslated term, that is, a user-level term; see term.
The corresponding call (guard-theorem x simplify guard-debug (w state)
state) returns a translated term.
