[isabelle-dev] [isabelle] Interpretation inside locale raises DUP
florian.haftmann at informatik.tu-muenchen.de
Tue Dec 17 20:24:18 CET 2013
> 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.
See now http://isabelle.in.tum.de/reports/Isabelle/rev/e58623a33ba5
> 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 =
>>> 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)
>>> |> Idents.put (merge_idents (marked, marked'))
>>> |> Context.proof_of
>> 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
>> 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
>> (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,
>> PGP available:
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 263 bytes
Desc: OpenPGP digital signature
More information about the isabelle-dev