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
|
\DOC SELECT_ELIM
\TYPE {SELECT_ELIM : (thm -> (term # thm) -> thm)}
\SYNOPSIS
Eliminates an epsilon term, using deduction from a particular instance.
\KEYWORDS
rule, epsilon.
\DESCRIBE
{SELECT_ELIM} expects two arguments, a theorem {th1}, and a pair
{(v,th2):(term # thm)}. The conclusion of {th1} must have the form {P($@ P)},
which asserts that the epsilon term {$@ P} denotes some value at which
{P} holds. The variable {v} appears only in the assumption {P v} of
the theorem {th2}. The conclusion of the resulting theorem matches
that of {th2}, and the hypotheses include the union of all hypotheses
of the premises excepting {P v}.
{
A1 |- P($@ P) A2 u {{P v}} |- t
----------------------------------- SELECT_ELIM th1 (v,th2)
A1 u A2 |- t
}
\noindent where {v} is not free in {A2}. If {v} appears in the conclusion of
{th2}, the epsilon term will NOT be eliminated, and the conclusion will be
{t[$@ P/v]}.
\FAILURE
Fails if the first theorem is not of the form {A1 |- P($@ P)}, or if
the variable {v} occurs free in any other assumption of {th2}.
\EXAMPLE
If a property of functions is defined by:
{
INCR = |- !f. INCR f = (!t1 t2. t1 < t2 ==> (f t1) < (f t2))
}
\noindent The following theorem can be proved.
{
th1 = |- INCR(@f. INCR f)
}
\noindent Additionally, if such a function is assumed to exist, then one
can prove that there also exists a function which is injective (one-to-one) but
not surjective (onto).
{
th2 = [ INCR g ] |- ?h. ONE_ONE h /\ ~ONTO h
}
\noindent These two results may be combined using {SELECT_ELIM} to
give a new theorem:
{
#SELECT_ELIM th1 ("g:num->num", th2);;
|- ?h. ONE_ONE h /\ ~ONTO h
}
\USES
This rule is rarely used. The equivalence of {P($@ P)} and {$? P}
makes this rule fundamentally similar to the {?}-elimination rule {CHOOSE}.
\SEEALSO
CHOOSE, SELECT_AX, SELECT_CONV, SELECT_INTRO, SELECT_RULE.
\ENDDOC
|
