# Re: [isabelle] the state of the lattice theories

Florian,
On 29/07/2011, at 3:58 PM, Florian Haftmann wrote:
> first of all, HOL-Lattice is more an example than a library. I would
> guess that the lattice in HOL-Algebra is what you want to start an.
OK. This being the case, could (/should) it be moved from the top-level, to e.g. HOL/Library/ or ex/, or maybe Proofs/?
On a related note, HOL/Library/ is a zoo. Would it be reasonable to introduce more structure there, ala Haskell's hierarchical libraries? How about the stuff in the top-level HOL/ directory?
> The order development in HOLCF is traditionally something specific apart.
Indeed it was an entirely separate Isabelle logic (built on top of HOL), but Brian's recent work has made HOLCF a HOL library. It provides convenient ways of making recursive definitions over PCPOs that strike me as useful for doing the same thing over complete lattices.
>> Has there been enough exploration of this design space such that the one true order and lattice theory is waiting to spring forth?
>
> Well, there *has* been a lots of effort to reduce the number of lattice
> developments to effectively two. For the background, I quote here from
> an e-mail from isabelle-dev:
>
> <...>
Thanks for that. I am using the lattice theory in HOL/ (Complete_Lattice and friends) which is quite pleasant.
cheers
peter
--
http://peteg.org/

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*