Re: [isabelle] the state of the lattice theories


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.



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