Email Gateway (Sep 10 2021 at 01:04): Email Gateway (Sep 10 2021 at 01:04):From: mahonybp@tpg.com.au
As usual, sorry, if this is a double up, but I did search through the
list for related posts without success.
I have been a bit frustrated recently by phantom locale notations
making my proof states impossible to read.
It seems to come up in locale hierarchies where the notation for
abbreviations is changed to reflect strengthened defining properties.
This is a simple example:
locale pos =
fixes
x :: int
assumes
x_pos: ‹0 ≤ x›
begin
abbreviation
‹half ≡ x div 2›
notation
half (":clubs:")
end
locale big = pos +
assumes
x_big: ‹10 ≤ x›
begin
notation
half (":spades:")
end
locale pos_big =
big +
Y: pos y
for
y
begin
term "half" ―‹result: "♣"›
end
It seems that the locale expression is including the pos notation for
half (rather than Y.half) and it is overriding the big notation for
half!
If I reverse the order of inclusion this changes.
locale big_pos =
Y: pos y +
big
for
y
begin
term "half" ―‹result: "♠"›
end
This is often a viable a work around, but not always. For example if I
have a local interpretation in the locale the same phenomena occurs.
I am tempted to see this as a bug, rather than a feature.
Anyone else had this problem? Work arounds?
Email Gateway (Sep 10 2021 at 08:34):From: Peter Lammich <lammich@in.tum.de>
Hi,
not sure if I would see this behaviour as error. What would be the
default policy for conflicting notations?
Note, however, that there is an easy 'fix', by strategically inserting
a no_notation:
locale pos_big =
big +
Y: pos y
for
y
begin
no_notation half (":clubs:")
...
Email Gateway (Sep 10 2021 at 13:23):From: "Dr. Brendan Patrick Mahony" <mahonybp@tpg.com.au>
I would point out that “Y: pos y" does not have a half abbreviation only a Y.half. It is adding a notation for the half from “big”. This not a “conflicting” notation.
This is not even due to some form of inheritance conflict, for example:
locale pos2 =
fixes
x :: "int"
begin
abbreviation
‹half ≡ x div 2›
notation
half (":spades:")
end
locale pos2_pos =
pos2 +
Y: pos y
for
y
begin
term "half" ―‹result: "♣"›
end
I would submit the suggested “fix” is simply another manifestation of the odd behaviour.
In any case it does not sort the problem when manifested by an interpretation in a proof environment, which is where my patience wore down enough to make the post.
Email Gateway (Oct 04 2021 at 13:43):From: Makarius <makarius@sketis.net>
I have stared at your examples for 10min, but did not see anything unusual.
Locale expressions lead to a certain canonical order of declarations, and
usually the last one "wins".
See the attached variant of your setup, where locale big_pos vs. pos_big
produce different output, due to change of the inclusion order.
We do have unclear situations concerning locale contexts, but here I think it
is right.
Makarius
Scratch.thy
Last updated: Jan 04 2025 at 20:18 UTC