[isabelle] the state of the lattice theories


Recently I've been in need of a theory of complete lattices.

There are two on offer:

- HOL/Lattice/*

This look really polished but uses a type class hierarchy distinct from the rest of the HOL image.

It includes a type for dual orders, which I need.

- HOL/Complete_Lattice.thy and it's friend HOL/Inductive.thy

These use the standard HOL type classes. There are lots of proofs of dual results but no "dual" type constructor. Also the syntax for lattices gets nuked at the end of the development.

In both cases there is no support for product lattices, which is straightforward to add.

I am sure there are more differences than just these.

I also note that there is another definition of partial orders (etc) in HOLCF, and probably elsewhere.

Has there been enough exploration of this design space such that the one true order and lattice theory is waiting to spring forth?

More generally, is there (or should there be) a bug/feature/wishlist tracker for Isabelle for these sorts of things? It might help reduce parallel developments, or least clarify what their relative strengths are.



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