1\DOC REFINE_EXISTS_TAC
2
3\TYPE {Q.REFINE_EXISTS_TAC : term quotation -> tactic}
4
5\SYNOPSIS
6Attacks existential goals, making the existential variable more concrete.
7
8\KEYWORDS
9
10
11\LIBRARY
12Q
13
14\DESCRIBE
15The tactic {Q.REFINE_EXISTS_TAC q} parses the quotation {q} in the
16context of the (necessarily existential) goal to which it is applied,
17and uses the resulting term as the witness for the goal.  However, if
18the witness has any variables not already present in the goal, then
19these are treated as new existentially quantified variables.  If there
20are no such ``free'' variables, then the behaviour is the same as
21{EXISTS_TAC}.
22
23\FAILURE
24Fails if the goal is not existential, or if the quotation can not
25parse to a term of the same type as the existentially quantified
26variable.
27
28\EXAMPLE
29If the quotation doesn't mention any new variables:
30{
31   - Q.REFINE_EXISTS_TAC `n` ([``n > x``], ``?m. m > x``);
32   > val it =
33       ([([``n > x``], ``n > x``)], fn)
34       : (term list * term) list * (thm list -> thm)
35}
36If the quotation does mention any new variables, they are
37existentially quantified in the new goal:
38{
39   - Q.REFINE_EXISTS_TAC `n + 2` ([``~P 0``], ``?p. P (p - 1)``);
40   > val it =
41       ([([``~P 0``], ``?n. P (n + 2 - 1)``)], fn)
42       : (term list * term) list * (thm list -> thm)
43}
44
45
46\USES
47{Q.REFINE_EXISTS_TAC} is useful if it is clear that an existential goal
48will be solved by a term of particular form, while it is not yet clear
49precisely what term this will be.  Further proof activity should be
50able to exploit the additional structure that has appeared in the
51place of the existential variable.
52
53\SEEALSO
54Tactic.EXISTS_TAC.
55\ENDDOC
56