[isabelle-dev] Exponentiation by squaring
Rene.Thiemann at uibk.ac.at
Tue Feb 5 10:05:45 CET 2019
in the AFP there is Subresultants/Binary_Exponentiation.thy. Perhaps your changes make this theory obsolete.
The Binary_Exponentiation algorithm is then later on used in Berlekamp-Zassenhaus in modular arithmetic to compute inverses in prime-fields.
> Am 05.02.2019 um 09:52 schrieb Manuel Eberl <eberlm at in.tum.de>:
> If I'm not mistaken, the default code setup for the "power" operation in
> HOL is linear in the exponent (it just does multiplication n times). I
> didn't find anything on faster exponentiation in the distribution or the
> AFP. so in 154cf64e403e, I committed some material about exponentiation
> by squaring that works in logarithmic time in the exponent for monoid_mult.
> I wonder if this should be a code_unfold or code_abbrev rule for
> monoid_mult in general, or perhaps just for some instances like nat and int.
> There's also setup in HOL-Number_Theory to do modular exponentiation "a
> ^ n mod m" and congruences of the form "[a ^ n = b] (mod m)" using this,
> at least for int and nat. I'm not sure if the rules I set up are the
> best ones and, again, this could be generalised to
> euclidean_semiring_cancel but I'm not sure if I should.
> Does anyone have any stakes in/opinions on this?
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
More information about the isabelle-dev