Filter
Top Products
8.2. DEPTH CONVERSIONS 69
#DEPTH_CONV BETA_CONV ‘(\f x. f x) (\y. y + 1)‘;;
it : thm = |- (\f x. f x) (\y. y + 1) = (\x. (\y. y + 1) x)
#REDEPTH_CONV BETA_CONV ‘(\f x. f x) (\y. y + 1)‘;;
it : thm = |- (\f x. f x) (\y. y + 1) = (\x. x + 1)
#TOP_DEPTH_CONV BETA_CONV ‘(\f x. f x) (\y. y + 1)‘;;
it : thm = |- (\f x. f x) (\y. y + 1) = (\x. x + 1)
#TOP_DEPTH_CONV NUM_RED_CONV ‘7 * (3 EXP 10) + 11‘;;
it : thm = |- 7 * 3 EXP 10 + 11 = 413354
The difference is that the main sweeps are respectively top-down and bottom-up,
which can lead to one or the other being preferable, mainly for efficiency reasons,
in some situations. TOP DEPTH CONV is the default for HOL’s rewriting, described
in a later chapter.
The conversionals all have fairly straightforward definitions using HOL’s primi-
tive and derived equality rules. For example, THENC just needs to apply the conver-
sion to a term, getting a theorem, then take the right-hand side of this theorem’s
conclusion, apply the second conversion to that and then link the equations together
using the primitive inference rule TRANS. One could write an equivalent function as:
#let THENC’ conv1 conv2 t =
let th1 = conv1 t in
let th2 = conv2 (rand(concl th1)) in
TRANS th1 th2;;
THENC’ : (’a -> thm) -> (term -> thm) -> ’a -> thm = <fun>
The depth conversionals can be implemented by a recursive traversal of the term,
using primitive rules like MK COMB to lift the equational theorems up to the whole
term. In fact, the implementations are a bit more sophisticated because they are
careful to avoid creating trivial equations unless needed.