1\DOC X_CHOOSE_TAC 2 3\TYPE {X_CHOOSE_TAC : term -> thm_tactic} 4 5\SYNOPSIS 6Assumes a theorem, with existentially quantified variable replaced by a given 7witness. 8 9\KEYWORDS 10tactic, witness, quantifier, existential. 11 12\DESCRIBE 13{X_CHOOSE_TAC} expects a variable {y} and theorem with an existentially 14quantified conclusion. When applied to a goal, it adds a new 15assumption obtained by introducing the variable {y} as a witness for 16the object {x} whose existence is asserted in the theorem. 17{ 18 A ?- t 19 =================== X_CHOOSE_TAC y (A1 |- ?x. w) 20 A u {w[y/x]} ?- t (y not free anywhere) 21} 22 23 24\FAILURE 25Fails if the theorem's conclusion is not existentially quantified, or 26if the first argument is not a variable. Failures may arise in the 27tactic-generating function. An invalid tactic is produced if the 28introduced variable is free in {w}, {t} or {A}, or if the theorem has 29any hypothesis which is not alpha-convertible to an assumption of the 30goal. 31 32\EXAMPLE 33Given a goal of the form 34{ 35 {n < m} ?- ?x. m = n + (x + 1) 36} 37the following theorem may be applied: 38{ 39 th = [n < m] |- ?p. m = n + p 40} 41by the tactic {(X_CHOOSE_TAC (Term`q:num`) th)} giving 42the subgoal: 43{ 44 {n < m, m = n + q} ?- ?x. m = n + (x + 1) 45} 46 47 48\SEEALSO 49Thm.CHOOSE, Thm_cont.CHOOSE_THEN, Thm_cont.X_CHOOSE_THEN. 50\ENDDOC 51