real_vector.subspace · Beginner Questions

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

Jakub Kądziołka (Jun 16 2021 at 20:15):

Nicolò Cavalleri (Jun 17 2021 at 10:02):

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

Jakub Kądziołka (Jun 17 2021 at 15:31):

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?

Jakub Kądziołka (Jun 17 2021 at 17:37):

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

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

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!

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.

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⌂

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.

Manuel Eberl (Jun 17 2021 at 18:18):

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.

Manuel Eberl (Jun 17 2021 at 18:19):

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

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?

Nicolò Cavalleri (Jun 17 2021 at 18:21):

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.