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

Otherwise we would define »inf« with »THE x. …«, and this means that for
particular instances of lattices (sets, nats, …) you have to derive
type-specific primitive rules (e.g. inf on 0/Suc representation, inf on
{}/insert representation) manually starting with a »THE x. …«
definition.  In practice, it is much more straightforward to define inf
on particular types directly and then prove that this instance conforms
to its axiomatic specification.  As a side effect, you get reasonable
code equations, something which can hardly be achieved if inf would be a
generic polymorphic operation rather than a class parameter.

Of course, these constructive type classes are more specific than the
mathematical concept they represent, but for meta-theory a
record/locale-based approach with explicit carrier sets as in
HOL-Algebra is much more feasible anyway.  But see also the funny lemma
http://isabelle.in.tum.de/repos/isabelle/file/7270ae921cf2/src/HOL/Lattices.thy#l447
which shows how even the contructive type classes are able to talk about
uniqueness.

Hope this helps,
	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/20110708/67c558a1/attachment.sig>