1\DOC CHOOSE_TAC
2
3\TYPE {CHOOSE_TAC : thm_tactic}
4
5\SYNOPSIS
6Adds the body of an existentially quantified theorem to the assumptions of
7a goal.
8
9\KEYWORDS
10tactic, existential.
11
12\DESCRIBE
13When applied to a theorem {A' |- ?x. t} and a goal, {CHOOSE_TAC} adds
14{t[x'/x]} to the assumptions of the goal, where {x'} is a variant of
15{x} which is not free in the goal or assumption list; normally {x'} is
16just {x}.
17{
18         A ?- u
19   ====================  CHOOSE_TAC (A' |- ?x. t)
20    A u {t[x'/x]} ?- u
21}
22Unless {A'} is a subset of {A}, this is not a valid tactic.
23
24\FAILURE
25Fails unless the given theorem is existentially quantified.
26
27\EXAMPLE
28Suppose we have a goal asserting that the output of an electrical circuit
29(represented as a boolean-valued function) will become high at some time:
30{
31   ?- ?t. output(t)
32}
33and we have the following theorems available:
34{
35   t1 = |- ?t. input(t)
36   t2 = !t. input(t) ==> output(t+1)
37}
38Then the goal can be solved by the application of:
39{
40   CHOOSE_TAC th1
41     THEN EXISTS_TAC (Term `t+1`)
42     THEN UNDISCH_TAC (Term `input (t:num) :bool`)
43     THEN MATCH_ACCEPT_TAC th2
44}
45
46\COMMENTS
47To do similarly with several existentially quantified variables, use
48{REPEAT_TCL CHOOSE_THEN ASSUME_TAC} in place of {CHOOSE_TAC}
49
50\SEEALSO
51Thm_cont.CHOOSE_THEN, Tactic.X_CHOOSE_TAC, Thm_cont.REPEAT_TCL.
52\ENDDOC
53