Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Locale, sublocale, Interpretations and a clean...


view this post on Zulip Email Gateway (Aug 19 2022 at 16:55):

From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear Joachim,

The assumptions in your locales lack their names, so the example as such does not work. I
guess that locale A should have assumption "a" and "B" has "b".

Interpretations of locales at the theory level have the disadvantage that they generate a
huge number of theorems that both consume memory and pollute the name space. In
JinjaThreads, I had quite a number of such interpretations and they once caused memory
problems (before David Matthews implemented a smarter GC). Nowadays, I try to avoid
interpretations at the theory level. Instead, use two options. Either, I interpret a
locale in an unnamed context whenever I need it. Or, I declare a wrapper locale without
parameters in which I import the locales via sublocale. In both cases, I get all the
theorems from that locale that I want - independent of the imports.

One thing that might help me to work around the limitation would be if

context B begin sublocale A "int B" end

made the theorem "B x ==> A (int x)" (which I believe is generated
there) available by some name (e.g. B_sublocale_of_A), and similarly for
interpretations.
It is unfortunate that this theorem is not generated automatically. Therefore, I normally
prove the theorem first as a lemma B_to_A (by copying the proof of the interpretation
command). Then, I replace the proof for the interpretation command with "by(rule B_to_A)".

If you cannot change the interpretation itself, you can get B_to_A by stating it and
proving it with unfold_locales.

Andreas

view this post on Zulip Email Gateway (Aug 19 2022 at 16:55):

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

That seems to be precisely the work-around I’m looking at.

With
theory C_Imp
imports C
begin

locale C_True
begin
sublocale C True.
end

end

I can change my integration theory to read

theory Integration
imports A B C C_Imp C_to_B B_to_A
begin

interpretation C_True.

theorem "0 < int (if True then 2 else 1)" by (rule a)

end

and everything works as I want it to.

Thanks!
Joachim
signature.asc

view this post on Zulip Email Gateway (Aug 19 2022 at 16:56):

From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear Joachim,

I recommend that you interpret of C_True in an unnamed context like this:

theory Integration
imports A B C C_Imp C_to_B B_to_A
begin

context begin
interpretation C_True.

theorem "0 < int (if True then 2 else 1)" by (rule a)
end

The reason is the following:
Suppose that you or someone else adds another sublocale declaration to C later in some
unrelated theory and then imports your theory. With an interpretation at the global theory
level, there is no way to get the theorems from the newly imported locales, because the
interpretation of C_True is still active. If it is done in an unnamed context, the
interpretation vanished at the "end" and you can re-interpret it later again.

Best,
Andreas


Last updated: Mar 29 2024 at 08:18 UTC