[isabelle-dev] Additional type variable(s) in specification

[Alexander Krauss]

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


Makarius wrote:
> 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 
packages...

Alex