[isabelle-dev] Binding with implicit rename

[Florian Haftmann]

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

After some internal discussion I have come to the conclusion that this
is actually a bad idea since then a theory would contain things which
are supposed to be used in user space but not referenced by explicit
text.  I think now the best solution is to have optional explicit names
given by the user.

	Florian

-- 

Home:
http://www.in.tum.de/~haftmann

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 262 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20101026/78adcac8/attachment.sig>