SELECT_CONV : conv

- 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 goalUsing the built-in arithmetic theorem
([0 < m], (@n. n < m) < SUC m)

this goal may be reduced by the tactic MATCH_MP_TAC LESS_SUC to the subgoalLESS_SUC |- !m n. m < n ==> m < (SUC n)

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) < m)

which is then straightforward to prove.([0 < m], ?n. n < m)

- SEEALSO

HOL Kananaskis-14