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_______________________________________________
Isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
