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
|
\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`;;
val it : thm = |- (\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`;;
val it : thm = |- (\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.
\SEEALSO
DEPTH_BINOP_CONV, DEPTH_CONV, PROP_ATOM_CONV, REDEPTH_CONV, TOP_DEPTH_CONV,
TOP_SWEEP_CONV.
\ENDDOC
|
