[isabelle-dev] [isabelle] Interpretation inside locale raises DUP

[Florian Haftmann]

> 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

	Florian

> 
> 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
>>
>  
>  
>  
>  
> 

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 263 bytes
Desc: OpenPGP digital signature
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20131217/b3ffe2c2/attachment.asc>