>> I wrote to Florian about this exact issue back in February 2010. >> Florian's recommended solution at the time was to add a new subclass >> of archimedean_field that fixes the floor function and assumes a >> correctness property about it. This solution is really easy to >> implement (see attached diff). If people think this is a reasonable >> design, then I'll let someone else go ahead and test and commit the >> patch.
> I want to add important context for that recommendation: a few years
> ago, around 2006, when I entered this type class adventure in more deep,
> I came to the conclusion that it is usually better to have
> »constructive« type classes, e.g. if we specify a semilattice as type
> class, we don't assume »there exists a inf such that …« but we add an
> explicit parameter »inf« which a corresponding set of properties.
Another addition: it would also be possible to turn floor and ceiling to
parameters of archimedean_field, similar to complete_lattice which also
includes bot and top, although both could be defined as derived operations.
Florian
--
Home:
http://www.in.tum.de/~haftmann
PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
