1\DOC MESON_TAC 2 3\TYPE {MESON_TAC : thm list -> tactic} 4 5\SYNOPSIS 6Performs first order proof search to prove the goal, using the given 7theorems as additional assumptions in the search. 8 9\KEYWORDS 10decision procedure, tactic. 11 12\LIBRARY 13mesonLib 14 15\DESCRIBE 16{MESON_TAC} performs first order proof using the model elimination 17algorithm. This algorithm is semi-complete for pure first order 18logic. It makes special provision for handling polymorphic and 19higher-order values, and often this is sufficient. It does not handle 20conditional expressions at all, and these should be eliminated before 21{MESON_TAC} is applied. 22 23{MESON_TAC} works by first converting the problem instance it is given 24into an internal format where it can do proof search efficiently, 25without having to do proof search at the level of HOL inference. If a 26proof is found, this is translated back into applications of HOL 27inference rules, proving the goal. 28 29The feedback given by {MESON_TAC} is controlled by the level of the 30integer reference variable {mesonLib.chatting}. At level zero, 31nothing is printed. At the default level of one, a line of dots is 32printed out as the proof progresses. At all other values for this 33variable, {MESON_TAC} is most verbose. If the proof is progressing 34quickly then it is often worth waiting for it to go quite deep into 35its search. Once a proof slows down, it is not usually worth waiting 36for it after it has gone through a few (no more than five or six) 37levels. (At level one, a ``level'' is represented by the printing of 38a single dot.) 39 40\FAILURE 41{MESON_TAC} fails if it searches to a depth equal to the contents of 42the reference variable {mesonLib.max_depth} (set to 30 by default, but 43changeable by the user) without finding a proof. Shouldn't fail 44otherwise. 45 46 47 48\USES 49{MESON_TAC} can only progress the goal to a successful proof of the 50(whole) goal or not at all. In this respect it differs from tactics 51such as simplification and rewriting. Its ability to solve 52existential goals and to make effective use of transitivity theorems 53make it a particularly powerful tactic. 54 55 56 57\COMMENTS 58The assumptions of a goal are ignored when {MESON_TAC} is applied. To 59include assumptions use {ASM_MESON_TAC}. 60 61 62 63\SEEALSO 64mesonLib.ASM_MESON_TAC, mesonLib.GEN_MESON_TAC. 65\ENDDOC 66