----------------------------------------------------------------------
EXISTS_LEFT                                                    (Drule)
----------------------------------------------------------------------
EXISTS_LEFT : term list -> thm -> thm

SYNOPSIS
Existentially quantifes hypotheses of a theorem.

KEYWORDS
existential, assumption, hypothesis

DESCRIBE
In this example, assume that {h1} and {h3} (only) involve the free variable {x}.

      h1, h2, h3 |- t
   --------------------- EXISTS_LEFT [``x``]
   ?x. h1 /\ h3, h2 |- t


FAILURE
{EXISTS_LEFT} will fail if the term list supplied does not consist only of free
variables

EXAMPLE
Where {th} is {[p, q, g x, h y, f x y] |- r}, and {fvx} and {fvy} are
{``x``} and {``y``},

{EXISTS_LEFT [fvx, fvy] th} is {[p, q, ?y. (?x. g x /\ f x y) /\ h y] |- r}

{EXISTS_LEFT [fvy, fvx] th} is {[p, q, ?x. (?y. h y /\ f x y) /\ g x] |- r}

USES
Where {EQ_TRANS} is
{[] |- !x y z. (x = y) /\ (y = z) ==> (x = z)}
and the current goal is {a = b},
the tactic {MATCH_MP_TAC EQ_TRANS} gives a new goal
{?y. (a = y) /\ (y = b)}
by virtue of the smart features built into {MATCH_MP_TAC}.

Where {trans_thm} is
{[] |- !x y z. (x = y) ==> (y = z) ==> (x = z)}
the same result could of course be achieved by rewriting it with
{AND_IMP_INTRO}.
But more generally, {EXISTS_LEFT} could be used as a building-block for a more
flexible tactic.
In this instance, one might start with

val trans_thm_h = UNDISCH_ALL (SPEC_ALL trans_thm) ;
EXISTS_LEFT (thm_frees trans_thm_h) trans_thm_h ;

giving {[?y. (x = y) /\ (y = z)] |- x = z}

SEEALSO
Drule.EXISTS_LEFT1, Thm.CHOOSE, Thm.EXISTS, Tactic.CHOOSE_TAC,
Tactic.EXISTS_TAC.

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