On Fri, 2011-01-21 at 07:27 -0800, Brian Huffman wrote: > On Fri, Jan 21, 2011 at 7:03 AM, Tjark Weber <[email protected]> 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 _______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
