[isabelle-dev] Typedef and localization

[Jasmin Christian Blanchette]

Am 10.09.2010 um 17:26 schrieb Makarius:

> So same more explanations here:
> 
>  * A local context is characterized by a mixture of Frees and Vars.  The
>    Frees are like local constants, the Vars express generality (like
>    adhoc quantifiers that have already been generalized).  This is
>    particularly important for type variables, because there is no
>    explicit quantification.
> 
>  * In a global situations "variables" are just "variables", they can be
>    either all fixed or all schematic, but not mixed.  The
>    varify_global / unvarify_global operations allow to flip coins.  The
>    "global" in the name indicates that something special is going on
>    here, outside the usual context discipline.
> 
>    It depends on the situations how things are stored in the background
>    context -- the typedef package prefers the free variant right now (as
>    does the locale infrastructure, IIRC).  Digging through the history
>    further might explain further details, how the typedef of 9cc3df9a606e
>    emerged.

Thanks for the explanations. I was clearly too quick to assume this was a bug. But it remains a quirk in my eyes. Today "Typedef" is still half-local, half-global. There might come the day where it's fully localized and something like

   locale Foo =
   fixes f :: "'a => 'b"

   typedef bar = "UNIV::'a multiset=>bool"

is accepted by Isabelle. Then the calls to "varify_global" in various tools will be broken. Assuming that full localization is the goal, wouldn't a good first step be to avoid clashes with the context in "Typedef", "Datatype", "Quotient_Type", etc.? Then tool authors could start migrating their "varify_global"s to a proper context-sensitive varify (if they haven't done so already, as I accidentally did in Nitpick).

Anyway, I've already fixed Nitpick so I can live with the current situation.

Jasmin