[isabelle-dev] Typedef and localization

[Makarius]

On Thu, 9 Sep 2010, Jasmin Christian Blanchette wrote:

> I ran into a strange behavior of "Typedef". The theory below captures 
> the problem:
>
>   theory N
>   imports Multiset
>   begin
>
>   locale Foo =
>   fixes f :: "'a => 'b"
>
>   ML {* Typedef.get_info @{context} @{type_name multiset} *}
>
> Now, 'a and 'b are fixed in the context, and "Typedef.get_info" takes a 
> context, so it should be context-aware. Which means that it shouldn't 
> talk about 'a or 'b, since these are taken by the context already. But 
> it does! This is the result of the invocation above:
>
>  [({Abs_name = "Multiset.Abs_multiset", Rep_name = "Multiset.count", abs_type = "'a Multiset.multiset",
>     rep_type = "'a ⇒ Nat.nat", axiom_name = "Multiset.type_definition_multiset"},
>    {Rep = "count (?x∷?'a multiset) ∈ multiset", set_def =
>     SOME "multiset ≡ {f∷?'a ⇒ nat. finite {x∷?'a. (0∷nat) < f x}}", ...]
>  : Typedef.info list
>
> Notice that "abs_type" and "rep_type" talk about 'a -- but that's just a 
> clash with the 'a that's already fixed in the locale. It should be 'c or 
> ?'a (the latter would require changing the tools based on "Typedef" -- 
> e.g. removing calls to "varify"), but not 'a. Interestingly, the 
> theorems are correctly generalized to ?'a -- it's just "abs_type" and 
> "rep_type" that are broken.

Inspecting the authoritative source, which is the ML text together with 
its history, it says in 
http://isabelle.in.tum.de/repos/isabelle/annotate/9cc3df9a606e/src/HOL/Tools/typedef.ML#l38

type info =
   (*global part*)
   {rep_type: typ, abs_type: typ, Rep_name: string, Abs_name: string, axiom_name: string} *
   (*local part*)
   {inhabited: thm, type_definition: thm, set_def: thm option, Rep: thm, Rep_inverse: thm,
     Abs_inverse: thm, Rep_inject: thm, Abs_inject: thm, Rep_cases: thm, Abs_cases: thm,
     Rep_induct: thm, Abs_induct: thm};

And the log entry of that change:

   Typedef.info: separate global and local part, only the latter is
   transformed by morphisms;

This means things are formally all-right, despite the surprise.


These explanations in the repository always assume a common ground of 
thinking about the system, which might make them appear a bit hermetic at 
some point.

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.


 	Makarius