1\DOC EXISTS_TAC
2
3\TYPE {EXISTS_TAC : (term -> tactic)}
4
5\SYNOPSIS
6Reduces existentially quantified goal to one involving a specific witness.
7
8\KEYWORDS
9tactic, quantifier, existential, choose, witness.
10
11\DESCRIBE
12When applied to a term {u} and a goal {?x. t}, the tactic
13{EXISTS_TAC} reduces the goal to {t[u/x]} (substituting {u}
14for all free instances of {x} in {t}, with variable renaming if
15necessary to avoid free variable capture).
16{
17    A ?- ?x. t
18   =============  EXISTS_TAC "u"
19    A ?- t[u/x]
20}
21
22
23\FAILURE
24Fails unless the goal's conclusion is existentially quantified and the
25term supplied has the same type as the quantified variable in the goal.
26
27\EXAMPLE
28The goal:
29{
30   ?- ?x. x=T
31}
32can be solved by:
33{
34   EXISTS_TAC ``T`` THEN REFL_TAC
35}
36
37\SEEALSO
38Thm.EXISTS.
39\ENDDOC
40