[isabelle-dev] Example for global interpretation into instantiation [was: Future of permanent_interpretation]

[Clemens Ballarin]

Hi Florian,

I didn't have time to look at your patches, and since I only have superficial knowledge of instantiation contexts I didn't fully understand the example either.  I guess though that the purpose of these global interpretations is to propagate some constant declarations into the surrounding theory.  If this is useful we should certainly have such a command.

What I still fail to understand is why you want to use 'global_interpretation' as keyword if the command occurs directly in a theory.  This is redundant.  I now take this as a temporary solution until there is some better terminology for distinguishing kinds of interpretations, and I very much hope that we will not get into another debate about renaming 'interpretation' to 'global_interpretation' or similar after the 2016 release.

Clemens


On 17 December, 2015 17:49 CET, Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de> wrote: 
 
> Hi Clemens,
> 
> I have found a potential example for global interpretation into
> instantiation in the existing Isabelle sources.
> 
> The example is presented in the attached patches, which can be applied
> in alphabetical order on top of 32a530a5c54c.
> 
> The first patch experimentally introduces a global_interpretation
> keyword, which is then used in theory src/HOL/Library/Saturated.thy:
> 
> instantiation sat :: (len) "{Inf, Sup}"
> begin
> 
> global_interpretation Inf_sat: semilattice_neutr_set min "top :: 'a sat"
>   defines Inf_sat = Inf_sat.F
>   by standard (simp add: min_def)
> 
> global_interpretation Sup_sat: semilattice_neutr_set max "bot :: 'a sat"
>   defines Sup_sat = Sup_sat.F
>   by standard (simp add: max_def bot.extremum_unique)
> 
> end
> 
> Here we have a clear distinction between interpretation, which would
> only last until the closing end, and the explicitly permanent global
> interpretation which provides the necessary instance definitions.
> 
> This pattern, which uses interpretation as a kind of simple definitional
> package, is very common nowadays, as can be seen in theories like
> src/HOL/Groups_Big.thy, src/HOL/Groups_List.thy,
> src/HOL/Lattices_Big.thy or src/HOL/Library/Multiset.thy.
> 
> I have prepared this to give some evidence that my insistence on proper
> distinction between (confined) interpretation and (permanent) global
> interpretation has significant practical implications (although the
> experimental nature of the patches exhibits some issues in the internal
> machinery which would have to worked out properly first).  So, it is
> really a good idea to have a separate keyword »global_interpretation«.
> 
> Hence, before letting »permanent_interpretation« stand as it is, I would
> really prefer to replace the existing occurrences by
> »global_interpretation«, to avoid confusion in the long run.
> 
> So, my minimal plan for the upcoming release would be:
> * Provide »global_interpretation« as separate keyword.
> * Discontinue »permanent_interpretation« entirely – remaining
> occurrences are suitable for »global_interpretation«.
> * »interpretation« retains its current traditional semantics.  No
> systematic replacement by »global_interpretation«.
> * Polish the documentation accordingly.
> 
> I have no idea whether you have a time slot to consider and give
> feedback on this; anyway this plan is quite minimal invasive wrt.
> existing sources, so I am confident that it is appropriate for the
> upcoming release.
> 
> All the best,
>     Florian
> 
> -- 
> 
> PGP available:
> http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de