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
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
|
\DOC ONCE_DEPTH_CONV
\TYPE {ONCE_DEPTH_CONV : (conv -> conv)}
\SYNOPSIS
Applies a conversion once to the first suitable sub-term(s) encountered in
top-down order.
\KEYWORDS
conversional.
\DESCRIBE
{ONCE_DEPTH_CONV c tm} applies the conversion {c} once to the first subterm or
subterms encountered in a top-down `parallel' search of the term {tm} for which
{c} succeeds. If the conversion {c} fails on all subterms of {tm}, the theorem
returned is {|- tm = tm}.
\FAILURE
Never fails.
\EXAMPLE
The following example shows how {ONCE_DEPTH_CONV} applies a conversion to only
the first suitable subterm(s) found in a top-down search:
{
#ONCE_DEPTH_CONV BETA_CONV "(\x. (\y. y + x) 1) 2";;
|- (\x. (\y. y + x)1)2 = (\y. y + 2)1
}
\noindent Here, there are two beta-redexes in the input term. One of these
occurs within the other, so {BETA_CONV} is applied only to the outermost one.
Note that the supplied conversion is applied by {ONCE_DEPTH_CONV} to all
independent subterms at which it succeeds. That is, the conversion is applied
to every suitable subterm not contained in some other subterm for which the
conversions also succeeds, as illustrated by the following example:
{
#ONCE_DEPTH_CONV num_CONV "(\x. (\y. y + x) 1) 2";;
|- (\x. (\y. y + x)1)2 = (\x. (\y. y + x)(SUC 0))(SUC 1)
}
\noindent Here {num_CONV} is applied to both {1} and {2}, since neither term
occurs within a larger subterm for which the conversion {num_CONV} succeeds.
\USES
{ONCE_DEPTH_CONV} is frequently used when there is only one subterm to which
the desired conversion applies. This can be much faster than using other
functions that attempt to apply a conversion to all subterms of a term (e.g.
{DEPTH_CONV}). If, for example, the current goal in a goal-directed proof
contains only one beta-redex, and one wishes to apply {BETA_CONV} to it, then
the tactic
{
CONV_TAC (ONCE_DEPTH_CONV BETA_CONV)
}
\noindent may, depending on where the beta-redex occurs, be much faster than
{
CONV_TAC (TOP_DEPTH_CONV BETA_CONV)
}
{ONCE_DEPTH_CONV c} may also be used when the supplied conversion {c} never
fails, in which case using a conversion such as {DEPTH_CONV c}, which
applies {c} repeatedly would never terminate.
\COMMENTS
The implementation of this function uses failure to avoid rebuilding
unchanged subterms. That is to say, during execution the failure string
{`QCONV`} may be generated and later trapped. The behaviour of the function
is dependent on this use of failure. So, if the conversion given as argument
happens to generate a failure with string {`QCONV`}, the operation of
{ONCE_DEPTH_CONV} will be unpredictable.
\SEEALSO
DEPTH_CONV, REDEPTH_CONV, TOP_DEPTH_CONV, ONCE_REW_DEPTH_CONV.
\ENDDOC
|
