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
Locale_Mixin_Subsumption_1.thy
Description: application/extension-thy
Locale_Mixin_Subsumption_2.thy
Description: application/extension-thy
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev