PairRules.PCHOOSE

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:

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

then

    A ?- s1
   ==========  CHOOSE_THEN ttac (A' |- ?q. t)
    B ?- s2

This is invalid unless A' is a subset of A.

FAILURE

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

SEEALSO

CHOOSE_THEN, PCHOOSE_TAC, P_PCHOOSE_THEN