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