Dear all, thanks Manuel and Florian for pointing to other variants of discrete logarithms.
I would like to mention a fairly recent one in AFP/Sqrt_Babylonian/Log_Impl.thy. It defines log_floor and log_ceiling :: “int => int => nat”. The advantage of these functions are improved code equations which work like repeated squaring for exponentiation algorithms. The efficiency has been crucial when computing logarithms of numbers x with more than 100,000 digits, i.e., where log2 x >= 300,000. (These numbers arose during the factorization of large integer polynomials.) Cheers, René > Am 13.08.2016 um 17:02 schrieb Manuel Eberl <ebe...@in.tum.de>: > > There's also natlog2 in src/HOL/Analysis/Summation_Tests.thy, which I > introduced because I didn't know about the other ones. > > Manuel > > > On 13/08/16 15:09, Florian Haftmann wrote: >> Hi all, >> >> after studying 28d1deca302e I realized that we have now two theories >> dealing with discrete functions (with one having been hidden in >> Float.thy for years): >> >> Log_Nat.floorlog :: "nat ⇒ nat ⇒ nat" >> Discrete.log :: "nat ⇒ nat" >> Log_Nat.bitlen :: "int ⇒ int" >> Discrete.sqrt :: "nat ⇒ nat" >> >> »Discrete.log« seems to be »Log_Nat.floorlog 2« and »Log_Nat.bitlen« is >> just a variant with different types. >> >> Just to place a memo for future consolidation. >> >> Cheers, >> Florian >> >> >> >> _______________________________________________ >> isabelle-dev mailing list >> isabelle-...@in.tum.de >> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev >> > _______________________________________________ > isabelle-dev mailing list > isabelle-...@in.tum.de > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev