1\DOC EXISTS
2
3\TYPE {EXISTS : term * term -> thm -> thm}
4
5\SYNOPSIS
6Introduces existential quantification given a particular witness.
7
8\KEYWORDS
9rule, existential.
10
11\DESCRIBE
12When applied to a pair of terms and a theorem, the first term an existentially
13quantified pattern indicating the desired form of the result, and the second a
14witness whose substitution for the quantified variable gives a term which is
15the same as the conclusion of the theorem, {EXISTS} gives the desired theorem.
16{
17    A |- p[u/x]
18   -------------  EXISTS (?x. p, u)
19    A |- ?x. p
20}
21
22
23\FAILURE
24Fails unless the substituted pattern is the same as the conclusion of the
25theorem.
26
27\EXAMPLE
28The following examples illustrate how it is possible to deduce different
29things from the same theorem:
30{
31   - EXISTS (Term `?x. x=T`,T) (REFL T);
32   > val it = |- ?x. x = T : thm
33
34   - EXISTS (Term `?x:bool. x=x`,T) (REFL T);
35   > val it = |- ?x. x = x : thm
36}
37
38
39\SEEALSO
40Thm.CHOOSE, Drule.SIMPLE_EXISTS, Tactic.EXISTS_TAC.
41\ENDDOC
42