Suppose I have a locale that depends on a certain type that we require to satisfy certain type class hypotheses, e.g.

```
locale test =
fixes f :: "('a :: t2_space) => ('b :: t2_space)"
assumes cont: "continuous_on UNIV f"
```

and I want to extend it to a locale that adds other hypotheses but that also needs to put other instances on my types, e.g.

```
locale test_2 = test + assumes linear: "linear f"
```

for which I need e.g. `'b :: real_vector`

. How do I specify this new requirement?

```
locale test_2 =
test f for f :: "'a :: {real_vector, t2_space} ⇒ 'b :: {real_vector, t2_space}" +
assumes linear: "linear f"
```

Note however that the `linear`

already gives you the `real_vector`

constraint anyway.

(You might want `real_normed_vector`

anyway, which contains both.)

Manuel Eberl said:

`locale test_2 = test f for f :: "'a :: {real_vector, t2_space} ⇒ 'b :: {real_vector, t2_space}" + assumes linear: "linear f"`

If I do so it says `Parameter(s) declared simultaneously in expression and for clause: f`

!

Works fine for me. What did you write exactly?

Ops I forgot the f... it works indeed, sorry!

No worries!

Manuel Eberl said:

(You might want

`real_normed_vector`

anyway, which contains both.)

What if I want it to be a topological vector space whose topology does not come from a norm: is there a topological_vector_space in HOL?

Hm, if anything it would have to be `topological_real_vector_space`

because type classes in Isabelle cannot have more than one type variable, i.e. you cannot have a `vector_space`

type class, only a `real_vector_space`

class.

Well, that would be fine: I am working with real numbers only, but it does not exist yet, right?

I had a quick look and didn't find it, no.

Isabelle's type class system is really not great for showing "abstract" results about structures due to its limitations.

Ok thanks!

It works well for working with concrete ones.

But if you want to do fancier stuff you may have to work entirely with locales instead.

But a `topological_real_vector_space`

would of course be perfectly possible.

It probably doesn't exist because for the "interesting" real topological vector spaces the topology is always induced by a norm

Especially since the type class approach only allows you to fashion your type with **one** canonical topology. And that's probably going to be the one induced by the norm.

(There are ways to work with topologies in a more liberal way though, there is a type `'a toplogy`

representing a topology on the type `'a`

, and then you can e.g. write `openin top X`

to say that `X`

is open in the topology `top`

).

Manuel Eberl said:

It probably doesn't exist because for the "interesting" real topological vector spaces the topology is always induced by a norm

I kind of disagree with this (what about infinite dimensional Frechet spaces?) but I get your point! My problem is that I am trying to write code that works with the current library for smooth manifolds, so I cannot make a lot of choices in the implementaion, otherwise I would certainly follow your tip of using locales! In any case there's no problem here, since you say `topological_real_vector_space`

can be done and I only need that!

The smooth manifold development was already pushing what you can do with the current formalisation in a lot of ways

Last updated: Sep 25 2021 at 08:21 UTC