On Sun, 7 Apr 2013, Clemens Ballarin wrote:
Quoting Makarius <[email protected]>:
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
concept.
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
remember).
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:
context
begin
private definition ...
private lemma ...
private interpretation ...
private notation
definition ...
theorem ...
end
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
is this:
bundle my_decls =
foo [simp]
bar [intro]
baz [elim]
context includes my_decls
begin
theorem ...
end
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.
Makarius
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
