[isabelle-dev] Theory for discrete log etc.
Rene.Thiemann at uibk.ac.at
Tue Nov 22 16:08:36 CET 2016
thanks Manuel and Florian for pointing to other variants of discrete logarithms.
I would like to mention a fairly recent one in
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.)
> Am 13.08.2016 um 17:02 schrieb Manuel Eberl <eberlm at 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.
> 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.
>> isabelle-dev mailing list
>> isabelle-dev at in.tum.de
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
More information about the isabelle-dev