[isabelle-dev] Complete Distributive Lattice

[viorel.preoteasa at gmail.com]

I am working on the generalization of the complete distributive lattices. Changing the axioms from

 

sup  x (Inf Y) = …

 

to the more general form:

 

Sup (Inf ` A) = …

 

I have done these changes already for the previous release candidate, and I just need to integrate them into the current repository version.

I have a question about how to organize these changes. The problem is that most of the results for the more general lattice (instantiations 

to set, fun) require Hilbert_Choice which is not available in Complete_Lattice. Now I have added all results about complete distributive 

lattices that need Hilbert Choice in Hilbert_Choice.thy. Is this acceptable?

 

Best regards,

 

Viorel Preoteasa

 

 

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20180308/6793fc6c/attachment.html>