On 12/06/2016 18:22, Florian Haftmann wrote:
Thus I would like to understand why we cannot reuse Sup etc in HOLCF like we do for all the other variants of lattices we have. We would probably need a suitable type class because at the moment lub is unrestricted.For each type class, per type constructor there is at most *one* instance. If we use the standard HOL class hierarchy for HOLCF, we would e.g. enforce the order on pairs to be component-wise due to the required / given instance of cpo in HOLCF and hence rule out e.g. lexicographic ordering on pairs. Hence the use of a separate type class hierarchy makes sense for that specific application.
You are saying that the problem is the ordering which would be shared, which is why we use "⊑" in HOLCF rather than "<=".
But that argument applies to any instantiation of the order on products. That is, any application that instantiates the product order should therefore not use the generic "<="? Probably not if it is a development that is supposed to be the basis for many others, like HOLCF?
So maybe the deeper reason is indeed the usual problem with type classes, in which case I would support the plain ASCII "LUB".
Tobias
Cheers,
Florian
smime.p7s
Description: S/MIME Cryptographic Signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
