Email Gateway (Aug 19 2022 at 16:55): 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
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
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: Nov 21 2024 at 12:39 UTC