Dear Manuel, 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. Cheers, René > Am 05.02.2019 um 09:52 schrieb Manuel Eberl <ebe...@in.tum.de>: > > Hello, > > 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? > > Manuel > _______________________________________________ > 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