[isabelle-dev] Binding with implicit rename

[Christian Sternagel]

Hi Florian,

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

Admittedly, after reading once more through the above paragraph, my own 
suggestion seems rather ad-hoc ... Nevertheless, maybe it gives rise to 
discussion ;)

cheers

chris


On 10/07/2010 09:23 AM, Florian Haftmann wrote:
> Typically, bindings are created by the user in the theory text and
> passed down from there, e.g.
>
>    specification (definition) foo :: T
>    where
>      "P foo"
>
> creates a @{binding foo}.
>
> However in packages often also bindings are created automatically.
> Currently I am working on some fragements of a mechanism which analyzes
> parts of a theory (most prominently constants and theorems) and
> generated new constants and theorems from them.  The result, in
> particular the new constants, are highly unpredictable, and the user is
> not really interested in the number or names of the new constants.  The
> situation is somehow similar to the predicate compiler, but even less
> tamed.  To ensure that the new constants do not clash with existing
> ones, the bindings for them have to be distilled carefully and a rather
> unsatisfactory way.  I am asking myself whether this could be
> dramatically simplified by giving bindings a »liberal« flag:  this could
> be set e.g. using a function Binding.liberal :: binding ->  binding; on
> declaration in a namespace, the basename of a liberal binding would be
> modified if it would clash with an existing declaration.  User-space
> binding would stay non-liberal an issue an error on clashing.
>
> I think such a liberal binding mechanism would be helpful for all kind
> of tools which provide automatic, rather unpredictable theory extensions.
>
> Any opinions?
>
>      Florian
>
>
>
>
> _______________________________________________
> Isabelle-dev mailing list
> Isabelle-dev at mailbroy.informatik.tu-muenchen.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev