Filter
Top Products
Chapter 8
Conversions
A conversion in HOL is a derived rule of type term -> thm that when given a
term t, always returns (assuming it doesn’t fail) a theorem of the form |- t = t’.
Conversions were introduced into Cambridge LCF by Paulson (1983), who showed
that they gave a convenient and regular way of implementing many handy derived
rules. Conversions can be considered as transforming a term into an equal one,
and also giving a theorem to justify this equality. They are therefore useful as
building-blocks for larger transformations, similarly justified.
HOL has a variety of built-in conversions, and they often have names ending
in CONV as a reminder that they are conversions. Rather trivially, for example, the
primitive inference rule REFL is a conversion, which takes a term t and returns a
theorem |- t = t. If we think of conversions as transforming one term to another,
REFL is a sort of ‘identity’ conversion. In fact, for this reason, it is given a new
name ALL CONV, since it is a conversion that always, trivially, works on any term.
Its converse, in a sense, is a conversion NO CONV which always fails:
#let (ALL_CONV:conv) = REFL;;
ALL_CONV : conv = <fun>
#let (NO_CONV:conv) = fun tm -> failwith "NO_CONV";;
NO_CONV : conv = <fun>
A slightly more interesting conversion is BETA CONV, which performs a beta re-
duction step on terms of the form (\x. ...) t:
#BETA_CONV ‘(\x. x + 1) 2‘;;
it : thm = |- (\x. x + 1) 2 = 2 + 1
There are also some conversions special to particular theories. For example there
is a conversion NUM RED CONV to evaluate the result of an arithmetic operation on
two numerals:
#NUM_RED_CONV ‘2 * 2‘;;
it : thm = |- 2 * 2 = 4
#NUM_RED_CONV ‘2 EXP 10‘;;
it : thm = |- 2 EXP 10 = 1024
#NUM_RED_CONV ‘100 DIV 7‘;;
it : thm = |- 100 DIV 7 = 14
8.1 Conversionals
These conversions are building blocks. The mechanism for building them up is
a suite of higher order functions called ‘conversionals’ or ‘conversion combining
67