[isabelle-dev] Locale interpretation with mixins

[Florian Haftmann]

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_1.thy
Type: application/x-extension-thy
Size: 2138 bytes
Desc: not available
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20120501/3e1d4ba3/attachment-0002.bin>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: Locale_Mixin_Subsumption_2.thy
Type: application/x-extension-thy
Size: 2117 bytes
Desc: not available
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20120501/3e1d4ba3/attachment-0003.bin>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 262 bytes
Desc: OpenPGP digital signature
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20120501/3e1d4ba3/attachment-0001.asc>