[isabelle-dev] Binding with implicit rename

[Alexander Krauss]

Florian Haftmann wrote:
> What I have to address is that
> you cannot be sure that a given name is already used, regardless how
> many prefices you add.

There is a bit more to this story:

Ideally, the internals of a package should be completely invisible 
unless a user explicitly chooses to look at them (eg. by looking at 
concealed facts), which is always at your own risk... Traditionally, 
packages made no real attempt at hiding their stuff, but the recent 
Binding.conceal efforts try to move towards this.

What Florian tries to avoid with "liberal bindings" is the following 
situation, which can be illustrated nicely using the function package:

   definition "f_graph = True"
   fun f where "f x = x"

*** Duplicate constant declaration "Scratch.f_graph" vs. "Scratch.f_graph"

But the symmetric situation would not be avoided by a liberal binding alone:

   fun f where "f x = x"
   definition "f_graph = True"
   (here we get a type error instead, by mere coincidence)

It would be nice if we could find a convention that avoids both kinds of 
errors. In principle, a combination "liberal + prefix" could do this... 
On the other hand, if I add the prefix "function_package_INTERNAL"¸ it 
is unlikely that a clash will ever occur in practice. So I am not sure 
if we really need a new concept...

Alex