# [isabelle-dev] binary arithmetic optimization

Brian Huffman brianh at cs.pdx.edu
Tue Feb 12 03:21:21 CET 2008

```Hello all,

Recently I tested a variation of HOL/ex/Binary.thy: Instead of using a
function "bit :: nat => bool => nat", I replaced this with a pair of
functions, "bit0 :: nat => nat" and "bit1 :: nat => nat" which are
equal to "bit False" and "bit True", respectively. (The modified
theory file is attached.)

When proving the example lemmas with global timing enabled, I measured
a speed-up of about 30-40% on my machine.

I propose that a similar modification be done for the numerals in
Isabelle/HOL. We could replace "Bit :: int => bit => int" with
constants "Bit0 :: int => int" and "Bit1 :: int => int". This would
also make the "bit" datatype unnecessary.

Today I modified a copy of Isabelle/HOL in this way; everything seems
to work just fine, and binary arithmetic works faster. However, code
generation will need a bit more work, and the HOL/Word library will
need some non-trivial modifications.

- Brian

-------------- next part --------------
(*  Title:      HOL/ex/Binary.thy
ID:         \$Id: Binary.thy,v 1.9 2007/09/18 14:08:04 wenzelm Exp \$
Author:     Makarius
*)

header {* Simple and efficient binary numerals *}

theory Binary
imports Main
begin

subsection {* Binary representation of natural numbers *}

definition
bit0 :: "nat \<Rightarrow> nat" where
"bit0 n = n + n"

definition
bit1 :: "nat \<Rightarrow> nat" where
"bit1 n = Suc (n + n)"

lemmas bit_def = bit0_def bit1_def
lemmas bit_simps = bit_def

ML {*
structure Binary =
struct
fun dest_binary (Const (@{const_name HOL.zero}, Type ("nat", _))) = 0
| dest_binary (Const (@{const_name HOL.one}, Type ("nat", _))) = 1
| dest_binary (Const ("Binary.bit0", _) \$ bs) = 2 * dest_binary bs
| dest_binary (Const ("Binary.bit1", _) \$ bs) = 2 * dest_binary bs + 1
| dest_binary t = raise TERM ("dest_binary", [t]);

fun mk_bit 0 = @{term bit0}
| mk_bit 1 = @{term bit1}
| mk_bit _ = raise TERM ("mk_bit", []);

fun mk_binary 0 = @{term "0::nat"}
| mk_binary 1 = @{term "1::nat"}
| mk_binary n =
if n < 0 then raise TERM ("mk_binary", [])
else
let val (q, r) = Integer.div_mod n 2
in mk_bit r \$ mk_binary q end;
end
*}

subsection {* Direct operations -- plain normalization *}

lemma binary_norm:
"bit0 0 = 0"
"bit1 0 = 1"
unfolding bit_def by simp_all

"n + 0 = n"
"0 + n = n"
"1 + 1 = bit0 1"
"bit0 n + 1 = bit1 n"
"bit1 n + 1 = bit0 (n + 1)"
"1 + bit0 n = bit1 n"
"1 + bit1 n = bit0 (n + 1)"
"bit0 m + bit0 n = bit0 (m + n)"
"bit0 m + bit1 n = bit1 (m + n)"
"bit1 m + bit0 n = bit1 (m + n)"
"bit1 m + bit1 n = bit0 ((m + n) + 1)"

lemma binary_mult:
"n * 0 = 0"
"0 * n = 0"
"n * 1 = n"
"1 * n = n"
"bit1 m * n = bit0 (m * n) + n"
"bit0 m * n = bit0 (m * n)"
"n * bit1 m = bit0 (m * n) + n"
"n * bit0 m = bit0 (m * n)"

lemmas binary_simps = binary_norm binary_add binary_mult

subsection {* Indirect operations -- ML will produce witnesses *}

lemma binary_less_eq:
fixes n :: nat
shows "n \<equiv> m + k \<Longrightarrow> (m \<le> n) \<equiv> True"
and "m \<equiv> n + k + 1 \<Longrightarrow> (m \<le> n) \<equiv> False"
by simp_all

lemma binary_less:
fixes n :: nat
shows "m \<equiv> n + k \<Longrightarrow> (m < n) \<equiv> False"
and "n \<equiv> m + k + 1 \<Longrightarrow> (m < n) \<equiv> True"
by simp_all

lemma binary_diff:
fixes n :: nat
shows "m \<equiv> n + k \<Longrightarrow> m - n \<equiv> k"
and "n \<equiv> m + k \<Longrightarrow> m - n \<equiv> 0"
by simp_all

lemma binary_divmod:
fixes n :: nat
assumes "m \<equiv> n * k + l" and "0 < n" and "l < n"
shows "m div n \<equiv> k"
and "m mod n \<equiv> l"
proof -
from `m \<equiv> n * k + l` have "m = l + k * n" by simp
with `0 < n` and `l < n` show "m div n \<equiv> k" and "m mod n \<equiv> l" by simp_all
qed

ML {*
local
infix ==;
val op == = Logic.mk_equals;
fun plus m n = @{term "plus :: nat \<Rightarrow> nat \<Rightarrow> nat"} \$ m \$ n;
fun mult m n = @{term "times :: nat \<Rightarrow> nat \<Rightarrow> nat"} \$ m \$ n;

val binary_ss = HOL_basic_ss addsimps @{thms binary_simps};
fun prove ctxt prop =
Goal.prove ctxt [] [] prop (fn _ => ALLGOALS (full_simp_tac binary_ss));

fun binary_proc proc ss ct =
(case Thm.term_of ct of
_ \$ t \$ u =>
(case try (pairself (`Binary.dest_binary)) (t, u) of
SOME args => proc (Simplifier.the_context ss) args
| NONE => NONE)
| _ => NONE);
in

