[isabelle-dev] Private modifier and qualifiers [was Interpretation in arbitrary targets.]

[Makarius]

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 
> 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