[isabelle-dev] Additional type variable(s) in specification
krauss at in.tum.de
Thu Dec 2 21:58:47 CET 2010
Brian Huffman wrote:
> *My* first idea was that "typedef" didn't need to be defining a set
> constant at all.
(I would appreciate if we could keep this discussion focused. To discuss
typedef, please start a new thread.)
> When we speak about "users" of packages it covers both ML and Isar
> theory sources, e.g. the function package is a user of the inductive
> package. It is important to keep modularity here.
> The system is able to distinguish between things that are visible in the
> source vs. internal uses of the same specifciation mechanisms to some
> extent, but one needs to look very closely at that when modifying the
> behaviour here.
I think there is a formal difference here that is beyond "Isar" vs. "ML":
a) If function calls inductive, then it is exclusively interested in
getting an inhabitant of a specification in the auxiliary context (which
I nowadays prefer to call the "package context"). Its interpretation in
the target is really arbitrary. Local_Theory.define does this uniformly.
b) A user invocation of inductive via the Isar command does not care
about the package context, which is discarded immediately. Here the
target is what counts. In particular, the image in the target is very
irregular at the moment, since the type arguments are only inserted in
very special situations.
It may be worthwhile to make this distinction explicit somehow, but I
want to do a bit of reading before suggesting a concrete solution.
In general, composability of packages is one of my "favorite" problems.
We are still at the beginning here: whenever a package is used for the
first time by some other code, amusing problems come to light. Maybe at
some point we will arrive at a set of general conventions for modular
More information about the isabelle-dev