1\DOC PROVE
2
3\TYPE {PROVE : thm list -> term -> thm}
4
5\SYNOPSIS
6Prove a theorem with use of supplied lemmas.
7
8\KEYWORDS
9proof, first order.
10
11\DESCRIBE
12An invocation {PROVE thl M} attempts to prove {M} using an automated
13reasoner supplied with the lemmas in {thl}. The automated reasoner
14performs a first order proof search. It currently provides some support
15for polymorphism and higher-order values (lambda terms).
16
17\FAILURE
18If the proof search fails, or if {M} does not have type {bool}.
19
20\EXAMPLE
21{
22- PROVE []  (concl SKOLEM_THM);
23Meson search level: ........
24> val it = |- !P. (!x. ?y. P x y) = ?f. !x. P x (f x) : thm
25
26- let open arithmeticTheory
27  in
28    PROVE [ADD_ASSOC, ADD_SYM, ADD_CLAUSES]
29      (Term `x + 0 + y + z = y + (z + x)`)
30  end;
31Meson search level: ............
32> val it = |- x + 0 + y + z = y + (z + x) : thm
33}
34
35\COMMENTS
36Some output (a row of dots) is currently generated as {PROVE} works. If
37the frequency of dot emission becomes slow, that is a sign that the
38term is not likely to be proved with the current lemmas.
39
40Unlike {MESON_TAC}, {PROVE} can handle terms with conditionals.
41
42\SEEALSO
43bossLib.PROVE_TAC, mesonLib.MESON_TAC, mesonLib.ASM_MESON_TAC.
44
45\ENDDOC
46