Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Phantom locale notations


view this post on Zulip 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?

view this post on Zulip 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:")

...

view this post on Zulip 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.

view this post on Zulip 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: Jul 15 2022 at 23:21 UTC