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
|
\DOC CHOOSE
\TYPE {CHOOSE : ((term # thm) -> thm -> thm)}
\SYNOPSIS
Eliminates existential quantification using deduction from a
particular witness.
\KEYWORDS
rule, existential.
\DESCRIBE
When applied to a term-theorem pair {(v,A1 |- ?x. s)} and a second
theorem of the form {A2 u {{s[v/x]}} |- t}, the inference rule {CHOOSE}
produces the theorem {A1 u A2 |- t}.
{
A1 |- ?x. s[x] A2 u {{s[v/x]}} |- t
--------------------------------------- CHOOSE ("v",(A1 |- ?x. s))
A1 u A2 |- t
}
\noindent Where {v} is not free in {A2} or {t}.
\FAILURE
Fails unless the terms and theorems correspond as indicated above; in
particular, 1) {v} must be a variable and have the same type as the variable
existentially quantified over, and it must not be free in {A2} or {t};
2) the second theorem must have {s[v/x]} in its assumptions.
\SEEALSO
CHOOSE_TAC, EXISTS, EXISTS_TAC, SELECT_ELIM.
\ENDDOC
|
