----------------------------------------------------------------------
CHOOSE_TAC                                                    (Tactic)
----------------------------------------------------------------------
CHOOSE_TAC : thm_tactic

SYNOPSIS
Adds the body of an existentially quantified theorem to the assumptions of
a goal.

KEYWORDS
tactic, existential.

DESCRIBE
When applied to a theorem {A' |- ?x. t} and a goal, {CHOOSE_TAC} adds
{t[x'/x]} to the assumptions of the goal, where {x'} is a variant of
{x} which is not free in the goal or assumption list; normally {x'} is
just {x}.

         A ?- u
   ====================  CHOOSE_TAC (A' |- ?x. t)
    A u {t[x'/x]} ?- u

Unless {A'} is a subset of {A}, this is not a valid tactic.

FAILURE
Fails unless the given theorem is existentially quantified.

EXAMPLE
Suppose we have a goal asserting that the output of an electrical circuit
(represented as a boolean-valued function) will become high at some time:

   ?- ?t. output(t)

and we have the following theorems available:

   t1 = |- ?t. input(t)
   t2 = !t. input(t) ==> output(t+1)

Then the goal can be solved by the application of:

   CHOOSE_TAC th1
     THEN EXISTS_TAC (Term `t+1`)
     THEN UNDISCH_TAC (Term `input (t:num) :bool`)
     THEN MATCH_ACCEPT_TAC th2


COMMENTS
To do similarly with several existentially quantified variables, use
{REPEAT_TCL CHOOSE_THEN ASSUME_TAC} in place of {CHOOSE_TAC}

SEEALSO
Thm_cont.CHOOSE_THEN, Tactic.X_CHOOSE_TAC, Thm_cont.REPEAT_TCL.

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