SELECT_CONV : term -> thm

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 CONDITIONS

Fails if applied to a term that is not of the form `P[@x.P[x]/x]`.

EXAMPLE

  # SELECT_CONV `(@n. n < m) < m`;;
  val it : thm = |- (@n. n < m) < m <=> (?n. n < m)

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

  # g `!m. 0 < m ==> (@n. n < m) < SUC m`;;

We start off:

  # e(REPEAT STRIP_TAC THEN
      MATCH_MP_TAC(ARITH_RULE `!m n. m < n ==> m < SUC n`));;
  val it : goalstack = 1 subgoal (1 total)

   0 [`0 < m`]

  `(@n. n < m) < m`

This is now in the correct form for using SELECT_CONV:

  # e(CONV_TAC SELECT_CONV);;
  val it : goalstack = 1 subgoal (1 total)

   0 [`0 < m`]

  `?n. n < m`

and the resulting subgoal is straightforward to prove, e.g. by ASM_MESON_TAC[] or EXISTS_TAC `0` THEN ASM_REWRITE_TAC[].

SEE ALSO

SELECT_ELIM, SELECT_RULE.