[isabelle-dev] Sort Annotation vs. Class Context for Lemmas

[Brian Huffman]

On Fri, Jan 21, 2011 at 7:03 AM, Tjark Weber <webertj at in.tum.de> wrote:
> On Fri, 2011-01-21 at 15:27 +0100, Tobias Nipkow wrote:
>> One issue can be that if some sort involves multiple type classes, the
>> corresponding class may not have been defined. That is the one advantage
>> of sorts: you can create conjunctions/intersection of type classes on
>> the fly.
>
> If there is just one intersection of type classes, one should perhaps
> consider defining the corresponding class (before stating the lemma in
> its context).  The alternative is that the poor user who later feels
> that this class would be really useful has to re-prove every lemma.
>
> Of course, this doesn't work for lemmas that involve separate sorts.

I'm not sure if this is what you have in mind, but in HOLCF there is a
continuity predicate

cont :: ('a::cpo => 'b::cpo) => bool

which of course is impossible to define or reason about within the
context of any single class (unless you do some weird mixing of
locale- and class-based reasoning). The same goes for the "mono"
predicate in the main HOL libraries. So it is clear that locale
contexts are quite restrictive compared to stating lemmas with type
class constraints.

But anyway, let me step back a bit and ask a higher-level question:
Why do you need to prove lemmas *in* the context of a class at all?

Unless you are planning on doing locale interpretations of
class-locales (which are often a poor fit for where they are used;
search for "%m n::nat. m dvd n & ~ n dvd m" in GCD.thy for some
examples) I don't see any advantage to proving class-specific lemmas
inside the locale context.

- Brian