CHOOSE_THEN : thm_tactical

- STRUCTURE
- SYNOPSIS
- Applies a tactic generated from the body of existentially quantified theorem.
- DESCRIPTION
- When applied to a theorem-tactic ttac, an existentially quantified theorem A' |- ?x. t, and a goal, CHOOSE_THEN applies the tactic ttac (t[x'/x] |- t[x'/x]) to the goal, where x' is a variant of x chosen not to be free in the assumption list of the goal. Thus if:then
A ?- s1 ========= ttac (t[x'/x] |- t[x'/x]) B ?- s2

This is invalid unless A' is a subset of A.A ?- s1 ========== CHOOSE_THEN ttac (A' |- ?x. t) B ?- s2

- FAILURE
- Fails unless the given theorem is existentially quantified, or if the resulting tactic fails when applied to the goal.
- EXAMPLE
- This theorem-tactical and its relatives are very useful for using existentially quantified theorems. For example one might use the inbuilt theoremto help solve the goal
LESS_ADD_1 = |- !m n. n < m ==> (?p. m = n + (p + 1))

by starting with the following tactic?- x < y ==> 0 < y * y

which reduces the goal toDISCH_THEN (CHOOSE_THEN SUBST1_TAC o MATCH_MP LESS_ADD_1)

which can then be finished off quite easily, by, for example:?- 0 < ((x + (p + 1)) * (x + (p + 1)))

REWRITE_TAC[ADD_ASSOC, SYM (SPEC_ALL ADD1), MULT_CLAUSES, ADD_CLAUSES, LESS_0]

- SEEALSO

HOL Kananaskis-14