[isabelle-dev] Syntax for lattice operations?

[Tobias Nipkow]

On 11/06/2016 21:26, Florian Haftmann wrote:
>> For the moment I think bold syntax in the first choice.  In the middle
>> run I would suggest to have a closer look at HOLCF/Porder.thy to see
>> whether something can be done to integrate it more with the standard
>> type classes;  a least it formalizes a lot about upper / lower bounds
>> which is not HOLCF-specific in any way, so it could go to HOL/Library
>> for example.
>
> After a closer look I came to conclusion that the use of Sup syntax in
> HOLCF/Porder.thy is very application-specific.  And it is a deliberate
> separate type class hierarchy since these type classes are tailored
> towards continuous function space.
>
> So maybe the best option here is to stay with plain ASCII syntax: ‹LUB
> x∈A. f x›. – to emphasize its somewhat specific application.

The lub operation in is a lattice-theoretic supremum. So in principle we should 
be able to use operator names and syntax for that; otherwise there is something 
wrong (or maybe our type classes are inadequate).

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.

Tobias

> Cheers,
> 	Florian
>
>
>
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>

-------------- 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/0f973880/attachment.bin>