Re: [isabelle] Code equations for "power"
On 08/01/16 17:26, Manuel Eberl wrote:
I think that this can work for power, but it can also lead to surprises because the
rewrite does not trigger always and users then have to understand the whole setup to find
out. I had experimented with such rewrites for subset tests (end of theory
Library/Cardinality), but this never worked as well as I had hoped, because the rewrite
needed the sort card_UNIV, which was hardly present in any code equation.
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
I guess that's a pretty good compromise, isn't it? Most of the time, exported code using
the "power" operation will probably be dealing with types that fulfil at least
monoid_mult, and then this fast variant could be used.
RenÃ Thiemann and Christian Sternagel faced the same problem for linorders and
comparators. They have implemented a custom function in ML that transforms the code
equations, but users have to call this manually (see their ITP2015 paper). This approach
is less convenient, but more robust.
This archive was generated by a fusion of
Pipermail (Mailman edition) and