Re: [isabelle] Locales and bundles in Isabelle – a short comparion



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

On 28/01/14 10:14, Florian Haftmann wrote:
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





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.