[isabelle] Extra type variables, type classes and locales



Hallo,

I have with a hidden extra type variable again and again I have no
clue what exactly went wrong. I've made a small example:

class testC = type +
fixes from_nat :: "nat => 'a"
 and  to_nat :: "'a => nat"

locale Test =
fixes  dummy :: "'a::testC"
assumes dd: "ALL z::'a::testC. to_nat z ~= 0"
begin

definition ftest :: "nat => 'a list" where "ftest n == [from_nat n]"

inductive test::"nat => nat => bool"
where
"((ftest a)::'a list) = ((ftest b)::'a list) ==> test a b"
...

I thought the locale not only fixed dummy but also 'a so that it isn't
necessarily an extra type variable in the inductive definition. Am I
wrong or is there another mistake in my example?

Thanks in advance,
Christoph





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.