[isabelle-dev] binary arithmetic optimization

[Lawrence Paulson]

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...

Larry

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
>
>
> <Binary.thy>_______________________________________________
> Isabelle-dev mailing list
> Isabelle-dev at mailbroy.informatik.tu-muenchen.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev