FDL > PVS > Prelude > exists1 : Theory

PVS-2.4 prelude.pvs

 exists1 provides a unique existence function; it takes a predicate
 and asserts that there is one and only one element of the type that
 satisfies the predicate.  The expression "exists1! (x:t): p(x)" is
 translated to "exists1(LAMBDA (x:t): p(x))".

exists1 [T:TYPE] : THEORY
BEGIN

x: VAR T

y: VAR T

p: VAR pred[T]

q: VAR pred[T]

unique?(p): bool = FORALL x, y : (p(x) AND p(y)) IMPLIES (x = y);

exists1(p): bool = (EXISTS x : p(x)) AND unique?(p);

unique lem: LEMMA (FORALL x : p(x) IMPLIES q(x)) IMPLIES unique?(q) IMPLIES unique?(p)

exists1 lem: LEMMA (exists1! x : p(x)) IMPLIES (EXISTS x : p(x))

END exists1