SELECT_INTRO

Drule.SELECT_INTRO : (thm -> thm)

Introduces an epsilon term.

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

See also

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