[isabelle-dev] Syntax for lattice operations?
florian.haftmann at informatik.tu-muenchen.de
Sat Jun 11 10:53:22 CEST 2016
Am 11.06.2016 um 00:13 schrieb Makarius:
> On 10/03/16 11:19, Makarius wrote:
>> On Thu, 10 Mar 2016, Johannes Hölzl wrote:
>>> Alternatively: Would a lattice_syntax locale work nowadays? I remember
>>> I tried it once and for some reason it didn't work. Either notations
>>> aren't supported in locales or they are exported after the context
>> The concept of 'bundle' was introduced for that, e.g. to allow "includes
>> lattice_syntax" for local contexts.
>> Unfortunately, it is not quite finished: notation within bundles is not
>> yet supported. It might be relatively easy to do that, but I am
>> presently working in other corners of the system.
> This thread is still pending, while the bundle concept has been enhanced
> in Isabelle/a59801b7f125.
first, thanks for implementing this; we can now really move forward
wrt. more flexible syntax.
> This shows changes are only needed in relatively isolated places so
> far there was not even any attempt to use the more flexible type class
> operations of main HOL instead of independent operations with
> alternative (bold) syntax.
> How shall we proceed? Make Lattice_Syntax standard and cleanup
> conflicting applications?
I had a quick look at the changesets; as far as I can glimpse, most
occurences are due to LUB from HOLCF/Porder.thy.
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
There are various occurences of no_notation etc. in the HOL and AFP
theories which I will inspect to see what can be done there.
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 819 bytes
Desc: OpenPGP digital signature
More information about the isabelle-dev