Re: [isabelle] Extra type variables in constdef

Dear all,

On 21.09.2007, at 16:13, Makarius wrote:

On Fri, 21 Sep 2007, Florian Haftmann wrote:

  c :: "'a itself => int => bool"
  "c (T::'a itself) x == b (a x :: 'a)"

Just note that there is no need to invent a dummy argument T here, because
the canonical term TYPE('a) of type 'a itself will do the trick.

many thanks for the input, it has solved my problem! But now I ran into another problem:

Suppose I have some axiomatic type classes and some constants defined over them:

axclass A < type
axclass B < type

f :: "'a::A => bool"
g :: "'a::A => 'b::B"
h :: "'b::B => bool"

Now I want to declare a set inductively like this:

x :: "('a::A) set"

inductive x

xf: "f (a::'a::A) ==> a : x"

xg: "h ((g (a::'a::A))::'b::B) ==> a : x"

The second intro rule fails because of an extra type variable.

I tried the same trick as above, declaring the set x like this:

x :: "('a::A * 'b::B itself) set"

inductive x

xf: "f (a::'a::A) ==> (a, TYPE('b::B) ) : x"

xg: "h ((g (a::'a::A))::'b::B) ==> (a, TYPE('b)) : x"

But now, not even the first intro rule is accepted. The error message is

*** Type unification failed: No type arity itself :: type
*** Type error in application: Incompatible operand type
*** Operator: (Pair (a::'a)) :: ??'a => 'a x ??'a
*** Operand: TYPE('b) :: 'b itself
*** The error(s) above occurred for f (a::'a::A) ==> (a, TYPE ('b::B) ) : x
*** At command "inductive".

What is wrong here? Is there any way to add extra type variables to the set specification?

Thanks a lot in advance

Nicole Rauch

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