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
