Re: [isabelle] code generation for saturated naturals



On Wed, Sep 7, 2011 at 11:32 PM, Florian Haftmann
<florian.haftmann at informatik.tu-muenchen.de> wrote:
> instantiation sat :: (len) complete_distrib_lattice
>
> which is still left as an exercise to prove.

I haven't added this instance proof yet, but I did add another one:
Type 'a sat is now an instance of the number_semiring class. Proving
this instance involved showing that the function "Sat :: nat => 'a
sat" is identical to the polymorphic function "of_nat" at the same
type.

This brings up another issue: It is generally undesirable to have two
different copies of the same function around if they are both in
common use, since this means that we would have to maintain two
similar-looking but separate sets of simp rules. This was the
motivation for making "int :: nat => int" into an abbreviation for
"of_nat :: nat => int" a few years ago; it let us remove a lot of
duplication and simpset inconsistencies from the standard library.

So here's what I propose for the saturated arithmetic library: Rename
the current constant "Sat :: nat => 'a sat" to something like
Abs_sat', and reintroduce the user-friendly name "Sat" as a
type-constrained abbreviation for "of_nat".

The only reason I'm hesitant to make this change myself is that I
don't know how it might affect code generation -- currently "Sat" has
some special status because it appears in the [code abstype]
declaration.

- Brian





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