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-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
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
