<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN">
<html>
<head>
<meta content="text/html; charset=windows-1252"
http-equiv="Content-Type">
<title></title>
</head>
<body text="#000000" bgcolor="#ffffff">
On 07/10/2011 08:44 AM, Florian Haftmann wrote:
<blockquote cite="mid:4E194A30.9050705@informatik.tu-muenchen.de"
type="cite">
<blockquote type="cite">
<blockquote type="cite">
<pre wrap="">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.
</pre>
</blockquote>
</blockquote>
<pre wrap="">
</pre>
<blockquote type="cite">
<pre wrap="">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.
</pre>
</blockquote>
<pre wrap="">
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
</pre>
</blockquote>
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.<br>
<br>
<br>
Lukas<br>
<br>
<blockquote cite="mid:4E194A30.9050705@informatik.tu-muenchen.de"
type="cite">
<pre wrap=""></pre>
<pre wrap="">
<fieldset class="mimeAttachmentHeader"></fieldset>
_______________________________________________
isabelle-dev mailing list
<a class="moz-txt-link-abbreviated" href="mailto:isabelle-dev@in.tum.de">isabelle-dev@in.tum.de</a>
<a class="moz-txt-link-freetext" href="https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev">https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev</a>
</pre>
</blockquote>
<br>
</body>
</html>