[isabelle-dev] Nominal and FinFuns from the AFP

[Makarius]

On Thu, 31 May 2012, Andreas Lochbihler wrote:

>> At some point, when I have bundles ready to work with the existing
>> notation commands, we can fine-tune this scheme further, to allow users to
>> 'include' syntax in local situations.
> I tried to implement the new syntax for FinFuns with bundles and Brian's 
> notation attribute 
> (https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/2012-April/002585.html), 
> but it was not satisfactory.

I did not have time yet to look more closely at that.

Note that notation is based on "syntax declarations" of the local theory 
infrastructure, which is slightly different from what you have in 
attributes.  So notation as attributes is a bad idea.

Generally it is important to avoid too many concurrent attempts to do 
things half way, it will take extra time to sort it out and re-unify 
diverging approaches.

So users need to wait until I find time to continue work on the 'bundle' 
concept, and its further potential.


> 1. I did not know how to get dynamic bundles, i.e., how to add 
> declarations one after the other to a bundle. Hence, I would have to 
> introduce all the notation in a single place before which all constants 
> must have been defined.

The concept you are describing here is called locale.  Bundles are static.


> 2. Theory-level commands like interpretation do not work inside an 
> auxiliary context and neither can they cope wth "includes". Hence, I 
> cannot use such pretty syntax in the parameter instantiations for 
> interpretation. This possibly also applies to the where clause although 
> I did not need that for FinFun.

This looks like another refinement to be done eventually.  Such things 
need time to consolitate.  For the moment it is just something that is not 
supported.


 	Makarius