PSPEC_PAIR

PairRules.PSPEC_PAIR : thm -> term * thm

Specializes the conclusion of a theorem, returning the chosen variant.

When applied to a theorem A |- !p. t, the inference rule PSPEC_PAIR returns the term q' and the theorem A |- t[q'/p], where q' is a variant of p chosen to avoid free variable capture.

     A |- !p. t
   --------------  PSPEC_PAIR
    A |- t[q'/q]

Failure

Fails unless the theorem’s conclusion is a paired universal quantification.

Comments

This rule is very similar to plain PSPEC, except that it returns the variant chosen, which may be useful information under some circumstances.

See also

Drule.SPEC_VAR, PairRules.PGEN, PairRules.PGENL, PairRules.PGEN_TAC, PairRules.PSPEC, PairRules.PSPECL, PairRules.PSPEC_ALL