[isabelle-dev] Sort Annotation vs. Class Context for Lemmas
Hi, I noticed that numerous lemmas in HOL that refer to class constants are stated at the top level (using implicit or explicit sort annotations), rather than in the corresponding class context (see, for instance, Compl_lessThan in HOL/SetInterval.thy). If I am not mistaken, this means the corresponding lemma is not available in the context of the class, which seems unfortunate. Is this merely a legacy issue, or are there genuine reasons for stating these lemmas with sort annotations? Kind regards, Tjark ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Sort Annotation vs. Class Context for Lemmas
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. Tobias Tjark Weber schrieb: Hi, I noticed that numerous lemmas in HOL that refer to class constants are stated at the top level (using implicit or explicit sort annotations), rather than in the corresponding class context (see, for instance, Compl_lessThan in HOL/SetInterval.thy). If I am not mistaken, this means the corresponding lemma is not available in the context of the class, which seems unfortunate. Is this merely a legacy issue, or are there genuine reasons for stating these lemmas with sort annotations? Kind regards, Tjark ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Sort Annotation vs. Class Context for Lemmas
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. Kind regards, Tjark ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Sort Annotation vs. Class Context for Lemmas
On Fri, Jan 21, 2011 at 7:03 AM, Tjark Weber webe...@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
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Sort Annotation vs. Class Context for Lemmas
On Fri, 2011-01-21 at 07:27 -0800, Brian Huffman wrote:
On Fri, Jan 21, 2011 at 7:03 AM, Tjark Weber webe...@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
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
