On 07/10/2011 08:44 AM, Florian Haftmann wrote:
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
I reached my goal of enabling execution of floor and ceiling with the
provided changesets and am satisfied about its current state. If anyone
wants to modify it, he can go ahead -- but I won't spend any time on
that issue anymore.
Lukas
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
