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
|
\DOC SIMPLE_EXISTS
\TYPE {SIMPLE_EXISTS : term -> thm -> thm}
\SYNOPSIS
Introduces an existential quantifier over a variable in a theorem.
\DESCRIBE
When applied to a pair consisting of a variable {v} and a theorem {|- p},
{SIMPLE_EXISTS} returns the theorem {|- ?v. p}. It is not compulsory for {v} to
appear free in {p}, but otherwise the quantification is vacuous.
\FAILURE
Fails only if {v} is not a variable.
\EXAMPLE
{
# SIMPLE_EXISTS `x:num` (REFL `x:num`);;
val it : thm = |- ?x. x = x
}
\COMMENTS
The {EXISTS} function is more general: it can introduce an existentially
quantified variable to replace chosen instances of any term in the theorem.
However, {SIMPLE_EXISTS} is easier to use when the simple case is needed.
\SEEALSO
CHOOSE, EXISTS.
\ENDDOC
|
