[isabelle] Phantom locale notations





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 ("♣")

end

locale big = pos + 
assumes
  x_big: ‹10 ≤ x›

begin

notation
half ("♠")

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?


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.