[isabelle-dev] Locale interpretation with mixins

[Florian Haftmann]

Hi Clemens,

> 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
> concrete.

I agree.

> 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.

Cheers,
	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: signature.asc
Type: application/pgp-signature
Size: 262 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20120513/bf73bf74/attachment.sig>