1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
|
\DOC SPEC_ALL
\TYPE {SPEC_ALL : thm -> thm}
\SYNOPSIS
Specializes the conclusion of a theorem with its own quantified variables.
\KEYWORDS
rule.
\DESCRIBE
When applied to a theorem {A |- !x1...xn. t}, the inference rule {SPEC_ALL}
returns the theorem {A |- t[x1'/x1]...[xn'/xn]} where the {xi'} are distinct
variants of the corresponding {xi}, chosen to avoid clashes with any variables
free in the assumption list. Normally {xi'} is just {xi}, in which case
{SPEC_ALL} simply removes all universal quantifiers.
{
A |- !x1...xn. t
--------------------------- SPEC_ALL
A |- t[x1'/x1]...[xn'/xn]
}
\FAILURE
Never fails.
\EXAMPLE
The following example shows how variables are also renamed to avoid clashing
with those in assumptions.
{
# let th = ADD_ASSUM `m = 1` ADD_SYM;;
val th : thm = m = 1 |- !m n. m + n = n + m
# SPEC_ALL th;;
val it : thm = m = 1 |- m' + n = n + m'
}
\SEEALSO
GEN, GENL, GEN_ALL, GEN_TAC, SPEC, SPECL, SPEC_ALL, SPEC_TAC.
\ENDDOC
|
