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