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