Filter
Top Products
68 CHAPTER 8. CONVERSIONS
operators’. These allow one to construct composite conversions in a user-defined
way. For example, the conversional THENC, used infix, uses one conversion and then
afterwards, another, e.g.
#(BETA_CONV THENC NUM_RED_CONV) ‘(\x. x + 1) 2‘;;
it : thm = |- (\x. x + 1) 2 = 3
The conversional REPEATC allows one to use a conversion repeatedly until it fails
(maybe zero times), e.g.
#REPEATC BETA_CONV ‘23‘;;
it : thm = |- 23 = 23
#REPEATC BETA_CONV ‘(\x. x + 1)‘;;
it : thm = |- (\x. x + 1) = (\x. x + 1)
#REPEATC BETA_CONV ‘(\x. x + 1) 2‘;;
it : thm = |- (\x. x + 1) 2 = 2 + 1
#REPEATC BETA_CONV ‘(\x. (\y. x + y) 2) 1‘;;
it : thm = |- (\x. (\y. x + y) 2) 1 = 1 + 2
8.2 Depth conversions
The conversions above are still only applied at the top level of a term. For example,
the following fails because the beta-redex is deeper inside the term than expected:
#BETA_CONV ‘1 + (\x. x + 1) 2‘;;
Uncaught exception: Failure "BETA_CONV: Not a beta-redex"
However there is an additional set of conversionals that apply the given conver-
sion at depth inside the term. For example ONCE DEPTH CONV applies a conversion
to the first applicable term(s) encountered in a top-down traversal of the term. No
deeper terms are examined, but several terms can be converted provided they are
disjoint:
#ONCE_DEPTH_CONV NUM_RED_CONV ‘1 + (2 + 3)‘;;
it : thm = |- 1 + 2 + 3 = 1 + 5
#ONCE_DEPTH_CONV NUM_RED_CONV ‘(1 + 1) * (1 + 1)‘;;
it : thm = |- (1 + 1) * (1 + 1) = 2 * 2
Conversions like NUM RED CONV can be used to reduce a term completely by ap-
plying it in a single bottom-up sweep. This is done by the conversional DEPTH CONV,
e.g.
#DEPTH_CONV NUM_RED_CONV ‘7 * (3 EXP 10) + 11‘;;
it : thm = |- 7 * 3 EXP 10 + 11 = 413354
However, this isn’t always what’s needed; sometimes the act of applying a
conversion at one level can create new applicable terms lower down; in this case
DEPTH CONV will not reexamine them. Two other conversionals, TOP DEPTH CONV
and REDEPTH CONV, will keep applying conversions as long as possible all over the
term.