GPSPEC

PairRules.GPSPEC : (thm -> thm)

Specializes the conclusion of a theorem with unique pairs.

When applied to a theorem A |- !p1...pn. t, where the number of universally quantified variables may be zero, GPSPEC returns A |- t[g1/p1]...[gn/pn], where the gi is paired structures of the same structure as pi and made up of distinct variables , chosen by genvar.

        A |- !p1...pn. t
   -------------------------  GPSPEC
    A |- t[g1/p1]...[gn/pn]

Failure

Never fails.

GPSPEC is useful in writing derived inference rules which need to specialize theorems while avoiding using any variables that may be present elsewhere.

See also

Drule.GSPEC, PairRules.PGEN, PairRules.PGENL, Term.genvar, PairRules.PGEN_TAC, PairRules.PSPEC, PairRules.PSPECL, PairRules.PSPEC_ALL, PairRules.PSPEC_TAC, PairRules.PSPEC_PAIR