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
|
\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} is not, in fact,
a conversion (i.e. a function that maps a term {t} to a theorem {|- t = t'}).
\SEEALSO
ABS_CONV, COMB_CONV, RAND_CONV, RATOR_CONV.
\ENDDOC
|
