[isabelle] Code equations for "power"


I just noticed that the "power" function is exported as

power :: forall a. (Power a) => a -> Nat -> a;
power a n =
  (if equal_nat n zero_nat then one
    else times a (power a (minus_nat n one_nat)));

This looks pretty inefficient to me; something like iterated squaring should be much faster, and it's pretty easy to do. However, this only works in the type class mult_monoid; power, on the other hand, is defined in the type class "power". (the difference is essentially that the latter does not demand associativity, if I am not mistaken)

Is it still possible to use the more efficient iterative squaring when applicable? I attached something using code_unfold, but I'm not sure if that really does what one would want it to do.

Moreover, for rational numbers, one could optimise this even futher: multiplication on rational numbers reduces the numerator and denominator after the multiplication. In the case of "power", this is unnecessary, since the numerator and denominator of the result will always be coprime if they were coprime before. Perhaps this would be a worthwhile optimisation?

Lastly, I was wondering whether there was something like "divmod" in Isabelle, i.e. an operation that returns both the quotient and the remainder, since most languages have a corresponding operation that is more efficient than computing the two separately.



Attachment: MyPower.thy
Description: application/extension-thy

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.