[isabelle-dev] binary arithmetic optimization
lp15 at cam.ac.uk
Tue Feb 12 17:02:46 CET 2008
Certainly an interesting idea. HOL4 also uses separate constants.
Thanks for trying this out!
I don't know who is going to fix code generation though...
On 12 Feb 2008, at 02:21, Brian Huffman wrote:
> 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
> Isabelle-dev mailing list
> Isabelle-dev at mailbroy.informatik.tu-muenchen.de
More information about the isabelle-dev