val less_eq_proc = binary_proc (fn ctxt => fn ((m, t), (n, u)) =>
let val k = n - m in
if k >= 0 then
SOME (@{thm binary_less_eq(1)} OF [prove ctxt (u == plus t (Binary.mk_binary k))])
else
SOME (@{thm binary_less_eq(2)} OF
[prove ctxt (t == plus (plus u (Binary.mk_binary (~ k - 1))) (Binary.mk_binary 1))])
end);

val less_proc = binary_proc (fn ctxt => fn ((m, t), (n, u)) =>
let val k = m - n in
if k >= 0 then
SOME (@{thm binary_less(1)} OF [prove ctxt (t == plus u (Binary.mk_binary k))])
else
SOME (@{thm binary_less(2)} OF
[prove ctxt (u == plus (plus t (Binary.mk_binary (~ k - 1))) (Binary.mk_binary 1))])
end);

val diff_proc = binary_proc (fn ctxt => fn ((m, t), (n, u)) =>
let val k = m - n in
if k >= 0 then
SOME (@{thm binary_diff(1)} OF [prove ctxt (t == plus u (Binary.mk_binary k))])
else
SOME (@{thm binary_diff(2)} OF [prove ctxt (u == plus t (Binary.mk_binary (~ k)))])
end);

fun divmod_proc rule = binary_proc (fn ctxt => fn ((m, t), (n, u)) =>
if n = 0 then NONE
else
let val (k, l) = Integer.div_mod m n
in SOME (rule OF [prove ctxt (t == plus (mult u (Binary.mk_binary k)) (Binary.mk_binary l))]) end);

end;
*}

simproc_setup binary_nat_less_eq ("m <= (n::nat)") = {* K less_eq_proc *}
simproc_setup binary_nat_less ("m < (n::nat)") = {* K less_proc *}
simproc_setup binary_nat_diff ("m - (n::nat)") = {* K diff_proc *}
simproc_setup binary_nat_div ("m div (n::nat)") = {* K (divmod_proc @{thm binary_divmod(1)}) *}
simproc_setup binary_nat_mod ("m mod (n::nat)") = {* K (divmod_proc @{thm binary_divmod(2)}) *}

