1\DOC CHOOSE_THEN
2
3\TYPE {CHOOSE_THEN : thm_tactical}
4
5\SYNOPSIS
6Applies a tactic generated from the body of existentially quantified theorem.
7
8\KEYWORDS
9theorem-tactic, existential.
10
11\DESCRIBE
12When applied to a theorem-tactic {ttac}, an existentially quantified
13theorem {A' |- ?x. t}, and a goal, {CHOOSE_THEN} applies the tactic
14{ttac (t[x'/x] |- t[x'/x])} to the goal, where {x'} is a variant of
15{x} chosen not to be free in the assumption list of the goal. Thus if:
16{
17    A ?- s1
18   =========  ttac (t[x'/x] |- t[x'/x])
19    B ?- s2
20}
21then
22{
23    A ?- s1
24   ==========  CHOOSE_THEN ttac (A' |- ?x. t)
25    B ?- s2
26}
27This is invalid unless {A'} is a subset of {A}.
28
29\FAILURE
30Fails unless the given theorem is existentially quantified, or if the
31resulting tactic fails when applied to the goal.
32
33\EXAMPLE
34This theorem-tactical and its relatives are very useful for using existentially
35quantified theorems. For example one might use the inbuilt theorem
36{
37   LESS_ADD_1 = |- !m n. n < m ==> (?p. m = n + (p + 1))
38}
39to help solve the goal
40{
41   ?- x < y ==> 0 < y * y
42}
43by starting with the following tactic
44{
45   DISCH_THEN (CHOOSE_THEN SUBST1_TAC o MATCH_MP LESS_ADD_1)
46}
47which reduces the goal to
48{
49   ?- 0 < ((x + (p + 1)) * (x + (p + 1)))
50}
51which can then be finished off quite easily, by, for example:
52{
53   REWRITE_TAC[ADD_ASSOC, SYM (SPEC_ALL ADD1),
54               MULT_CLAUSES, ADD_CLAUSES, LESS_0]
55}
56
57
58\SEEALSO
59Tactic.CHOOSE_TAC, Thm_cont.X_CHOOSE_THEN.
60\ENDDOC
61