[isabelle-dev] Locale interpretation with mixins
florian.haftmann at informatik.tu-muenchen.de
Sun May 13 11:06:02 CEST 2012
> 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.
thanks for reminding me of that. So, an interpretation is a composition
of two morphisms phi and sigma, where
* phi is the instantiation morphism and
* sigma is a mixin morphism
Sigma in an abstract sense is generic, and, I guess, also the
implementation does not make any further assumptions on it. It is
exposed by two user interfaces:
* the »where« clause of interpretation
* the class target
I deem the discussion about Tools/interpretation_with_defs.ML is mostly
about user interface issues rather than generic mixin morphisms.
> a) This is intentional. Mathematics is full of examples where a concept
> can be defined differently (more easily) in a situation that is more
> I might have to tweak inheritance of rewrite morphisms in the
> future, though, and that's why the documentation is relatively vague.
Underspecification is a powerful defense shield ;-).
> 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.
I think the problem is that we would need sigma^-1 for this since we
have to apply it to a subgoal rather than a plain theorem. As long as
sigma does only rewriting, this is no fundamental problem.
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 262 bytes
Desc: OpenPGP digital signature
More information about the isabelle-dev