[isabelle-dev] Typedef and localization

[Jasmin Christian Blanchette]

Hi all,

I reported the following issue to Florian. Since it's a general "philosophy" thing he suggested I discuss it on the dev list.

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.

Any opinions?

Jasmin