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 and with the names of constants. 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 the names of constants.
{
#let v=mk_var(`T`,":bool") in ASSUME "!^v. ^v \/ ~^v";;
!T. T \/ ~T |- !T. T \/ ~T
#SPEC_ALL it;;
!T. T \/ ~T |- T' \/ ~T'
}
\SEEALSO
GEN, GENL, GEN_ALL, GEN_TAC, SPEC, SPECL, SPEC_ALL, SPEC_TAC.
\ENDDOC
|
