Re: [isabelle] the state of the lattice theories

Hi Peter,

> OK. This being the case, could (/should) it be moved from the top-level, to e.g. HOL/Library/ or ex/, or maybe Proofs/?

here there are two misunderstandings mixed together:

a) Basically, everything inside HOL/ can be considered a library as long
it is a suitable development to build upon, be it HOL-Algebra or
HOL-Imperative_HOL.  Typically the developer of a (let's call it)
extension is able to tell you whether it can suit your purpose.

b) Proofs/ is not a directory, it is a particular image of the HOL
session run with proof terms.

> On a related note, HOL/Library/ is a zoo. Would it be reasonable to
introduce more structure there, ala Haskell's hierarchical libraries?

It would surely, but we have no hierarchical theory name space (yet).

> 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.

I dimly remember that once Brian and I discussed whether some ordering
stuff could be shared here, but AFAIR the major obstacle was that HOL
orderings have an explicit strict part <, which seems to be inconvenient
for HOLCF.

Hope this helps,



PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

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