----------------------------------------------------------------------
SELECT_INTRO                                                   (Drule)
----------------------------------------------------------------------
SELECT_INTRO : (thm -> thm)

SYNOPSIS
Introduces an epsilon term.

KEYWORDS
rule, epsilon.

DESCRIBE
{SELECT_INTRO} takes a theorem with an applicative conclusion, say
{P x}, and returns a theorem with the epsilon term {$@ P} in place
of the original operand {x}.

     A |- P x
   --------------  SELECT_INTRO
    A |- P($@ P)

The returned theorem asserts that {$@ P} denotes some value
at which {P} holds.

FAILURE
Fails if the conclusion of the theorem is not an application.

EXAMPLE
Given the theorem

   th1 = |- (\n. m = n)m

applying {SELECT_INTRO} replaces the second occurrence of {m} with the
epsilon abstraction of the operator:

   - val th2 = SELECT_INTRO th1;
   val th2 = |- (\n. m = n)(@n. m = n) : thm

This theorem could now be used to derive a further result:

   - EQ_MP (BETA_CONV(concl th2)) th2;
   val it = |- m = (@n. m = n) : thm


SEEALSO
Thm.EXISTS, Conv.SELECT_CONV, Drule.SELECT_ELIM, Drule.SELECT_RULE.

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