[isabelle-dev] Typedef and localization
Jasmin Christian Blanchette
jasmin.blanchette at gmail.com
Mon Sep 13 15:19:42 CEST 2010
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
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.
More information about the isabelle-dev