1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
|
\DOC prove_thm
\TYPE {prove_thm : ((string # term # tactic) -> thm)}
\SYNOPSIS
Attempts to prove a boolean term using the supplied tactic, then save the
theorem.
\DESCRIBE
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 the latter case {prove_thm} will list the unsolved goals to help the user.
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.
\SEEALSO
prove, PROVE, TAC_PROOF, VALID.
\ENDDOC
|
