[isabelle-dev] Exponentiation by squaring

[Manuel Eberl]

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