Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Exporting local setup to global context


view this post on Zulip Email Gateway (Jul 28 2020 at 14:12):

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

view this post on Zulip Email Gateway (Aug 03 2020 at 06:01):

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

view this post on Zulip Email Gateway (Aug 05 2020 at 09:50):

From: Lukas Stevens <lukas.stevens+isabelle-users@in.tum.de>
Thanks, that is what I needed :)


Last updated: Dec 05 2021 at 23:19 UTC