PROVE
bossLib.PROVE : thm list -> term -> thm
Also exported as BasicProvers.PROVE.
Prove a theorem with use of supplied lemmas.
An invocation PROVE thl M attempts to prove M using an automated
reasoner supplied with the lemmas in thl. The automated reasoner
performs a first order proof search. It currently provides some support
for polymorphism and higher-order values (lambda terms).
Failure
If the proof search fails, or if M does not have type bool.
Example
> PROVE [] (concl SKOLEM_THM);
Meson search level: ........
val it = ⊢ ∀P. (∀x. ∃y. P x y) ⇔ ∃f. ∀x. P x (f x): thm
> let open arithmeticTheory
in
PROVE [ADD_ASSOC, ADD_SYM, ADD_CLAUSES]
(Term `x + 0 + y + z = y + (z + x)`)
end;
Meson search level: ............
val it = ⊢ x + 0 + y + z = y + (z + x): thm
Comments
Some output (a row of dots) is currently generated as PROVE works. If
the frequency of dot emission becomes slow, that is a sign that the term
is not likely to be proved with the current lemmas.
Unlike MESON_TAC, PROVE can handle terms with conditionals.
See also
bossLib.PROVE_TAC,
mesonLib.MESON_TAC,
mesonLib.ASM_MESON_TAC