PEXISTS_UNIQUE_CONV : conv

- STRUCTURE
- LIBRARY
- pair
- SYNOPSIS
- Expands with the definition of paired unique existence.
- DESCRIPTION
- Given a term of the form "?!p. t[p]", the conversion PEXISTS_UNIQUE_CONV proves that this assertion is equivalent to the conjunction of two statements, namely that there exists at least one pair p such that t[p], and that there is at most one value p for which t[p] holds. The theorem returned is:where p' is a primed variant of the pair p none of the components of which appear free in the input term. Note that the quantified pair p need not in fact appear free in the body of the input term. For example, PEXISTS_UNIQUE_CONV "?!(x,y). T" returns the theorem:
|- (?!p. t[p]) = (?p. t[p]) /\ (!p p'. t[p] /\ t[p'] ==> (p = p'))

|- (?!(x,y). T) = (?(x,y). T) /\ (!(x,y) (x',y'). T /\ T ==> ((x,y) = (x',y')))

- FAILURE
- PEXISTS_UNIQUE_CONV tm fails if tm does not have the form "?!p.t".
- SEEALSO

HOL Kananaskis-14