PSPEC
PairRules.PSPEC : (term -> thm -> thm)
Specializes the conclusion of a theorem.
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
See also
Thm.SPEC, PairRules.IPSPEC,
PairRules.PSPECL,
PairRules.PSPEC_ALL,
PairRules.PGEN,
PairRules.PGENL