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

[Tjark Weber]

On Fri, 2011-01-21 at 07:27 -0800, Brian Huffman wrote:
> On Fri, Jan 21, 2011 at 7:03 AM, Tjark Weber <webertj at in.tum.de> wrote:
> > 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.

Of course.  (What I had in mind was more along the lines of 'a::A,
'b::B, but your example is even nicer.)

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

Well, to enable what the class tutorial calls "abstract reasoning," that
is, transfer of theorems to interpretations and sublocales.

Kind regards,
Tjark