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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
