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.haftm...@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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
