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
|
\DOC X_CHOOSE_TAC
\TYPE {X_CHOOSE_TAC : term -> thm_tactic}
\SYNOPSIS
Assumes a theorem, with existentially quantified variable replaced by a given
witness.
\KEYWORDS
tactic, witness, quantifier, existential.
\DESCRIBE
{X_CHOOSE_TAC} expects a variable {y} and theorem with an existentially
quantified conclusion. When applied to a goal, it adds a new
assumption obtained by introducing the variable {y} as a witness for
the object {x} whose existence is asserted in the theorem.
{
A ?- t
=================== X_CHOOSE_TAC `y` (A1 |- ?x. w)
A u {{w[y/x]}} ?- t (`y` not free anywhere)
}
\FAILURE
Fails if the theorem's conclusion is not existentially quantified, or if
the first argument is not a variable. Failures may arise in the
tactic-generating function. An invalid tactic is produced if the
introduced variable is free in {w} or {t}, or if the theorem has any
hypothesis which is not alpha-convertible to an assumption of the
goal.
\EXAMPLE
Given a goal:
{
# g `(?y. x = y + 2) ==> x < x * x`;;
}
\noindent the following may be applied:
{
# e(DISCH_THEN(X_CHOOSE_TAC `d:num`));;
val it : goalstack = 1 subgoal (1 total)
0 [`x = d + 2`]
`x < x * x`
}
\noindent after which the following will finish things:
{
# e(ASM_REWRITE_TAC[] THEN ARITH_TAC);;
val it : goalstack = No subgoals
}
\SEEALSO
CHOOSE, CHOOSE_THEN, X_CHOOSE_THEN.
\ENDDOC
|
