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
