*To*: Isabelle <isabelle-users at cl.cam.ac.uk>*Subject*: Re: [isabelle] Phantom locale notations*From*: "Dr. Brendan Patrick Mahony" <mahonybp at tpg.com.au>*Date*: Fri, 10 Sep 2021 22:52:51 +0930*Authentication-results*: cam.ac.uk; iprev=pass (mta2.cl.cam.ac.uk) smtp.remote-ip=128.232.25.22; spf=softfail smtp.mailfrom=tpg.com.au; dkim=pass header.d=tpg.com.au header.s=alpha header.a=rsa-sha256; arc=none*Authentication-results*: cam.ac.uk; iprev=pass (rpt-glb-mail03.tpgi.com.au) smtp.remote-ip=60.241.0.28; spf=pass smtp.mailfrom=tpg.com.au; dkim=pass header.d=tpg.com.au header.s=alpha header.a=rsa-sha256; arc=none*Cc*: Peter Lammich <lammich at in.tum.de>*In-reply-to*: <b9e336730a0beb2e9d9867dbbe6e4e4d0bbddb3d.camel@in.tum.de>*References*: <5edeae7bcb0c3f772f7e738339211900063c8525@new-postoffice.tpg.com.au> <b9e336730a0beb2e9d9867dbbe6e4e4d0bbddb3d.camel@in.tum.de>

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? > >

**References**:**[isabelle] Phantom locale notations***From:*mahonybp

**Re: [isabelle] Phantom locale notations***From:*Peter Lammich

- Previous by Date: [isabelle] EuroProofNet - Call for Working Group membership Application
- Next by Date: Re: [isabelle] Using the Parallel library
- Previous by Thread: Re: [isabelle] Phantom locale notations
- Next by Thread: Re: [isabelle] Using the Parallel library
- Cl-isabelle-users September 2021 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list