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
|
\DOC SELECT_INTRO
\TYPE {SELECT_INTRO : (thm -> thm)}
\SYNOPSIS
Introduces an epsilon term.
\KEYWORDS
rule, epsilon.
\DESCRIBE
{SELECT_INTRO} takes a theorem with an applicative conclusion, say
{P x}, and returns a theorem with the epsilon term {$@ P} in place
of the original operand {x}.
{
A |- P x
-------------- SELECT_INTRO
A |- P($@ P)
}
\noindent The returned theorem asserts that {$@ P} denotes some value
at which {P} holds.
\FAILURE
Fails if the conclusion of the theorem is not an application.
\EXAMPLE
Given the theorem
{
th1 = |- (\n. m = n)m
}
\noindent applying {SELECT_INTRO} replaces the second occurrence of {m} with the
epsilon abstraction of the operator:
{
#let th2 = SELECT_INTRO th1;;
th2 = |- (\n. m = n)(@n. m = n)
}
\noindent This theorem could now be used to derive a further result:
{
#EQ_MP(BETA_CONV(concl th2))th2;;
|- m = (@n. m = n)
}
\SEEALSO
EXISTS, SELECT_AX, SELECT_CONV, SELECT_ELIM, SELECT_RULE.
\ENDDOC
|
