RESQ_SPEC : (term -> thm -> thm)
STRUCTURE
SYNOPSIS
Specializes the conclusion of a restricted universally quantified theorem.
DESCRIPTION
When applied to a term u and a theorem A |- !x::P. t, RESQ_SPEC returns the theorem A, P u |- 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, P u |- t[u/x]
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.
   #let th = RESQ_GEN "x:num" "\y.0<y" (REFL "x:num");;
   th = |- !x :: \y. 0 < y. x = x

   #RESQ_SPEC "y:num" th;;
   (\y'. 0 < y')y |- y = y
SEEALSO
HOL  Kananaskis-10