[isabelle-dev] Evaluation of floor and ceiling

[Florian Haftmann]

>> 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



-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 262 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20110710/7567a3fe/attachment.sig>