----------------------------------------------------------------------
PSPEC                                                      (PairRules)
----------------------------------------------------------------------
PSPEC : (term -> thm -> thm)

KEYWORDS
rule.

LIBRARY
pair

SYNOPSIS
Specializes the conclusion of a theorem.

DESCRIBE
When applied to a term {q} and a theorem {A |- !p. t}, then {PSPEC} returns
the theorem {A |- t[q/p]}.
If necessary, variables will be renamed prior to the specialization to ensure
that {q} is free for {p} in {t}, that is,
no variables free in {q} become bound after substitution.

     A |- !p. t
   --------------  PSPEC "q"
    A |- t[q/p]




FAILURE
Fails if the theorem’s conclusion is not a paired universal quantification,
or if {p} and {q} have different types.

EXAMPLE
{PSPEC} specialised paired quantifications.

   - PSPEC (Term `(1,2)`) (ASSUME (Term`!(x,y). (x + y) = (y + x)`));
   > val it =  [.] |- 1 + 2 = 2 + 1 : thm


{PSPEC} treats paired structures of variables as variables and
preserves structure accordingly.

   - PSPEC (Term `x:'a#'a`) (ASSUME (Term `!(x:'a,y:'a). (x,y) = (x,y)`));
   > val it =  [.] |- x = x : thm




SEEALSO
Thm.SPEC, PairRules.IPSPEC, PairRules.PSPECL, PairRules.PSPEC_ALL,
PairRules.PGEN, PairRules.PGENL.

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