RESQ_SPEC
res_quanLib.RESQ_SPEC : term -> thm -> thm
Specializes the conclusion of a possibly-restricted universally quantified theorem.
When applied to a term u and a theorem A |- !x::P. t, RESQ_SPEC
returns the theorem A, u IN P |- t[u/x]. If necessary, variables will
be renamed prior to the specialization to ensure that u is free for
x in t, that is, no variables free in u become bound after
substitution.
A |- !x::P. t
--------------------- RESQ_SPEC "u"
A, u IN P |- t[u/x]
Additionally, if the input theorem is a standard universal quantification, then RESQ_SPEC behaves like SPEC.
Failure
Fails if the theorem's conclusion is not restricted universally quantified, or if type instantiation fails.
Example
The following example shows how RESQ_SPEC renames bound variables if
necessary, prior to substitution: a straightforward substitution would
result in the clearly invalid theorem (\y. 0 < y) y |- y = y.
> val th = RESQ_GEN ``x:num`` ``\y. 0 < y`` (REFL ``x:num``);
val th = |- !x :: \y. 0 < y. x = x : thm
> RESQ_SPEC ``y:num`` th;
val it = (\y'. 0 < y') y |- y = y : thm