[isabelle-dev] Binding with implicit rename

[Christian Sternagel]

Hi Florian,

you are right, I was thinking more from a user perspective, whereas your 
point is on the package developer side. Sorry, for my misinterpretation.

What I meant is that as a user, you can be sure that names that are 
automatically generated by packages (assuming that they use binding 
prefixes and respect each others naming conventions) are different from 
whatever name you could invent. (Is that true? Excluding Isabelle/ML.)

Only as a package developer, you have to make sure that whatever names 
you invent, are not used by other packages. For this purpose, I think 
your "liberal" flag makes perfect sense. As long as the user does not 
have to care about it at all.

Assuming I give some inductive definition:

inductive foo :: "..." where
   "..." |
   "..."

Then, as a user, I count on the name "foo.intros" and it would not be 
nice to get some variant, just because "inductive" marked its generated 
names as "liberal". I think, what I'm trying to say, is that package 
authors should be careful in cases where they produce names that are 
visible to the user. But that's a truism anyway ;)

cheers

chris

On 10/08/2010 09:18 AM, Florian Haftmann wrote:
> Hi Christian,
>
>> to me the liberal flag seems rather ad-hoc. Wouldn't a proper
>> hierarchical naming solve this problem (maybe by introducing an
>> automatic "sub-module" Internal/Auto/Whatever for any theory T, such
>> that automatic names may be referred to by using
>> T.Whatever.automatic_name).
>
> we *have* already the concept of binding prefices (what you refer to
> here as hierarchical naming), although the theory name part of the
> prefix currently is always a singleton.  What I have to address is that
> you cannot be sure that a given name is already used, regardless how
> many prefices you add.
>
> Cheers,
> 	Florian
>