Email Gateway (Aug 19 2022 at 10:32): Email Gateway (Aug 19 2022 at 10:32):From: René Neumann <rene.neumann@in.tum.de>
Anyone an idea?
I now introduced an auxiliary locale:
locale Bar' = Bar +
fixes G (structure)
defines "G == s_G"
and will do all the work then in context Bar'.
But this looks hacky.
Email Gateway (Aug 19 2022 at 10:46):From: René Neumann <rene.neumann@in.tum.de>
Hi,
I have problems declaring something as "(structure)", when it is not a
locale parameter (Isabelle2012 is used). Take the following example:
definition adj :: "'a set ⇒ 'a ⇒ 'a ⇒ bool" ("_ →ı _" [100,100] 40) where "
adj G v w ≡ v ∈ G ∧ v = w"
locale Foo =
fixes G :: "'a set" (structure)
locale Bar =
fixes s :: "'a"
begin
definition "s_G = {s}"
end
sublocale Bar ⊆ Foo s_G by unfold_locales
In the context 'Bar' I'd like to use "v → w", but I can't as s_G is not
marked as an implicit structure. I then tried (in context Bar)
notation s_G (structure)
From reading the documentation, this should be legal, but it yields:
*** Bad mixfix declaration for "local.s_G"
I appreciate any useful hints to make s_G the implicit structure argument.
Thanks,
René
smime.p7s
Email Gateway (Aug 19 2022 at 10:55):From: Makarius <makarius@sketis.net>
The implicit structure notation is only available for locale parameters.
Can you point to the place in the documentation where it is suggested
otherwise? The only place I see in Isabelle2012 isar-ref is section 5.6.2
about the 'fixes' of locale declarations.
I can't say on the spot if it is feasible to make implicit structures more
general -- they have been a bit on retreat in recent years, and are now a
bit old-fashioned anyway.
Makarius
Email Gateway (Aug 19 2022 at 10:56):From: René Neumann <rene.neumann@in.tum.de>
Am 02.04.2013 16:55, schrieb Makarius:
On Thu, 14 Mar 2013, René Neumann wrote:
I have problems declaring something as "(structure)", when it is not a
locale parameter (Isabelle2012 is used). Take the following example:definition adj :: "'a set ⇒ 'a ⇒ 'a ⇒ bool" ("_ →ı _" [100,100] 40)
where "
adj G v w ≡ v ∈ G ∧ v = w"locale Foo =
fixes G :: "'a set" (structure)locale Bar =
fixes s :: "'a"
begin
definition "s_G = {s}"
endsublocale Bar ⊆ Foo s_G by unfold_locales
In the context 'Bar' I'd like to use "v → w", but I can't as s_G is not
marked as an implicit structure. I then tried (in context Bar)notation s_G (structure)
From reading the documentation, this should be legal, but it yields:
*** Bad mixfix declaration for "local.s_G"
I appreciate any useful hints to make s_G the implicit structure
argument.The implicit structure notation is only available for locale parameters.
Can you point to the place in the documentation where it is suggested
otherwise? The only place I see in Isabelle2012 isar-ref is section
5.6.2 about the 'fixes' of locale declarations.
Section 7.3: notation goes with a 'struct_mixfix'. (Ironically, the
nonterminal 'fixes' (p. 82) does not support "(structure)" according to
the diagram given).
I can't say on the spot if it is feasible to make implicit structures
more general -- they have been a bit on retreat in recent years, and are
now a bit old-fashioned anyway.
But there is no replacement, is there?
Email Gateway (Aug 19 2022 at 10:57):From: Makarius <makarius@sketis.net>
On Tue, 2 Apr 2013, René Neumann wrote:
Section 7.3: notation goes with a 'struct_mixfix'. (Ironically, the
nonterminal 'fixes' (p. 82) does not support "(structure)" according to
the diagram given).
The documentation is generally a bit terse, but note that formally a
syntax diagram is always an over approximation: not everything that is
syntactically correct is so semantically. The error means it is rejected
in the semantics -- there are also indirect situations where it is
rejected via low-level errors, IIRC.
I will look again if the confusion about "mixfix" and "struct_mixfix" in
the syntax can be removed, to make it just subject to semantic checking.
I can't say on the spot if it is feasible to make implicit structures
more general -- they have been a bit on retreat in recent years, and
are now a bit old-fashioned anyway.But there is no replacement, is there?
There is no one-to-one replacement. Indexed syntax was originally
introduced as a way to make global notation usable in a local context,
with dependency on locale parameters. Later local notation and
abbreviations were introduced, and despite some challenges, they are more
powerful. This is why "(structure)" has now this old-fashioned accent
when seen in theory sources.
Makarius
Last updated: Apr 25 2024 at 20:15 UTC