[isabelle-dev] Syntax for lattice operations?

[Florian Haftmann]

Hi Makarius,

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
>>> -block.
>>
>> 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
for example.

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.

Cheers,
	Florian

-- 

PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 819 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20160611/057ef439/attachment.sig>