Email Gateway (Aug 22 2022 at 19:01): Email Gateway (Aug 22 2022 at 19:01):From: Peter Lammich <lammich@in.tum.de>
Hi all,
I have a command that takes a definition theorem of the form (f x1 ...
xn = t). It then has to define some auxiliary constants f_1 ... f_n,
and generate a new theorem f x1 ... xn = t', where t' contains the
auxiliary constants.
I'm using Specification.definition to define the auxiliary constants,
but I do not see how to get "safe" names for them, i.e., names derived
from "f" that do not clash with any existing constant.
A standard approach would be to use Name.variant, but for that I would
need to obtain all existing names. I do not know how.
Thanks for any pointers,
Peter
Email Gateway (Aug 22 2022 at 19:02):From: Makarius <makarius@sketis.net>
On 31/01/2019 14:52, Peter Lammich wrote:
I have a command that takes a definition theorem of the form (f x1 ...
xn = t). It then has to define some auxiliary constants f_1 ... f_n,
and generate a new theorem f x1 ... xn = t', where t' contains the
auxiliary constants.I'm using Specification.definition to define the auxiliary constants,
but I do not see how to get "safe" names for them, i.e., names derived
from "f" that do not clash with any existing constant.
The standard programming interface is Local_Theory.define -- it is more
robust and easier to use.
A standard approach would be to use Name.variant, but for that I would
need to obtain all existing names. I do not know how.
In such situations I usually invent funny names like this (see
src/Pure/Isar/experiment.ML):
val experiment_name = Binding.name ("experiment" ^ serial_string ())
|> Binding.concealed;
There can be still clashes, but they hardly ever happen in practice --
and there will be a clear error when it happens.
Makarius
Last updated: Apr 19 2024 at 01:05 UTC