Stream: Beginner Questions

Topic: Changing type classes in locales


view this post on Zulip Nicolò Cavalleri (Jun 21 2021 at 14:34):

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?

view this post on Zulip Manuel Eberl (Jun 21 2021 at 14:36):

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

view this post on Zulip Manuel Eberl (Jun 21 2021 at 14:37):

Note however that the linear already gives you the real_vector constraint anyway.

view this post on Zulip Manuel Eberl (Jun 21 2021 at 14:37):

(You might want real_normed_vector anyway, which contains both.)

view this post on Zulip Nicolò Cavalleri (Jun 21 2021 at 14:47):

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!

view this post on Zulip Manuel Eberl (Jun 21 2021 at 14:51):

Works fine for me. What did you write exactly?

view this post on Zulip Nicolò Cavalleri (Jun 21 2021 at 15:20):

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

view this post on Zulip Manuel Eberl (Jun 21 2021 at 15:21):

No worries!

view this post on Zulip Nicolò Cavalleri (Jun 21 2021 at 15:25):

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?

view this post on Zulip Manuel Eberl (Jun 21 2021 at 15:27):

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.

view this post on Zulip Nicolò Cavalleri (Jun 21 2021 at 15:29):

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

view this post on Zulip Manuel Eberl (Jun 21 2021 at 15:29):

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

view this post on Zulip Manuel Eberl (Jun 21 2021 at 15:29):

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

view this post on Zulip Nicolò Cavalleri (Jun 21 2021 at 15:29):

Ok thanks!

view this post on Zulip Manuel Eberl (Jun 21 2021 at 15:30):

It works well for working with concrete ones.

view this post on Zulip Manuel Eberl (Jun 21 2021 at 15:30):

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

view this post on Zulip Manuel Eberl (Jun 21 2021 at 15:30):

But a topological_real_vector_space would of course be perfectly possible.

view this post on Zulip Manuel Eberl (Jun 21 2021 at 15:31):

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

view this post on Zulip Manuel Eberl (Jun 21 2021 at 15:31):

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.

view this post on Zulip Manuel Eberl (Jun 21 2021 at 15:32):

(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).

view this post on Zulip Nicolò Cavalleri (Jun 21 2021 at 15:36):

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!

view this post on Zulip Manuel Eberl (Jun 21 2021 at 15:38):

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