PCHOOSE_TAC : thm_tactic

- STRUCTURE
- LIBRARY
- pair
- SYNOPSIS
- Adds the body of a paired existentially quantified theorem to the assumptions of a goal.
- DESCRIPTION
- When applied to a theorem A' |- ?p. t and a goal, CHOOSE_TAC adds t[p'/p] to the assumptions of the goal, where p' is a variant of the pair p which has no components free in the assumption list; normally p' is just p.Unless A' is a subset of A, this is not a valid tactic.
A ?- u ==================== CHOOSE_TAC (A' |- ?q. t) A u {t[p'/p]} ?- u

- FAILURE
- Fails unless the given theorem is a paired existential quantification.
- SEEALSO

HOL Kananaskis-14