/
Conv.RESORT_FORALL_CONV.doc
38 lines (30 loc) · 1.25 KB
/
Conv.RESORT_FORALL_CONV.doc
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
\TYPE {RESORT_FORALL_CONV : (term list -> term list) -> conv}
\SYNOPSIS
Reorders bound variables under universal quantifiers.
\KEYWORDS
\DESCRIBE
A call to {RESORT_FORALL_CONV f t} strips the outer
universally-quantified variables of {t}, giving a list {vs}, such that
{t} is of the form {!vs. body}. The list {vs} is then passed to the
function argument {f}. The result of the call {f vs} is expected to
be a new list of variables {vs'}, and the result of the conversion is
the theorem
{
|- (!vs. body) <=> (!vs'. body)
}
The function {f} is generally expected to return a permutation of the
variables appearing in the term {vs}, but may in fact introduce fresh
variables that are fresh for {body}, and may also remove variables
from {vs} that also don't appear in {body}.
\FAILURE
Given a term {t}, fails if {t} is not of boolean type. Fails if when
applied to the outermost universally quantified variables (permitted
to be the empty list) the function {f} returns a list of terms that
are not all variables. Also fails if either {f} returns a list that
does not include variables from {vs} that appear in the body of {t},
or if it includes variables that are in the body, but which were not
originally bound.
\SEEALSO
Conv.RESORT_EXISTS_CONV.
\ENDDOC