[isabelle-dev] Theory for discrete log etc.

[Thiemann, Rene]

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