Tactic.SELECT_ELIM

STRUCTURE

SYNOPSIS

Eliminates a Hilbert-choice ("selection") term from the goal.

DESCRIPTION

SELECT_ELIM_TAC searches the goal it is applied to for terms involving the Hilbert-choice operator, of the form @x. .... If such a term is found, then the tactic will produce a new goal, where the choice term has disappeared. The resulting goal will require the proof of the non-emptiness of the choice term’s predicate, and that any possible choice of value from that predicate will satisfy the original goal.

Thus, SELECT_ELIM_TAC can be seen as a higher-order match against the theorem

   |- !P Q. (?x. P x) /\ (!x. P x ==> Q x) ==> Q ($@ P)

where the new goal is the antecedent of the implication. (This theorem is SELECT_ELIM_THM, from theory bool.)

EXAMPLE

When applied to this goal,

   - SELECT_ELIM_TAC ([], ``(@x. x < 4) < 5``);
   > val it = ([([], ``(?x. x < 4) /\ !x. x < 4 ==> x < 5``)], fn) :
       (term list * term) list * (thm list -> thm)

the resulting goal requires the proof of the existence of a number less than 4, and also that any such number is also less than 5.

FAILURE

Fails if there are no choice terms in the goal.

COMMENTS

If the choice-term’s predicate is everywhere false, goals involving such terms will be true only if the choice of term makes no difference at all. Such situations can be handled with the use of SPEC_TAC. Note also that the choice of select term to eliminate is made in an unspecified manner.

SEEALSO

DEEP_INTRO_TAC, SELECT_ELIM, SELECT_INTRO, SELECT_RULE, SPEC_TAC