* Local theory specification commands may have a 'private' or
'restricted' modifier to limit name space accesses to the local scope,
as provided by some "context begin ... end" block. For example:
context
begin
private definition ...
private definition ...
private lemma ...
lemma ...
lemma ...
theorem ...
end
This refers to Isabelle/83071f4c8ae6.
After more than 10 years in the pipeline, and never-ending efforts to
localize almost all tools, there is now the long anticipated limitation of
name space accesses. There are presently two example applications:
(1) Local tool setup with some auxiliary constants: "induct_forall" etc.
in
http://isabelle.in.tum.de/repos/isabelle/file/83071f4c8ae6/src/HOL/HOL.thy#l1377
(2) Plain specifications that are meant to produce theory-qualified names:
AList.update etc. in
http://isabelle.in.tum.de/repos/isabelle/file/e83ecf0a0ee1/src/HOL/Library/AList.thy#l11
I am still not 100% sure about the choice of keywords. There are two
concepts that are supported: (a) totally inaccessible name space entry,
(b) name space entry that is only accessible by qualified names, not the
base name.
Presently we have:
(a) 'private'
(b) 'restricted'
I first started out implementing 'private' for the sake of Eisbach, which
really needs that. Then I noticed that in practice one mostly uses
'restricted' to eliminated old "hide (open)", but this keyword is a bit
awkward.
Here are some possible alternatives:
(a) 'hidden' (like Long_Name.hidden according to Isabelle/ML terminology)
(b) 'private' (like 'private' in Java/Scala, in non-serious mode)
or:
(a) 'private' (like 'private' on Java/Scala in serious mode)
(b) 'local' (like an ancient Isabelle command of that name)
By non-serious mode I mean the rather easy way to bypass 'private'
declarations on the JVM via reflection. Likewise our logical environment
always allows to access inaccessible names, after some tweaking of the
name space, e.g. via aliases. This could justify the use of 'private' for
what is now 'restricted', or it might be just too confusing to users.
Note that it is now releatively easy to test feasibility of new keywords
like this:
$ isabelle build -n -a -d '$AFP' -k hidden -k local
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
