SPECL : term list -> thm -> thm

- STRUCTURE
- SYNOPSIS
- Specializes zero or more variables in the conclusion of a theorem.
- DESCRIPTION
- 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
- Fails unless each of the terms is of the same type as that of the appropriate quantified variable in the original theorem.
- EXAMPLE
- The following is a specialization of a theorem from theory arithmetic.
- arithmeticTheory.LESS_EQ_LESS_EQ_MONO; > val it = |- !m n p q. m <= p /\ n <= q ==> m + n <= p + q : thm - SPECL (map Term [`1`, `2`, `3`, `4`]) it; > val it = |- 1 <= 3 /\ 2 <= 4 ==> 1 + 2 <= 3 + 4 : thm

- SEEALSO

HOL Kananaskis-14