Email Gateway (Aug 19 2022 at 13:21): Email Gateway (Aug 19 2022 at 13:21):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi all,
with the presence of »confined interpretation« in Isabelle, I asked
myself how this relates to the already existing declaration bundles.
See also attached theory.
The essence:
Conceptually, confined interpretation absorbs declaration bundles
entirely.
Not covered are declaration bundles defined inside a locale since
locales are not nestable.
There is a subtle structural difference:
a) confined interpretation can happen incrementally at arbitrary
positions inside the nested context;
b) inclusion of bundles can only happen at the beginning of a nested
context.
However, this does not make really a difference since you are always
free to open a new nested context if needed. I.e.
…A
interpretation …
…B
turns into
…A
context
includes …
begin
…B
end
This might suggest a declaration »inclusion« which includes a
declaration bundle up to the end of the current nested context, similar
to interpretation, e.g.
context
…
begin
…
inclusion …
…
end
Cheers,
Florian
Bundle_vs_Locale.thy
signature.asc
Email Gateway (Aug 19 2022 at 13:22):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Florian,
There's another difference between locales and bundles: locales can be extended at any
time whereas one cannot change a bundle after its declaration.
Andreas
Last updated: Apr 23 2024 at 20:15 UTC