Re: [isabelle] Extra type variables in constdef

• To: isabelle-users at cl.cam.ac.uk
• Subject: Re: [isabelle] Extra type variables in constdef
• From: Nicole Rauch <rauch at informatik.uni-kl.de>
• Date: Thu, 4 Oct 2007 15:04:30 +0200
• References: <D83FEB81-38AA-44DA-A5D0-43BD1005E9CC@informatik.uni-kl.de> <46F38853.5060205@informatik.tu-muenchen.de> <Pine.LNX.4.63.0709211610550.29132@atbroy100.informatik.tu-muenchen.de>

```Dear all,

On 21.09.2007, at 16:13, Makarius wrote:

```
```On Fri, 21 Sep 2007, Florian Haftmann wrote:

```
```constsdefs
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

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

Now I want to declare a set inductively like this:

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

inductive x
intros

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:

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

inductive x
intros

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?
```