Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Calling sublocale A < B in A’s context?

Email Gateway (Aug 19 2022 at 12:10):

From: Joachim Breitner <breitner@kit.edu>
Hi,

I have a pattern in my theories where I have a series of locales, each
refining the previous, e.g.

locale A =
fixes param :: bool
begin
lemma A_lem: "param = param"..
end

locale B = A + assumes "param = True"

and then in a different locale, I instantiate the initial locale and
step-for-step work through the assumptions of the following locales. So
what I’d like to do is something like

locale C =
fixes n :: nat
begin
(* ... *)
interpretation A "n = 0".
(* ... *)
lemma n: "n = 0" sorry
interpretation B "n = 0" by (unfold_locales, simp add: n)
(* ... *)
end

but (as documented, and quite correctly) now the results from locales A
and B are not available when interpreting C, or even when opening
"context C" again later. So what I have to do instead is:

locale C =
fixes n :: nat
begin
(* ... *)
end
sublocale C < A "n = 0".
context C begin
(* ... *)
lemma n: "n = 0" sorry
end
sublocale C < B "n = 0" by (unfold_locales, simp add: n)
context C begin
(* ... *)
end

which I find a bit ugly. Is there a way to declare a sublocale
relationship for the current locale form within that locale?

Thanks,
Joachim
signature.asc

Last updated: Apr 23 2024 at 08:19 UTC