SELECT_RULE : thm -> thm

- STRUCTURE
- 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:Applying SELECT_RULE to this theorem returns the following.
|- ?f. ONE_ONE f /\ ~ONTO f

- 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

HOL Kananaskis-14