From: Lukas Stevens <lukas.stevens+isabelle-users@in.tum.de>
Hi,
I want to add the constants of a type class as terms to Generic_Data
inside the context of the class. This can be achieved using local_setup
(see the code below). Of course, the data inside the Generic_Data is
only present in the context of the class. What I want, however, is that
the data is also available in the global context with the associated
type of the type class being abstracted to a schematic type that has a
type class constraint. Apparently, this can be done using theorem
attributes (e.g. see src/HOL/Orderings.thy under the section "Reasoning
tools setup").
Is it possible to achieve the same effect without using theorem attributes?
Lukas
From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Lukas,
there is the Isar command »declaration« which makes a declaration out of
a snippet of Isabelle/ML code. The snippet is provided a morphism
argument which allows to adapt formal entities according to the
particular context situation.
However I don't see why attributes should not be apt for your particular
example.
Please don't hesitate to ask if this sounds only like abstract nonsense.
Cheers,
Florian
signature.asc
From: Lukas Stevens <lukas.stevens+isabelle-users@in.tum.de>
Thanks, that is what I needed :)
Last updated: Jan 04 2025 at 20:18 UTC