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
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 on
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"