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



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

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: Bundle_vs_Locale.thy
Description: application/extension-thy

Attachment: signature.asc
Description: OpenPGP digital signature



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