Re: [isabelle] Code equations for "power"
mult_monoid assumes associativity of and neutrality of 1 for times. power does not impose
any constraints; it is a superclass of mult_monoid.
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
The code_unfold works if the call to power in the code equations is types with something
of sort mult_monoid. So if the code equation uses power on one of the standard numeric
types, everything is fine. But if you use power polymorphically for some 'a, then this
does not work if mult_monoid is not a supersort of 'a's sort. For example, if you have
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.
Custom implementations for power are not possible with the current setup. You can have
type-dependent implementations for a function only if that function is a type class
parameter (unless you play some sophisticated tricks like in the Containers AFP entry).
From what I can see, it does not seem reasonable to make power a type class parameter,
because then power cannot be a superclass of mult_monoid any more (you'd have to add power
as a type class parameter to the whole algebraic type class hierarchy). But you could
achieve something similar like this:
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
class power_impl = power +
fixes power_impl :: "'a => nat => 'a"
assumes power_impl: "power = power_impl"
declare power_impl [code]
Then, of course, you have to instantiate the new class power_impl for all types that
instantiate power and all users have to do the same for their own types. Unfortunately, we
do not (yet) have a mechanism to instantiate such definitional type classes automatically.
With this approach, you could declare custom code equations for instances like rat.
There are various specialised divmod constants in HOL, e.g., divmod_integer,
semiring_numeral_div_class.divmod and Divides.divmod_nat, but no systematic, algebraic
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and