LEAST_ELIM_TAC : tactic
STRUCTURE
SYNOPSIS
Eliminates a LEAST term from the current goal.
DESCRIPTION
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
HOL  Kananaskis-14