Nicolò Cavalleri (Jun 21 2021 at 14:34): 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?
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"
Note however that the linear already gives you the real_vector constraint anyway.
Manuel Eberl (Jun 21 2021 at 14:37):(You might want real_normed_vector anyway, which contains both.)
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!
Manuel Eberl (Jun 21 2021 at 14:51):Works fine for me. What did you write exactly?
Nicolò Cavalleri (Jun 21 2021 at 15:20):Ops I forgot the f... it works indeed, sorry!
Manuel Eberl (Jun 21 2021 at 15:21):No worries!
Nicolò Cavalleri (Jun 21 2021 at 15:25):Manuel Eberl said:
(You might want
real_normed_vectoranyway, 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?
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.
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?
Manuel Eberl (Jun 21 2021 at 15:29):I had a quick look and didn't find it, no.
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.
Nicolò Cavalleri (Jun 21 2021 at 15:29):Ok thanks!
Manuel Eberl (Jun 21 2021 at 15:30):It works well for working with concrete ones.
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.
Manuel Eberl (Jun 21 2021 at 15:30):But a topological_real_vector_space would of course be perfectly possible.
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
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.
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).
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!
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: Dec 21 2024 at 16:20 UTC