method_setup binary_simp = {*
Method.no_args (Method.SIMPLE_METHOD'
(full_simp_tac
(HOL_basic_ss
[@{simproc binary_nat_less_eq},
@{simproc binary_nat_less},
@{simproc binary_nat_diff},
@{simproc binary_nat_div},
@{simproc binary_nat_mod}])))
*} "binary simplification"

subsection {* Concrete syntax *}

syntax
"_Binary" :: "num_const \<Rightarrow> 'a"    ("\$_")

parse_translation {*
let

val syntax_consts = map_aterms (fn Const (c, T) => Const (Syntax.constN ^ c, T) | a => a);

fun binary_tr [Const (num, _)] =
let
val _ = z = 0 andalso n >= 0 orelse error ("Bad binary number: " ^ num);
in syntax_consts (Binary.mk_binary n) end
| binary_tr ts = raise TERM ("binary_tr", ts);

in [("_Binary", binary_tr)] end
*}

subsection {* Examples *}

lemma "\$6 = 6"

lemma "bit1 (bit0 (bit0 0)) = 1"

lemma "bit1 (bit0 (bit0 0)) = bit1 0"

lemma "\$5 + \$3 = \$8"
by binary_simp

lemma "\$5 * \$3 = \$15"
by binary_simp

lemma "\$5 - \$3 = \$2"
by binary_simp

lemma "\$3 - \$5 = 0"
by binary_simp

lemma "\$123456789 - \$123 = \$123456666"
by binary_simp

lemma "\$1111111111222222222233333333334444444444 - \$998877665544332211 =
\$1111111111222222222232334455668900112233"
by binary_simp

lemma "(1111111111222222222233333333334444444444::nat) - 998877665544332211 =
1111111111222222222232334455668900112233"
by simp

lemma "(1111111111222222222233333333334444444444::int) - 998877665544332211 =
1111111111222222222232334455668900112233"
by simp

lemma "\$1111111111222222222233333333334444444444 * \$998877665544332211 =
\$1109864072938022197293802219729380221972383090160869185684"
by binary_simp

lemma "\$1111111111222222222233333333334444444444 * \$998877665544332211 -
\$5555555555666666666677777777778888888888 =
\$1109864072938022191738246664062713555294605312381980296796"
by binary_simp

lemma "\$42 < \$4 = False"
by binary_simp

lemma "\$4 < \$42 = True"
by binary_simp

lemma "\$42 <= \$4 = False"
by binary_simp

lemma "\$4 <= \$42 = True"
by binary_simp

lemma "\$1111111111222222222233333333334444444444 < \$998877665544332211 = False"
by binary_simp

lemma "\$998877665544332211 < \$1111111111222222222233333333334444444444 = True"
by binary_simp

lemma "\$1111111111222222222233333333334444444444 <= \$998877665544332211 = False"
by binary_simp

lemma "\$998877665544332211 <= \$1111111111222222222233333333334444444444 = True"
by binary_simp

lemma "\$1234 div \$23 = \$53"
by binary_simp

lemma "\$1234 mod \$23 = \$15"
by binary_simp

lemma "\$1111111111222222222233333333334444444444 div \$998877665544332211 =
\$1112359550673033707875"
by binary_simp

lemma "\$1111111111222222222233333333334444444444 mod \$998877665544332211 =
\$42245174317582819"
by binary_simp

lemma "(1111111111222222222233333333334444444444::int) div 998877665544332211 =
1112359550673033707875"
by simp  -- {* legacy numerals: 30 times slower *}

lemma "(1111111111222222222233333333334444444444::int) mod 998877665544332211 =
42245174317582819"
by simp  -- {* legacy numerals: 30 times slower *}

end
```