----------------------------------------------------------------------
SELECT_CONV                                                     (Conv)
----------------------------------------------------------------------
SELECT_CONV : conv

SYNOPSIS
Eliminates an epsilon term by introducing an existential quantifier.

KEYWORDS
conversion, epsilon.

DESCRIBE
The conversion {SELECT_CONV} expects a boolean term of the form
{P[@x.P[x]/x]}, which asserts that the epsilon term {@x.P[x]} denotes
a value, {x} say, for which {P[x]} holds.  This assertion is equivalent
to saying that there exists such a value, and {SELECT_CONV} applied to a
term of this form returns the theorem {|- P[@x.P[x]/x] = ?x. P[x]}.

FAILURE
Fails if applied to a term that is not of the form {P[@x.P[x]/x]}.

EXAMPLE

SELECT_CONV (Term `(@n. n < m) < m`);
val it = |- (@n. n < m) < m = (?n. n < m) : thm




USES
Particularly useful in conjunction with {CONV_TAC} for proving properties
of values denoted by epsilon terms.  For example, suppose that one wishes
to prove the goal

   ([0 < m], (@n. n < m) < SUC m)

Using the built-in arithmetic theorem

   LESS_SUC  |- !m n. m < n ==> m < (SUC n)

this goal may be reduced by the tactic {MATCH_MP_TAC LESS_SUC} to
the subgoal

   ([0 < m], (@n. n < m) < m)

This is now in the correct form for using {CONV_TAC SELECT_CONV} to
eliminate the epsilon term, resulting in the existentially quantified goal

   ([0 < m], ?n. n < m)

which is then straightforward to prove.

SEEALSO
Drule.SELECT_ELIM, Drule.SELECT_INTRO, Drule.SELECT_RULE.

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