[isabelle-dev] Binding with implicit rename

[Florian Haftmann]

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

-- 

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/20101007/053c4314/attachment.sig>