Stream: Beginner Questions

Topic: real_vector.subspace


view this post on Zulip Nicolò Cavalleri (Jun 16 2021 at 18:03):

I am trying to understand the definition of subspace for vector bundles in Isabelle. If I ctrl+click subspace, Isabelle takes me to the code

global_interpretation real_vector?: vector_space "scaleR :: real ⇒ 'a ⇒ 'a :: real_vector"
  rewrites "Vector_Spaces.linear (*⇩R) (*⇩R) = linear"
    and "Vector_Spaces.linear (*) (*⇩R) = linear"
  defines dependent_raw_def: dependent = real_vector.dependent
    and representation_raw_def: representation = real_vector.representation
    and subspace_raw_def: subspace = real_vector.subspace
    and span_raw_def: span = real_vector.span
    and extend_basis_raw_def: extend_basis = real_vector.extend_basis
    and dim_raw_def: dim = real_vector.dim

However at this point I cannot ctrl+click anymore because Isabell does not compile the files in the HOL folder (because of the message error "Cannot update finished theory" that I saw in the mailing list to be substantially unsolvable). So I am not able to learn more how a subspace is implemented. Can someone point me out where to look for the real definition or a workaround to the ctrl click problem? I was not really able to understand the workarounds proposed by @Jakub Kądziołka in the mailing list

view this post on Zulip Jakub Kądziołka (Jun 16 2021 at 20:15):

Could you link to the mail of mine you're referring to?

view this post on Zulip Nicolò Cavalleri (Jun 17 2021 at 10:02):

https://isabelle.zulipchat.com/#narrow/stream/247541-Mirror.3A-Isabelle.20Users.20Mailing.20List/topic/.5Bisabelle.5D.20Go-to-definition.20doesn't.20work.20when.20exploring.20l.2E.2E.2E/near/221478195

view this post on Zulip Jakub Kądziołka (Jun 17 2021 at 15:31):

Ah, what I was suggesting there is to copy the code you posted here into the theory you're writing, so that it gets properly parsed by the IDE

view this post on Zulip Jakub Kądziołka (Jun 17 2021 at 15:31):

and then you can ctrl+click one layer deeper

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

Well if I do so in this case it takes me back to that same line in real_vector_spaces, so I am puzzled: what is the actual definition of subspaces?

view this post on Zulip Jakub Kądziołka (Jun 17 2021 at 17:37):

Take a look at vector_space

view this post on Zulip Nicolò Cavalleri (Jun 17 2021 at 17:44):

I tried but the first occurence of it in the file Vector_Spaces seems to be in the line

lemma subspace_sums: "⟦subspace S; subspace T⟧ ⟹ subspace {x + y|x y. x ∈ S ∧ y ∈ T}"

so I am still wondering where it all starts! I am not looking very hard in all files because I wish there was a way to find the definition automatically without me looking for it... But I can try harder if this is not possible

view this post on Zulip Jakub Kądziołka (Jun 17 2021 at 17:47):

hmm, looks like Isabelle's go-to-definition considers something that simply copies a symbol between namespaces to be a definition

view this post on Zulip Nicolò Cavalleri (Jun 17 2021 at 17:51):

But is the definition supposed to be in that file? Because I looked at all occurrences of subspace in that file and I did not find it... What other file could I look at? If I ctrl+click it it takes me to Real Vector Spaces even if the lemma is about subspaces of vector spaces on a generic field!

view this post on Zulip Manuel Eberl (Jun 17 2021 at 18:13):

It's in ~~/src/HOL/Modules.thy. Yes, finding definitions for constants coming from locales can be annoying. One way is to do something like find_consts "name:subspace" and see if it shows up in that list. In this case you find Modules.module.subspace.

view this post on Zulip Nicolò Cavalleri (Jun 17 2021 at 18:17):

What do you mean with "do find_consts "name:subspace""? If I type it in the middle of a file it tells me Inner syntax error⌂

view this post on Zulip Manuel Eberl (Jun 17 2021 at 18:18):

Sorry, that should be find_consts name:"subspace". You can do the same thing with the "Query" panel.

view this post on Zulip Manuel Eberl (Jun 17 2021 at 18:18):

(I for one never use that one though so I'm not sure how it works)

view this post on Zulip Manuel Eberl (Jun 17 2021 at 18:19):

You just put the find_consts invocation just about anywhere in your Isabelle file and it will search for constants matching that query, i.e. having the given type or, in this case, name.

view this post on Zulip Manuel Eberl (Jun 17 2021 at 18:19):

There's also find_theorems, which works similarly.

view this post on Zulip Nicolò Cavalleri (Jun 17 2021 at 18:20):

Ok thanks that works! I can't find the query panel but find_consts does the job

view this post on Zulip Nicolò Cavalleri (Jun 17 2021 at 18:21):

As for the problem of Isabelle not being able to typecheck the files in the HOL folder you agree there is no easy workaround right?

view this post on Zulip Nicolò Cavalleri (Jun 17 2021 at 18:21):

As in that does not involve copying code

view this post on Zulip Manuel Eberl (Jun 17 2021 at 18:23):

No, there isn't, currently. It's a known issue but not one that is easy to fix, apparently, or Makarius would have done it long ago.


Last updated: Sep 25 2021 at 09:17 UTC