P_PCHOOSE_TAC : (term -> thm_tactic)

- STRUCTURE
- LIBRARY
- pair
- SYNOPSIS
- Assumes a theorem, with existentially quantified pair replaced by a given witness.
- DESCRIPTION
- P_PCHOOSE_TAC expects a pair q and theorem with a paired existentially quantified conclusion. When applied to a goal, it adds a new assumption obtained by introducing the pair q as a witness for the pair p whose existence is asserted in the theorem.
A ?- t =================== P_CHOOSE_TAC "q" (A1 |- ?p. u) A u {u[q/p]} ?- t ("y" not free anywhere)

- FAILURE
- Fails if the theorem’s conclusion is not a paired existential quantification, or if the first argument is not a paired structure of variables. Failures may arise in the tactic-generating function. An invalid tactic is produced if the introduced variable is free in u or t, or if the theorem has any hypothesis which is not alpha-convertible to an assumption of the goal.
- SEEALSO

HOL Kananaskis-14