[isabelle-dev] Towards localized syntax: bundle mixins for locale and class specifications – Discussion of alternatives

[Clemens Ballarin]

Hi Florian,

Could you please explain what you mean by "surface context" in the 
documentation of the locale command:

> given bundles take effect in the surface context within both import and 
> body and the potentially following begin / end block

I'm trying to understand where exactly bundles in locale declarations 
are effective. I suppose they are not persisted beyond the locale 
declaration's begin /end block?

Clemens


On 2020-11-27 18:46, Florian Haftmann wrote:
> See now http://isabelle.in.tum.de/repos/isabelle/rev/e7c2848b78e8 for a
> refined and documented version.
> 
> 	Florian
> 
> Am 21.11.20 um 09:01 schrieb Florian Haftmann:
>> Since this thread did not stimulate any activity I will go on to
>> document the syntax in NEWS entries and manuals.
>> 
>> Cheers,
>> 	Florian
>> 
>> Am 01.11.20 um 18:09 schrieb Florian Haftmann:
>>> Dear all,
>>> 
>>> currently the syntax for bundle mixins for locale / class 
>>> specifications
>>> looks as follows:
>>> 
>>>   locale / class foo = import +
>>>     includes bundles
>>>     fixes …
>>>     assumes …
>>>   begin
>>> 
>>>   …
>>> 
>>>   end
>>> 
>>> While this use of »includes« rests firmly on established traditions, 
>>> it
>>> is a little bit unsatisfactory since it also applies to the »import«
>>> expression, but is notated *after* it.
>>> 
>>> I had thought about something like
>>> 
>>>   context
>>>     includes bundles
>>>   begin
>>> 
>>>   locale foo = import +
>>>     fixes …
>>>     assumes …
>>>   begin
>>> 
>>>   …
>>> 
>>>   end
>>> 
>>>   end
>>> 
>>> instead but this would require an artificial construction identifying
>>> nested contexts as »morally being global« internally.
>>> 
>>> A more inspiring solution could be to abandon the existing »includes«
>>> syntax entirely and replace it by a specific toplevel construct, e.g.
>>> 
>>>   including bundles lemma foo: ‹…› if ‹…› for …
>>> 
>>>   including bundles context group
>>>   begin
>>> 
>>>   …
>>> 
>>>   end
>>> 
>>>   including bundles locale bar = …
>>> 
>>> This looks charming but the progressive participle is reserved for
>>> proofs.  For the same reason »with« won't do.
>>> 
>>> Cheers,
>>> 	Florian
>>> 
>>> 
>>> _______________________________________________
>>> isabelle-dev mailing list
>>> isabelle-dev at in.tum.de
>>> https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
>>> 
>> 
>> 
>> _______________________________________________
>> isabelle-dev mailing list
>> isabelle-dev at in.tum.de
>> https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
>> 
> 
> 
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev