PCHOOSE_THEN : thm_tactical

- STRUCTURE
- LIBRARY
- pair
- SYNOPSIS
- Applies a tactic generated from the body of paired existentially quantified theorem.
- DESCRIPTION
- When applied to a theorem-tactic ttac, a paired existentially quantified theorem:
A' |- ?p. t

and a goal, CHOOSE_THEN applies the tactic ttac (t[p'/p] |- t[p'/p]) to the goal, where p' is a variant of the pair p chosen to have no components free in the assumption list of the goal. Thus if:

thenA ?- s1 ========= ttac (t[q'/q] |- t[q'/q]) B ?- s2

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

- FAILURE
- Fails unless the given theorem is a paired existential quantification, or if the resulting tactic fails when applied to the goal.
- SEEALSO

HOL Kananaskis-14