----------------------------------------------------------------------
LEAST_ELIM_TAC                                                (numLib)
----------------------------------------------------------------------
LEAST_ELIM_TAC : tactic

SYNOPSIS
Eliminates a {LEAST} term from the current goal.

KEYWORDS


DESCRIBE
{LEAST_ELIM_TAC} searches the goal it is applied to for free sub-terms
involving the {LEAST} operator, of the form {$LEAST P} ({P} will
usually be an abstraction).  If such a term is found, the tactic
produces a new goal where instances of the {LEAST}-term have
disappeared.  The resulting goal will require the proof that there
exists a value satisfying {P}, and that a minimal value satisfies the
original goal.

Thus, {LEAST_ELIM_TAC} can be seen as a higher-order match against the
theorem

   |- !P Q.
         (?n. P x) /\ (!n. (!m. m < n ==> ~P m) /\ P n ==> Q n) ==>
         Q ($LEAST P)

where the new goal is the antecdent of the implication.  (This theorem
is {LEAST_ELIM}, from theory {while}.)

FAILURE
The tactic fails if there is no free {LEAST}-term in the goal.

EXAMPLE
When applied to the goal

   ?- (LEAST n. 4 < n) = 5

the tactic {LEAST_ELIM_TAC} produces

   ?- (?n. 4 < n) /\ !n. (!m. m < n ==> ~(4 < m)) /\ 4 < n ==> (n = 5)




COMMENTS
This tactic assumes that there is indeed a least number satisfying the
given predicate.  If there is not, then the {LEAST}-term will have an
arbitrary value, and the proof should proceed by showing that the
enclosing predicate {Q} holds for all possible numbers.

If there are multiple different {LEAST}-terms in the goal, then
{LEAST_ELIM_TAC} will pick the first free {LEAST}-term returned by the
standard {find_terms} function.

SEEALSO
Tactic.DEEP_INTRO_TAC, Tactic.SELECT_ELIM_TAC.

----------------------------------------------------------------------