Re: [isabelle] Phantom locale notations



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

...


--
  Peter

On Fri, 2021-09-10 at 10:33 +0930, mahonybp at tpg.com.au wrote:
> 
> 
> 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.