[isabelle-dev] Proposing extensions to the Isabelle library?
nipkow at in.tum.de
Fri Dec 14 13:14:20 CET 2012
Am 13/12/2012 18:01, schrieb Alessandro Coglio:
> Hi Tobias, thank you for your answer.
> My LibExt also contained some type classes and theorems for finite lattices and
> finite linear orders, including a proof that finite lattices are complete (using
> the approach with type classes suggested by Florian Haftmann on isabelle-users
> some time ago). Do you have any comment on those?
> Sorry for missing Library/Product_Lattice. I suppose it makes sense that it is
> not part of Main, since one may want pair-wise or lexicographic ordering,
> depending on the application.
> I've attached a new LibExt without what's already in Product_Lattice.
Thanks for that, I'll integrate it with the library.
> I was wondering why Library/Product_Lattice proves prod :: (ord, ord) ord but
> not prod :: (inf, inf) inf (and same for sup, Inf, and Sup).
> On a semi-related topic, I was wondering why the Isabelle library has syntactic
> type classes for many (most?) operators but not for bot and top.
Florian can answer that one better than me.
> On 12/13/12 4:24 AM, Tobias Nipkow wrote:
>> Am 13/12/2012 03:21, schrieb Alessandro Coglio:
>>> Is there a process to propose extensions to the Isabelle library? Is
>>> isabelle-dev the right place, as opposed to isabelle-users?
>>> As part of an Isabelle project, I've developed some type classes and theorems
>>> for orders and lattices (see attached file) that could be of general use.
>> I looked at your theory, which deals with orderings on product types, and
>> noticed a few things:
>> 1. We already have Library/Product_ord, but it defines a *lexicographic*
>> ordering. Any objections if we rename it to Lex_Product_ord?
>> 2. We also have a Library/Product_lattice. It covers much the same ground as
>> your LibExt. I would not want to add another similar theory, but if you have any
>> additional results not contained in Product_lattice already, please filter them
>> out and I can add them.
>>> Thank you in advance!
>>> isabelle-dev mailing list
>>> isabelle-dev at in.tum.de
>> isabelle-dev mailing list
>> isabelle-dev at in.tum.de
More information about the isabelle-dev