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
|
\DOC SELECT_CONV
\TYPE {SELECT_CONV : term -> thm}
\SYNOPSIS
Eliminates an epsilon term by introducing an existential quantifier.
\KEYWORDS
conversion, epsilon.
\DESCRIBE
The conversion {SELECT_CONV} expects a boolean term of the form
{`P[@x.P[x]/x]`}, which asserts that the epsilon term {@x.P[x]} denotes
a value, {x} say, for which {P[x]} holds. This assertion is equivalent
to saying that there exists such a value, and {SELECT_CONV} applied to a
term of this form returns the theorem {|- P[@x.P[x]/x] = ?x. P[x]}.
\FAILURE
Fails if applied to a term that is not of the form {`P[@x.P[x]/x]`}.
\EXAMPLE
{
# SELECT_CONV `(@n. n < m) < m`;;
val it : thm = |- (@n. n < m) < m <=> (?n. n < m)
}
\USES
Particularly useful in conjunction with {CONV_TAC} for proving properties
of values denoted by epsilon terms. For example, suppose that one wishes
to prove the goal
{
# g `!m. 0 < m ==> (@n. n < m) < SUC m`;;
}
\noindent We start off:
{
# e(REPEAT STRIP_TAC THEN
MATCH_MP_TAC(ARITH_RULE `!m n. m < n ==> m < SUC n`));;
val it : goalstack = 1 subgoal (1 total)
0 [`0 < m`]
`(@n. n < m) < m`
}
\noindent This is now in the correct form for using {SELECT_CONV}:
{
# e(CONV_TAC SELECT_CONV);;
val it : goalstack = 1 subgoal (1 total)
0 [`0 < m`]
`?n. n < m`
}
\noindent and the resulting subgoal is straightforward to prove, e.g.
by {ASM_MESON_TAC[]} or {EXISTS_TAC `0` THEN ASM_REWRITE_TAC[]}.
\SEEALSO
SELECT_ELIM, SELECT_RULE.
\ENDDOC
|
