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