- STRUCTURE
hol88Lib
- SYNOPSIS
Attempts to prove a boolean term using the supplied tactic, then save the
theorem.
- DESCRIBE
Found in the hol88 library. When applied to a triple (s,tm,tac),
giving the name to save the theorem under, the term to prove (with no
assumptions) and the tactic to perform the proof, the function
prove_thm attempts to prove the goal ?- tm, that is, the term tm
with no assumptions, using the tactic tac. If prove_thm succeeds, it
attempts to save the resulting theorem in the current theory segment,
and if this succeeds, the saved theorem is returned.
- FAILURE
Fails if the term is not of type bool (and so cannot possibly be
the conclusion of a theorem), or if the tactic cannot solve the goal.
In addition, prove_thm will fail if the theorem cannot be saved, e.g. because
there is already a theorem of that name in the current theory segment, or if
the resulting theorem has assumptions; clearly this can only happen if the
tactic was invalid, so this gives some measure of validity checking. The
function is not available unless the hol88 library has been loaded.
- COMMENTS
In hol90, use store_thm instead; the cognitive dissonance between prove,
PROVE, and prove_thm proved to be too much for the author, so in hol90
PROVE doesn’t exist: there is only prove; and prove_thm doesn’t exist:
it has been replaced by store_thm.
- SEEALSO