[isabelle-dev] Private modifier and qualifiers [was Interpretation in arbitrary targets.]
makarius at sketis.net
Fri Apr 12 21:50:13 CEST 2013
On Sun, 7 Apr 2013, Clemens Ballarin wrote:
> Quoting Makarius <makarius at sketis.net>:
>> On Tue, 26 Mar 2013, Florian Haftmann wrote:
>> Note that we have one more aspect in the back-end that could help here: the
>> 'private' modifier.
> What would the 'private' modifier do in general? This sounds like a new
It has been in the pipeline only for approx. 4 years.
The basic idea is to control superficial visibility of formal entities
(name space accesses, notation, abbreviations, probably anything that is
managed formally as 'syntax_declaration' -- this also has a special status
in the bootstrapping of complex locale expressions, as you probably
I think there will be no impact on logical aspects here, so foundations,
derived consequences, hints for proof tools (simp, intro, elim, iff) will
be unaffected. Controlling that separately might or might not be a
related agenda -- it is likely to be technically quite different. One
could need a separate 'local' modifier at some point, but this is hard to
anticipate right now.
Note that the question came up here for local contexts, especially
unnamed contexts. For example:
private definition ...
private lemma ...
private interpretation ...
Note that presently, "context begin ... end" has some bias to "leak" most
of its body content. You can keep things local only by including them in
the head, where the context is first constructed (via 'fixes', 'assumes',
and the more recent 'includes' for bundles of declarations).
This means, the way to keep hints for proof tools private in Isabelle2013
bundle my_decls =
context includes my_decls
Another important consideration for 'private' are theory imports, to
reform the default everything-open approach that we've known for 20 years.
This then also touches questions about qualified theory names -- sessions
are properly formalized in Isabelle2013, but session prefixes for theory
names will break many existing tools who expect THY.LOC.XXX names.
More information about the isabelle-dev