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
39
40
41
42
43
|
\DOC SUB_CONV
\TYPE {SUB_CONV : (conv -> conv)}
\SYNOPSIS
Applies a conversion to the top-level subterms of a term.
\KEYWORDS
conversional.
\DESCRIBE
For any conversion {c}, the function returned by {SUB_CONV c} is a conversion
that applies {c} to all the top-level subterms of a term. If the conversion
{c} maps {t} to {|- t = t'}, then {SUB_CONV c} maps an abstraction {"\x.t"} to
the theorem:
{
|- (\x.t) = (\x.t')
}
\noindent That is, {SUB_CONV c "\x.t"} applies {c} to the body of the
abstraction {"\x.t"}. If {c} is a conversion that maps {"t1"} to the theorem
{|- t1 = t1'} and {"t2"} to the theorem {|- t2 = t2'}, then the conversion
{SUB_CONV c} maps an application {"t1 t2"} to the theorem:
{
|- (t1 t2) = (t1' t2')
}
\noindent That is, {SUB_CONV c "t1 t2"} applies {c} to the both the operator
{t1} and the operand {t2} of the application {"t1 t2"}. Finally, for any
conversion {c}, the function returned by {SUB_CONV c} acts as the identity
conversion on variables and constants. That is, if {"t"} is a variable or
constant, then {SUB_CONV c "t"} returns {|- t = t}.
\FAILURE
{SUB_CONV c tm} fails if {tm} is an abstraction {"\x.t"} and the conversion {c}
fails when applied to {t}, or if {tm} is an application {"t1 t2"} and the
conversion {c} fails when applied to either {t1} or {t2}. The function
returned by {SUB_CONV c} may also fail if the ML function {c:term->thm} is not,
in fact, a conversion (i.e. a function that maps a term {t} to a theorem
{|- t = t'}).
\SEEALSO
ABS_CONV, RAND_CONV, RATOR_CONV.
\ENDDOC
|
