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 ABS_CONV
\TYPE {ABS_CONV : conv -> conv}
\SYNOPSIS
Applies a conversion to the body of an abstraction.
\KEYWORDS
conversional, abstraction.
\DESCRIBE
If {c} is a conversion that maps a term {`t`} to the theorem {|- t = t'}, then
the conversion {ABS_CONV c} maps abstractions of the form {`\x. t`} to theorems
of the form:
{
|- (\x. t) = (\x. t')
}
\noindent That is, {ABS_CONV c `\x. t`} applies {c} to the body of the
abstraction {`\x. t`}.
\FAILURE
{ABS_CONV c tm} fails if {tm} is not an abstraction or if {tm} has the form
{`\x. t`} but the conversion {c} fails when applied to the term {t}, or if the
theorem returned has assumptions in which the abstracted variable {x} is free.
The function returned by {ABS_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'}).
\EXAMPLE
{
# ABS_CONV SYM_CONV `\x. 1 = x`;;
val it : thm = |- (\x. 1 = x) = (\x. x = 1)
}
\SEEALSO
GABS_CONV, RAND_CONV, RATOR_CONV, SUB_CONV.
\ENDDOC
|
