Email Gateway (Aug 19 2022 at 15:01): Email Gateway (Aug 19 2022 at 15:01):From: Lars Noschinski <noschinl@in.tum.de>
Hi,
I see that Named_Target.reinit is gone in 2014-rc0. It seems that it is
equivalent to leaving to a theory and then entering the target again.
What was its purpose and what is the right way to replace it?
It seems that it is sometimes necessary to perform these steps to get
the simpset updated after changing it in the background theory with
Local_Theory.background_theory_result.
Email Gateway (Aug 19 2022 at 15:02):From: Makarius <makarius@sketis.net>
On Wed, 23 Jul 2014, Lars Noschinski wrote:
I see that Named_Target.reinit is gone in 2014-rc0. It seems that it is
equivalent to leaving to a theory and then entering the target again.
What was its purpose and what is the right way to replace it?
This belongs to the system infrastructure -- user-space tools in
Isabelle/ML should not be affected by the change.
It seems that it is sometimes necessary to perform these steps to get
the simpset updated after changing it in the background theory with
Local_Theory.background_theory_result.
This sounds a bit odd, maybe some formerly global-theory tool that was
updated a bit too quickly, without really leaving the old ways behind.
Declarations with the "simp" attribute may be done like in Isar source,
using the ML antiquotation @{attributes [simp]} with Local_Theory.note,
for example. (Just hypersearch the sources for examples.)
If the simpset update is some other ML function, not an attribute, you may
use Simplifier.map_ss with Local_Theory.declaration, which also allows to
insist in a pervasive scope, such that the declaration affects the global
theory as well.
Makarius
Email Gateway (Aug 19 2022 at 15:02):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
This is a good opportunity to describe the rationale behind the local
theory / target / named target matter in more detail »as it is by now«.
The fundamental ideas have been presented in »Local Theory
Specifications in Isabelle/Isar« by Haftmann/Wenzel; as usual, the
implementation is a little bit more involved, and also some extensions
have appeared since then, notably nested target contexts and confined
interpretation.
What is a local theory? The extension of a proof context with an
abstract signature to allow definitional extensions (most prominently,
define and note – the actual interface can be found as *type
operations* in Pure/Isar/local_theory.ML).
A target is a particular implementation of the local theory signature.
The picture is a little complicated by the possibility to stack
arbitrary many auxiliary contexts on top a target (»context fixes …
assumes … begin … end« in Isar). However, these merely add variables and
assumptions in a canonical way; the target at the bottom of this stack,
the bottom target, is not really affected by this. So, if we speak
about target, we most times refer to a particular bottom target with a
(possibly empty) stack auf axuiliary contexts on top of it.
Conceptually, there are two main targets: the theory target and the
locale target, which can be seen as the most generic targets possible.
A slight variant of the locale target is the class target, which adds a
canonical interpretation on the theory level. An important class of
targets are theory-like targets, which behave almost like the theory
target, but feature slight modifications like additional syntax and a
consistency check before leaving the local theory. The overloading and
instantiation targets are prominent examples.
Concerning the concept of *named target. *Each type class and locale in
a theory can be referred to by a string s; if we identify the empty
string with the theory itself, Named_Target.init s opens a local theory
for the theory / locale / class with the appropriate theory / locale /
class target. This »selection by name« manifests in the Isar toplevel
also (»context s begin … end«), and hence the prominent status of these
named targets in the system infrastructure.
An important consequence of the abstract nature of local theories is
that only target implementations are allowed to break their abstraction;
client code is expected to operate on any kind of local theory
regardless of the particular (bottom) target. In the Isabelle
distribution, there are currently (Isabelle2014-RC0) four spots which
are candidates for a violation of this principle:
./Pure/Isar/class_declaration.ML:349: val proto_sub = case
Named_Target.class_of lthy of
./Pure/Isar/expression.ML:925: if Named_Target.is_theory lthy
./Pure/Isar/expression.ML:932: if Named_Target.is_theory lthy
./Tools/quickcheck.ML:365: val some_locale =
Named_Target.bottom_locale_of lthy;
The first one is sane since the class target is allowed to break its own
abstraction. Number two and three are similar. The last one is indeed a
little bit odd, but since its is some kind of diagnostic device, it is
maybe ok.
Generally, user space tools should refrain from using those
abstraction-breaking query operations in Named_Target. The same holds
for the Named_Target.switch (or its earlier predecessor,
Named_Target.reinit) which is a device to master the following situation
with an ad-hoc local theory switch which is currently allowed in Isar:
context s
begin
…
definition (in t):
…
…
end
If client code implements its own target, in most cases it will be a
theory-like target. There are two possibilites to approach it:
a) Something like
|> Local_Theory.init naming
{define = Generic_Target.define …,
notes = Generic_Target.notes Generic_Target.theory_notes,
abbrev = Generic_Target.abbrev Generic_Target.theory_abbrev,
declaration = K Generic_Target.theory_declaration,
subscription = Generic_Target.theory_registration,
pretty = …,
exit = … #> Local_Theory.target_of #> Sign.change_end_local}
(cf. Pure/Isar/class.ML) See how Generic_Target provides everything
needed to plug together implementations of local theory operations on
the spot.
b) If the target only adds a check or something similar before leaving
the local theory, it can also be setup using Named_Target.theory_like_init.
Hope this helps,
Florian
signature.asc
Last updated: Apr 24 2024 at 20:16 UTC