[isabelle-dev] Proposing extensions to the Isabelle library?

[Tobias Nipkow]

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.

Tobias

> Thanks!
> 
> 
> 
> On 12/13/12 4:24 AM, Tobias Nipkow wrote:
>> Am 13/12/2012 03:21, schrieb Alessandro Coglio:
>>> Hello,
>>>
>>> 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.
>>
>> Thanks
>> Tobias
>>
>>> Thank you in advance!
>>>
>>>
>>>
>>> _______________________________________________
>>> isabelle-dev mailing list
>>> isabelle-dev at in.tum.de
>>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>>>
>> _______________________________________________
>> isabelle-dev mailing list
>> isabelle-dev at in.tum.de
>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>