[isabelle-dev] Proposal for localized interpretations

[Jasmin Christian Blanchette]

Hi all,

The "interpretation" mechanism, as defined in "Pure/interpretation.ML", is used in a few places in Isabelle, including the new (co)datatype package, for allowing other tools and users to register their hooks. Unfortunately, it works at the theory level, which interacts poorly with local definitions. For example, if you try

   locale A =
    fixes a :: 'a
    assumes "a = a"
   begin

   datatype_new 'b x = X 'b

   end

with Isabelle2014, you will get

   Undeclared hyps:
       A a
   The error(s) above occurred for the goal statement⌂:
   left_total R ⟹ left_total (A.rel_x R)

This error arises in the Transfer hook. I can think of no way to solve this at the theory level.

To solve this issue, I introduced my own interpretation mechanism, in "HOL/Tools/Ctr_Sugar/local_interpretation.ML", that works both on theories and local theories. If you look at it, you will see that it is mostly a copy-paste job. The key insight is that there are three scenarios (taking datatypes as our example):

1. The datatype is defined after the hook is registered.

2a. The datatype is defined before the hook is registered.

2b. The dataype and the hooks are registered in two parallel theories, which are later merged.

In case 1, one can imagine having the datatype directly giving its local theory to the hook. This is what "local_interpretation.ML" does, and this is enough to solve the problem in the example above. In case 2a and 2b, things have to be done at the theory level, like before, but this is a rarer case (e.g. we have no local datatypes in "Main"). Also, the odd signature management that was necessary before to make 2a and 2b work (cf. my April 2 email to this mailing list) is now centralized (cf. e6e3b20340be).

I would like to propose either replacing the old mechanism by the new one or having both live in parallel in "Pure". It is certainly not perfect, but it is IMO an improvement over the statu quo. What do you think?

Jasmin