*To*: Manuel Eberl <eberlm at in.tum.de>, "cl-isabelle-users at lists.cam.ac.uk" <cl-isabelle-users at lists.cam.ac.uk>*Subject*: Re: [isabelle] Code equations for "power"*From*: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>*Date*: Fri, 8 Jan 2016 17:17:25 +0100*In-reply-to*: <568FCF40.30901@in.tum.de>*References*: <568FCF40.30901@in.tum.de>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:38.0) Gecko/20100101 Thunderbird/38.3.0

Dear Manuel,

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.

definition map_power :: "'a :: power list => 'a list" where "map_power = map power" then if you use map_power, you will end up with the original slow implementation.

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?

class power_impl = power + fixes power_impl :: "'a => nat => 'a" assumes power_impl: "power = power_impl" declare power_impl [code]

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.

Best, Andreas

**Follow-Ups**:**Re: [isabelle] Code equations for "power"***From:*Manuel Eberl

**Re: [isabelle] Code equations for "power"***From:*Thiemann, Rene

**References**:**[isabelle] Code equations for "power"***From:*Manuel Eberl

- Previous by Date: Re: [isabelle] Isabelle2016-RC0 - default output buffers
- Next by Date: Re: [isabelle] Isabelle2016-RC0: Windows bootstrapping
- Previous by Thread: [isabelle] Code equations for "power"
- Next by Thread: Re: [isabelle] Code equations for "power"
- Cl-isabelle-users January 2016 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list