[isabelle-dev] Locale interpretation with mixins

[Clemens Ballarin]

Hi Florian,

What is called mixin in the implementation is a transfer principle  
that is applied in addition to the interpretation morphism.  Currently  
users can only give equations, which yield rewrite morphisms, and  
consequently, the term 'mixin' appears nowhere in the documentation.   
On the other hand, the locale core 'knows' nothing about the  
equations.  For it, their are just general transfer principles.

Regarding your questions:

a) This is intentional.  Mathematics is full of examples where a  
concept can be defined differently (more easily) in a situation that  
is more concrete.  I might have to tweak inheritance of rewrite  
morphisms in the future, though, and that's why the documentation is  
relatively vague.

b) I don't yet see how one could reliably predict which equations  
should be unfolded.  This might be more obvious in the class package.   
For interpretation, we don't even know whether a rewrite morphism is  
related to a definition.

An alternative proof avoiding the 'OF construction' in your example is  
attached.

Clemens


Quoting Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>:

> Hi Clemens,
>
> I stumbled over two issues in locale interpretation.
>
> a) According to the tutorial, in situation like these
>
>   locale A = ?
>     --[ interpretation A: instantiation phi + mixin eqn]-->  theory
>
>   locale B = A + ?
>     --[ interpretation B: instantiation phi] -->             theory
>
> the mixin eqn is implicitly propagated to interpretation B.  I can
> observe this (cf. theory Locale_Mixin_Subsumption_2.thy).
>
> However, in a slightly more general situation
>
>   locale A = ?
>     --[ interpretation A: instantiation phi + mixin eqn]-->  theory
>
>   locale B = A + ?
>     --[ interpretation B: instantiation phi'] -->            theory
>
> where phi' is a more special variant of phi wrt. types, this does not
> hold, i.e. eqn is not part of B (cf. theory
> Locale_Mixin_Subsumption_1.thy, in which this situation appears quite
> natural).
>
> Is this behaviour intentional or a misfit?
>
> b) The examples also show another issue: equations stemming from mixins
> in interpretations are not applied to the interpretation proposition to
> prove itself; consequently, if the assumption part of a locale to
> interpret refers to derived definitions inside the locale, the proof of
> this requires to handle the primitive expanded version of those
> definitions rather than the definitions modulo the given mixins (hence
> the ? [OF this] ? construction in the proofs in the examples).
>
> This situations reminds of similiar experiences with derived definitions
> and the class target, or even the target infrastructure in general,
> where the equations stemming from derived definitions must be folded and
> unfolded in critical situation, cf. e.g.
> http://isabelle.in.tum.de/repos/isabelle/file/064394a1afb7/src/Pure/Isar/class_declaration.ML#l69
> where the fundamental introduction rule for class membership is
> preprocessed with those equations (»Class.these_defs«).  Maybe something
> similar needs to be done here;  due to the dynamic nature of the
> problem, I forsee no other possibility than to extend unfold_locales to
> consider mixin equations also by folding them in the remaining goals.
>
> Btw. these question have arisen when I spent some thought about the
> future of Tools/interpretation_with_defs.ML
>
> All the best,
> 	Florian
>
> --
>
> 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: Locale_Mixin_Subsumption_3.thy
Type: application/octet-stream
Size: 1888 bytes
Desc: not available
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20120506/bc5da3da/attachment-0002.obj>