Re: [isabelle] Phantom locale notations



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

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.



> On 10 Sep 2021, at 6:04 pm, Peter Lammich <lammich at in.tum.de> wrote:
> 
> 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.