Filter
Top Products
12.3. LISTS 95
But many of them have an almost equally direct strategy in terms of our binary
notation.
1
For example the following theorems, easily proved, can be used directly
as rewrite rules to perform arithmetic evaluation.
|- (!n. SUC (NUMERAL n) = NUMERAL (SUC n)) /\
(SUC _0 = BIT1 _0) /\
(!n. SUC (BIT0 n) = BIT1 n) /\
(!n. SUC (BIT1 n) = BIT0 (SUC n))
or
|- (!m n. (NUMERAL m = NUMERAL n) = (m = n)) /\
((_0 = _0) = T) /\
(!n. (BIT0 n = _0) = (n = _0)) /\
(!n. (BIT1 n = _0) = F) /\
(!n. (_0 = BIT0 n) = (_0 = n)) /\
(!n. (_0 = BIT1 n) = F) /\
(!m n. (BIT0 m = BIT0 n) = (m = n)) /\
(!m n. (BIT0 m = BIT1 n) = F) /\
(!m n. (BIT1 m = BIT0 n) = F) /\
(!m n. (BIT1 m = BIT1 n) = (m = n))
Most arithmetic operations can be implemented as a set of rewrite rules like
the above, and applied using the standard rewriting mechanism. A suite of such
rewrites is collected together into a single rewrite rule ARITH that will evaluate most
ground expressions using just the standard rewriting mechanism. For example:
#let conv = PURE_REWRITE_CONV[ARITH];;
conv : conv = <fun>
#conv ‘12345 * 12345‘;;
it : thm = |- 12345 * 12345 = 152399025
However, a few operations are hard to evaluate efficiently with the standard
rewriting mechanism; even ARITH_SUB is a bit inefficient, since the same condition
is tested repeatedly. Therefore we also provide a full suite of conversions, and collect
them together as NUM RED CONV and NUM REDUCE CONV.
12.3 Lists
A HOL recursive type of lists is defined, and various standard list combinators
defined by recursion. These often have the same names as their CAML counterparts,
but in upper case.
HD = |- HD (CONS h t) = h
TL = |- TL (CONS h t) = t
APPEND =
|- (!l. APPEND [] l = l) /\
(!h t l. APPEND (CONS h t) l = CONS h (APPEND t l))
1
Another nice example, though we don’t actually implement it, is the GCD function. Knuth
(1969) gives a simple algorithm based on gcd(2m,2n) = 2gcd(m, n), gcd(2m + 1,2n) = gcd(2m +
1,n) and gcd(2m+1,2n+1) = gcd(m−n, 2n+1). This outperforms Euclid’s method on machines
where bitwise operations are relatively efficient; our in-logic implementation would surely exhibit
the same characteristics even if our ‘bits’ are rather large!