1\DOC CHOOSE
2
3\TYPE {CHOOSE : term * thm -> thm -> thm}
4
5\SYNOPSIS
6Eliminates existential quantification using deduction from a
7particular witness.
8
9\KEYWORDS
10rule, existential.
11
12\DESCRIBE
13When applied to a term-theorem pair {(v,A1 |- ?x. s)} and a second
14theorem of the form {A2 u {s[v/x]} |- t}, the inference rule {CHOOSE}
15produces the theorem {A1 u A2 |- t}.
16{
17    A1 |- ?x. s        A2 u {s[v/x]} |- t
18   ---------------------------------------  CHOOSE (v,(A1 |- ?x. s))
19                A1 u A2 |- t
20}
21Where {v} is not free in {A1}, {A2} or {t}.
22
23\FAILURE
24Fails unless the terms and theorems correspond as indicated above; in
25particular {v} must have the same type as the variable existentially
26quantified over, and must not be free in {A1}, {A2} or {t}.
27
28\SEEALSO
29Tactic.CHOOSE_TAC, Thm.EXISTS, Tactic.EXISTS_TAC, Drule.SELECT_ELIM.
30\ENDDOC
31