Conv.SELECT

STRUCTURE

SYNOPSIS

Eliminates an epsilon term by introducing an existential quantifier.

DESCRIPTION

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

SELECT_ELIM, SELECT_INTRO, SELECT_RULE