[isabelle-dev] Evaluation of floor and ceiling

[Lukas Bulwahn]

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
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20110710/b027b6ef/attachment-0002.html>