Re: [isabelle] Interpretation inside locale raises DUP



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

Attachment: signature.asc
Description: OpenPGP digital signature



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