Does anyone know where to find documentation on the "itself" type constructor? Why is it needed? Same question for the "dummy" datatype.

When you define something like

```
definition P :: bool where
"P = (∀x y. x = y)"
```

or

```
definition Q :: bool where
"Q = finite UNIV"
```

you have an implicit dependency on a type parameter `'a`

that does not appear in the type of `P`

and `Q`

, e.g. the value of `P`

and `Q`

may depend on which type you pick. Therefore, an artificial dummy parameter of type `'a itself`

is introduced to make this explicit, where `'a itself`

is a singleton type whose only value is `Pure.type`

.

This allows you to write e.g. `P (Pure.type :: nat itself)`

to specify that you want the `P`

for the type `nat`

. A more convenient way to write the values of this singleton type is with the `TYPE`

syntax, e.g. `P TYPE(nat)`

.

One "real-life" example of this is the dimension of a Euclidean space. Euclidean spaces in Isabelle/HOL are modelled as a type class `euclidean_space`

, and then you can define

```
definition dimension :: "'a :: euclidean_space ⇒ nat" where
"dimension = card (Basis :: 'a set)"
```

and then use this as e.g. `dimension TYPE(real) = 1`

, `dimension TYPE(complex) = 2`

.

Not sure if or where this is documented.

As for the "dummy" datatype, not sure what you mean by that.

There is `Pure.dummy_pattern`

, which I think is not a "proper" term and is used for pattern matching (i.e. the `_`

that you can write in `case`

expressions, function definitions, etc.)

Not sure if that's what you meant.

Or are you talking about the

```
datatype (plugins only: extraction) "term" = dummy_term
```

from `HOL.Code_Evaluation`

?

Manuel Eberl said:

Or are you talking about the

`datatype (plugins only: extraction) "term" = dummy_term`

from

`HOL.Code_Evaluation`

?

No, just the type

```
term "x :: dummy"
```

If that is the same as `Term.dummyT`

, then it is often used to leave type holes in a term and then fill them with `Syntax.check_term`

.

@Manuel Eberl

Thanks.

Manuel Eberl said:

Not sure if or where this is documented.

I could not find an explanation for it, neither in the Isabelle sources nor via google. Isabelle is probably really hard to use if you don't share an office with an Isabelle elder :stuck_out_tongue:

Found it! §2.3.2 of the Isabelle/Isar implementation manual.

Perhaps the explanation is a bit less, uh, easy to understand than the one I wrote above.

I'm not even sure where I learnt about this; I think I just encountered it at some point and then it seemed kind of obvious what it was.

But yeah I'm sure it can be confusing at first.

Last updated: Sep 25 2021 at 09:17 UTC