----------------------------------------------------------------------
PEXISTS                                                    (PairRules)
----------------------------------------------------------------------
PEXISTS : term * term -> thm -> thm

KEYWORDS
rule, existential.

LIBRARY
pair

SYNOPSIS
Introduces paired existential quantification given a particular witness.

DESCRIBE
When applied to a pair of terms and a theorem, where the first term a paired
existentially quantified pattern indicating the desired form of the result,
and the second a witness whose substitution for the quantified pair gives a
term which is the same as the conclusion of the theorem,
{PEXISTS} gives the desired theorem.

    A |- t[q/p]
   -------------  EXISTS ("?p. t","q")
    A |- ?p. t




FAILURE
Fails unless the substituted pattern is the same as the conclusion of the
theorem.

EXAMPLE
The following examples illustrate the various uses of {PEXISTS}:

   - PEXISTS (Term`?x. x + 2 = x + 2`, Term`1`) (REFL (Term`1 + 2`));
   > val it = |- ?x. x + 2 = x + 2 : thm

   - PEXISTS (Term`?y. 1 + y = 1 + y`, Term`2`) (REFL (Term`1 + 2`));
   > val it = |- ?y. 1 + y = 1 + y : thm

   - PEXISTS (Term`?(x,y). x + y = x + y`, Term`(1,2)`) (REFL (Term`1 + 2`));
   > val it = |- ?(x,y). x + y = x + y : thm

   - PEXISTS (Term`?(a:'a,b:'a). (a,b) = (a,b)`, Term`ab:'a#'a`)
             (REFL (Term `ab:'a#'a`));
   > val it = |- ?(a,b). (a,b) = (a,b) : thm




SEEALSO
Thm.EXISTS, PairRules.PCHOOSE, PairRules.PEXISTS_TAC.

----------------------------------------------------------------------