----------------------------------------------------------------------
P_PCHOOSE_TAC                                              (PairRules)
----------------------------------------------------------------------
P_PCHOOSE_TAC : (term -> thm_tactic)

KEYWORDS
tactic, witness, quantifier, existential.

LIBRARY
pair

SYNOPSIS
Assumes a theorem, with existentially quantified pair replaced by a given
witness.

DESCRIBE
{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
Tactic.X_CHOOSE_TAC, PairRules.PCHOOSE, PairRules.PCHOOSE_THEN,
PairRules.P_PCHOOSE_THEN.

----------------------------------------------------------------------