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