Email Gateway (Aug 21 2022 at 20:21): Email Gateway (Aug 21 2022 at 20:21):From: Dominique Unruh <cl-isabelle-users@lists.cam.ac.uk>
Hello,
I ran into the following problem with inheritance of locales (when
trying to update the Complex_Bounded_Operator library on AFP).
I have the locale linear (defined in the Isabelle library) for
real-linear functions. I am defining the locale clinear analogously.
Now a complex-linear function is also real-linear.
So I add "sublocale clinear ⊆ linear".
However, doing so leads to an error: both linear and clinear contain a
sub-namespace vs1 created by Vector_Spaces.linear, so interpreting the
locale clinear produces a name conflict from then on. (I.e., clinear is
unusable)
I demonstrate the problem in the attached theory.
The problem can be circumvented by changing the declaration of locale
clinear to say "locale clinear = somename: Vector_Spaces.linear ...."
but that is inconvenient because then all theorems of clinear would have
to be prefixed.
It would be better if it would be possible to put everything from linear
under a prefix (e.g., "sublocale clinear ⊆ somename: linear" or
something) or at least to rename the vs1,from linear but I don't know how.
What's the best way to resolve this problem?
Best wishes,
Dominique.
Scratch.thy
Email Gateway (Aug 22 2022 at 09:06):From: Lukas Stevens <lukas.stevens+isabelle-users@in.tum.de>
Hi,
I must be missing something because you can actually do sublocale
clinear ⊆ linear: linear.
Email Gateway (Aug 22 2022 at 10:33):From: Dominique Unruh <cl-isabelle-users@lists.cam.ac.uk>
Hi,
I must be missing something because you can actually do sublocale
clinear ⊆ linear: linear.
Indeed you can. The error is delayed until you use the locale again.
You cannot, for example, do "lemma (in clinear) ..." or "context clinear
begin". As far as I can tell, there is no way how you can use clinear
after the sublocale command, so I think it's fair to say that the
sublocale command failed (it would probably be good to give the error
there, in fact).
Best wishes,
Dominique.
Email Gateway (Aug 22 2022 at 11:21):From: Stepan Holub <holub@karlin.mff.cuni.cz>
Hi, Dominique,
this works for me (in your Scratch.thy):
sublocale clinear ⊆ linear: linear
apply standard by (auto simp add: add scaleR_scaleC scale)
context clinear
begin
thm vs1.scale_zero_left
thm linear.vs1.scale_zero_left
end
Stepan
Email Gateway (Aug 22 2022 at 11:57):From: Lukas Stevens <stevensl@in.tum.de>
Hi,
I must be missing something because you can actually do sublocale
clinear ⊆ linear: linear.
smime.p7s
Email Gateway (Aug 22 2022 at 21:02):From: Dominique Unruh <cl-isabelle-users@lists.cam.ac.uk>
Hi Stepan and Lukas,
you are right! "sublocale clinear ⊆ linear: linear" indeed works.
I had not realized that the invented syntax I added in my text just to
illustrate what I mean is actually valid syntax and solves my problem.
Slightly embarrassing, but thanks for your answers! :)
Best wishes,
Dominique.
Last updated: Jan 04 2025 at 20:18 UTC