Guard-formula-utilities
Utilities that show guard proof obligations
See verify-guards and see guard for discussions of
guards. Here we discuss several utilities that provide the proof obligations
for guards, and briefly compare what is offered by each. Of course, see the
documentation of each utility for details.
The first pair of utilities captures formulas produced during guard
verification.
Verify-guards-formula: Use this to see what the corresponding
verify-guards event prints, but without following through with a proof
attempt. This utility is only for output, without returning an interesting
value.
Guard-obligation: This function is a programmatic version of the
macro, verify-guards-formula. It provides the guard obligation as a
set of clauses, along with other information.
The second pair of utilities captures the formula provided when a
:guard-theorem is supplied for a :use hint.
Gthm: This macro returns a user-level (``untranslated'')
representation of the term that is generated for a :guard-theorem
lemma-instance. Options control whether or not simplification and
guard-debug are used.
Guard-theorem: This utility is like gthm, except that it is
a function rather than a macro and it returns a translated term (a termp).
We conclude by contrasting these two pairs of utilities.
- The first pair can take as input as either a function symbol or a term;
for the second pair a function symbol (not a term) is required.
- The level of simplification differs between the two pairs. See guard-simplification for a detailed explanation; here are highlights. The
first pair simplifies (by default) with respect to the current-theory
before producing the guard proof obligation formula, as is typically done when
verifying guards; but the second pair only performs the theory-independent
simplification done for a :guard-theorem specified in a :use hint,
or if a suitable option is supplied, no simplification at all.
- The two pairs differ in their output signatures: in particular, the
utilities in the first pair return multiple values while those in the second
pair return a single value.
Subtopics
- Guard-simplification
- Levels of simplification for guard proof obligations
- Guard-obligation
- The guard proof obligation
- Gthm
- The guard theorem for a given function symbol
- Verify-guards-formula
- View the guard proof obligation, without proving it
- Guard-theorem-example
- How to use a previously-proved guard theorem
- Guard-theorem
- Use a previously-proved guard theorem
- Verify-guard-implication
- Guard implication for memoize keyword :invoke
