1\DOC X_CHOOSE_THEN
2
3\TYPE {X_CHOOSE_THEN : (term -> thm_tactical)}
4
5\SYNOPSIS
6Replaces existentially quantified variable with given witness, and passes it to
7a theorem-tactic.
8
9\KEYWORDS
10theorem-tactic, quantifier, existential.
11
12\DESCRIBE
13{X_CHOOSE_THEN} expects a variable {y}, a tactic-generating function
14{f:thm->tactic}, and a theorem of the form {(A1 |- ?x. w)} as
15arguments.  A new theorem is created by introducing the given variable
16{y} as a witness for the object {x} whose existence is asserted in the original
17theorem, {(w[y/x] |- w[y/x])}.  If the tactic-generating function {f}
18applied to this theorem produces results as follows when applied to a
19goal {(A ?- t)}:
20{
21    A ?- t
22   =========  f ({w[y/x]} |- w[y/x])
23    A ?- t1
24}
25then applying {(X_CHOOSE_THEN "y" f (A1 |- ?x. w))} to the
26goal {(A ?- t)} produces the subgoal:
27{
28    A ?- t
29   =========  X_CHOOSE_THEN y f (A1 |- ?x. w)
30    A ?- t1         (y not free anywhere)
31}
32
33
34\FAILURE
35Fails if the theorem's conclusion is not existentially quantified, or
36if the first argument is not a variable. Failures may arise in the
37tactic-generating function. An invalid tactic is produced if the
38introduced variable is free in {w}, {t} or {A}, or if the theorem has
39any hypothesis which is not alpha-convertible to an assumption of the
40goal.
41
42\EXAMPLE
43Given a goal of the form
44{
45   {n < m} ?- ?x. m = n + (x + 1)
46}
47the following theorem may be applied:
48{
49   th = [n < m] |- ?p. m = n + p
50}
51by the tactic {(X_CHOOSE_THEN (Term`q:num`) SUBST1_TAC th)} giving
52the subgoal:
53{
54   {n < m} ?- ?x. n + q = n + (x + 1)
55}
56
57
58\SEEALSO
59Thm.CHOOSE, Thm_cont.CHOOSE_THEN, Thm_cont.CONJUNCTS_THEN, Thm_cont.CONJUNCTS_THEN2, Thm_cont.DISJ_CASES_THEN, Thm_cont.DISJ_CASES_THEN2, Thm_cont.DISJ_CASES_THENL, Thm_cont.STRIP_THM_THEN, Tactic.X_CHOOSE_TAC.
60\ENDDOC
61