Re: [isabelle-dev] Efficient code for Discrete.log

2017-06-30 Thread Manuel Eberl
Thanks for the hint! I'll try to use that then. However, the main goal was to use PolyML's native log2 function anyway, which is likely much faster than anything we can implement in Isabelle. Manuel On 2017-06-29 20:12, Thiemann, Rene wrote: > Hi Manual, > > thanks for your efforts, but I

Re: [isabelle-dev] Efficient code for Discrete.log

2017-06-29 Thread Thiemann, Rene
Hi Manual, thanks for your efforts, but I believe there is already a more efficient way to compute log2. In your implementation, consider your intlog2_aux which roughly requires y iterations if log2(x) = y, since you always just add 1 to the accumulator. For some of my applications this

Re: [isabelle-dev] Efficient code for Discrete.log

2017-06-29 Thread Andreas Lochbihler
Hi Manuel, You are not the first to encouter this problem. Here's my experience: In 4b1b85f38944, I added code_printings for gcd and decided to add Gcd to the imports of Code_Target_Nat. IIRC this broke a few things in the AFP, which I had to fix. Meanwhile, Gcd has become part of Main again.