[isabelle-dev] Proposal for localized interpretations

[Jasmin Christian Blanchette]

Hi Florian,

Am 10.09.2014 um 10:22 schrieb Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>:

> when we started this hook business, the situation was as follows:
> 
> a) Hook clients were all for adding type class instances, i.e.
> inherently working a the theory level.
> 
> b) Hooks were a bootstrap device, e.g. after a certain point in the
> theory hierarchy they were considered to be »sealed« (by convention, not
> by implementation).
> 
> c) There were a few experimental theories which would add further hooks
> – these theories are gone nowadays.
> 
> So, the questions IMHO are:
> 
> 1. Is a) still valid today?  Maybe not, since the error in questions
> seems related to transfer.

Right. It's not just used for type class instances. Actually, already with the old package, there were extensions doing other things, e.g. the realizers for program extraction.

For Transfer and Lifting, Ondra is simply trying to derive new theorems from those generated by the BNF package. At the theory level, things get really bad, because he gets e.g. conditional theorems out of the package (with explicit locale assumptions) and would also need to generate theorems with those, which is, you will agree, wrong and infeasible in general. Hence we need a local-theory-to-local-theory connection.

> 2. What is the matter with b)?

I kind of understand what you mean, but not 100%. Could you try again? ;)

As I understand it, it's impossible to fully support every thinkable use case. But as long as the "interpretation" functor is instanciated under "Main", things should work fairly smoothly, and cases 2a and 2b (according to my original email) can only ever happen under "Main", where we have things under control. This leaves us with the clean case 1, where we can (and should IMO!) establish a local-theory-to-local-theory connection.

> I am not sure where to go from here.

Well, I am. My proposal is to kick out "interpretation.ML" and replace it with "local_interpretation.ML".

> Of course to fully generalize we
> would need a concept of »reconstructable«  local theory, i.e. each
> target would provide an operation reenter :: local_theory -> (theory ->
> local_theory) option.  Is it worth the effort?  It appears very similar
> to the ancient infamous reinit operation.

Who is talking about more effort? Why not consider what I proposed at face value?

Jasmin