PROVE : thm list -> term -> thm
STRUCTURE
bossLib
SYNOPSIS
Prove a theorem with use of supplied lemmas.
DESCRIPTION
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.

SEEALSO
PROVE_TAC, MESON_TAC, ASM_MESON_TAC
HOL  Trindemossen-1