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