SELECT_RULE : thm -> thm
STRUCTURE
Drule
SYNOPSIS
Introduces an epsilon term in place of an existential quantifier.
DESCRIPTION
The inference rule SELECT_RULE expects a theorem asserting the existence of a value x such that P holds. The equivalent assertion that the epsilon term @x.P denotes a value of x for which P holds is returned as a theorem. 
       A |- ?x. P
   ------------------  SELECT_RULE
    A |- P[(@x.P)/x]

FAILURE
Fails if applied to a theorem the conclusion of which is not existentially quantified.
EXAMPLE
The axiom INFINITY_AX in the theory ind is of the form: 
   |- ?f. ONE_ONE f /\ ~ONTO f
Applying SELECT_RULE to this theorem returns the following. 
   - SELECT_RULE INFINITY_AX;
   > val it =
     |- ONE_ONE (@f. ONE_ONE f /\ ~ONTO f) /\ ~ONTO @f. ONE_ONE f /\ ~ONTO f
     : thm

USES
May be used to introduce an epsilon term to permit rewriting with a constant defined using the epsilon operator.
SEEALSO
CHOOSE, SELECT_CONV, SELECT_ELIM, SELECT_INTRO
HOL  Trindemossen-1