[isabelle-dev] Syntax for lattice operations?

[Tobias Nipkow]

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
>

-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 5135 bytes
Desc: S/MIME Cryptographic Signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20160612/33c901ec/attachment.bin>