Re: [isabelle] Interpretation inside locale raises DUP



Hallo, Florian,

thank you for the analysis.  I have looked at this more closely now and, yes, I believe this is the correct fix.  Please go ahead and push.

Clemens


On 12 December, 2013 14:02 CET, Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de> wrote:

> Hi Clemens,
>
> I have done an analysis, and it seems to me that the critical spot is
>
> > fun init name thy =
> >   activate_all name thy Element.init (Morphism.transfer_morphism o Context.theory_of)
> >     (empty_idents, Context.Proof (Proof_Context.init_global thy))
> >   |-> Idents.put |> Context.proof_of;
>
> Using »empty_idents«, potentially pre-existing idents are chased away,
> whereas registrations are taken over from the initial background theory.
>
> This is no problem as long as
> a) no further registrations are added (as in »interpret«)
> b) the resulting target context is not used to setup further
> interpretations (which would not occur prior to Isabelle2013-1)
>
> I suggest to maintain the set of identifiers from the initial context, e.g.
>
> > fun init name thy =
> >   let
> >     val context = Context.Proof (Proof_Context.init_global thy);
> >     val marked = Idents.get context;
> >     val (marked', context') = activate_all name thy Element.init
> >       (Morphism.transfer_morphism o Context.theory_of) (empty_idents, context)
> >   in
> >     context'
> >     |> Idents.put (merge_idents (marked, marked'))
> >     |> Context.proof_of
> >   end;
>
> I have glimpsed this pattern from roundup itself.
>
> I did an experimental plausibility check which exhibited no problems.
> The only point of manual intervention is in
>
> http://sourceforge.net/p/afp/code/ci/ecad5b18ca0edd5d3f3d257d56a1aff2b2ac0a1b/tree/thys/Launchbury/HSem.thy
>
> the »interpret subpcpo ?S by (rule subpcpo_fjc)«, which explicitly
> relied on re-interpretation of the fragment subpcpo_syn to obtain a
> particular specialized syntax; but this fragment is already shadowed by
> a global schematic interpretation »interpretation subpcpo_syn S for S.« in
>
> http://sourceforge.net/p/afp/code/ci/ecad5b18ca0edd5d3f3d257d56a1aff2b2ac0a1b/tree/thys/Launchbury/HOLCF-Set.thy
>
> (sorry for not giving direct links, but SF does not seem to support this).
>
> Touching such a fundamental thing, I would kindly ask for your opinion
> whether I should push this in that shape or you know about further
> issues which have to be taken care of.
>
> Thanks and all the best,
> 	Florian
>
> --
>
> PGP available:
> http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
>









This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.