Where is the exact point in the HOL library where it is proven that if the type `'a`

has an instance as a real_vector then functions valued in `'a`

also do? How do I find out these kind of things? On Lean ctrl+click on + takes you to the instance where that type has been given addition but in Isabelle it takes you to the point where + is introduced in Isabelle

There is no `real_vector`

instance for functions in either `HOL`

or `HOL-Analysis`

. What library are you using exactly?

There is one in `Lp.Functional_Spaces`

in the AFP…

I don't know if there is a general way to find out where exactly a particular typeclass instance for a particular type constructor was proven.

I am using the smooth manifolds library. I guess

```
instance "fun" :: (type, real_vector) real_vector
by standard (auto simp: scaleR_fun_def algebra_simps)
```

is then the point where such instance is defined... What is exactly the syntax ` "fun" :: (type, real_vector)`

?

`instance a :: (b, c) d`

means that `'t 'u a :: d`

if `'t :: b`

and `'u :: c`

And "fun" is the internal name of the function type constructor. When you write `'a ⇒ 'b`

, the internal representation of that type is `('a, 'b) fun`

.

I see, the Smooth Manifold entry defines its own vector space instance for functions – presumably in the same way as the `Lp`

entry.

Can I write the instantiation in an equivalent way as

```
instantiation "'a ⇒ ('b :: real_vector)" :: real_vector
```

somehow? It tells me `Undefined type name: "'a ⇒ ('b :: real_vector)"`

No, you have to write `instantiation "fun" :: (type, real_vector) real_vector`

. The bit before the `::`

has to be a type constructor.

Ok, my final goal is to put an instance of `real_vector`

on the type `('a × (('a ⇒ real) ⇒ real))`

which ignores the first coordinate and treats pairs as if they were they second coordinate. Does this mean that I have to put an instance on a generic product of a type and a real vector space? This will probably collide with the instance of product of vector spaces which is more standard I guess

Indeed it says

```
Conflict of type arities:
prod :: (type, real_vector) cancel_ab_semigroup_add and
prod :: (cancel_ab_semigroup_add, cancel_ab_semigroup_add) cancel_ab_semigroup_add
```

You cannot do that in Isabelle. Typeclass instances must *always* be for a type constructor.

What you are trying to do would require something like `FlexibleInstances`

and `OverlappingInstances`

in Haskell, which the Isabelle type class system just doesn't support.

The only way around this would be to introduce a type clone of `'a × (('a ⇒ real) ⇒ real)`

with `type_definition`

, then you can instantiate it in whichever way you want

Manuel Eberl said:

The only way around this would be to introduce a type clone of

`'a × (('a ⇒ real) ⇒ real)`

with`type_definition`

, then you can instantiate it in whichever way you want

Ok thanks this is what I was looking for!

Sorry, type classes in Isabelle are just not very flexible… It's a known problem.

It would be nice to have some kind of deriving via typedef mechanism like in Haskell. This wouldn't require any changes to the core typeclass mechanism.

Lukas Stevens said:

It would be nice to have some kind of deriving via typedef mechanism like in Haskell. This wouldn't require any changes to the core typeclass mechanism.

A topic for a student perhaps?

Last updated: Sep 25 2022 at 23:25 UTC