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