EXISTS_TAC : (term -> tactic)

- STRUCTURE
- SYNOPSIS
- Reduces existentially quantified goal to one involving a specific witness.
- DESCRIPTION
- When applied to a term u and a goal ?x. t, the tactic EXISTS_TAC reduces the goal to t[u/x] (substituting u for all free instances of x in t, with variable renaming if necessary to avoid free variable capture).
A ?- ?x. t ============= EXISTS_TAC "u" A ?- t[u/x]

- FAILURE
- Fails unless the goal’s conclusion is existentially quantified and the term supplied has the same type as the quantified variable in the goal.
- EXAMPLE
- The goal:can be solved by:
?- ?x. x=T

EXISTS_TAC ``T`` THEN REFL_TAC

- SEEALSO

HOL Kananaskis-14