P_PCHOOSE_TAC

PairRules.P_PCHOOSE_TAC : (term -> thm_tactic)

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

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.

See also

Tactic.X_CHOOSE_TAC, PairRules.PCHOOSE, PairRules.PCHOOSE_THEN, PairRules.P_PCHOOSE_THEN