SPECL : term list -> thm -> thm
Specializes zero or more variables in the conclusion of a theorem.
When applied to a term list [u1;...;un] and a theorem
A |- !x1...xn. t, the inference rule SPECL returns the theorem
A |- t[u1/x1]...[un/xn], where the substitutions are made
sequentially left-to-right in the same way as for SPEC, with the same
sort of alpha-conversions applied to t if necessary to ensure that no
variables which are free in ui become bound after substitution.
It is permissible for the term-list to be empty, in which case
the application of SPECL has no effect.
A |- !x1...xn. t
-------------------------- SPECL [`u1`;...;`un`]
A |- t[u1/x1]...[un/xn]
- FAILURE CONDITIONS
Fails unless each of the terms is of the same as that of the
appropriate quantified variable in the original theorem.
The following is a specialization of a theorem from theory arithmetic.
# let t = ARITH_RULE `!m n p q. m <= p /\ n <= q ==> (m + n) <= (p + q)`;;
val t : thm = |- !m n p q. m <= p /\ n <= q ==> m + n <= p + q
# SPECL [`1`; `2`; `3`; `4`] t;;
val it : thm = |- 1 <= 3 /\ 2 <= 4 ==> 1 + 2 <= 3 + 4
In order to specialize variables while also instantiating types of polymorphic
variables, use ISPECL instead.
- SEE ALSO
GEN, GENL, GEN_ALL, GEN_TAC, SPEC, SPEC_ALL, SPEC_TAC.