*To*: isabelle-users at cl.cam.ac.uk*Subject*: [isabelle] Phantom locale notations*From*: mahonybp at tpg.com.au*Date*: Fri, 10 Sep 2021 10:33:43 +0930*Authentication-results*: cam.ac.uk; iprev=pass (mta0.cl.cam.ac.uk) smtp.remote-ip=128.232.25.20; spf=softfail smtp.mailfrom=tpg.com.au; arc=none*Authentication-results*: cam.ac.uk; iprev=pass (web-atmail1.tpgi.com.au) smtp.remote-ip=203.12.160.53; spf=pass smtp.mailfrom=tpg.com.au; arc=none

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

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

- Previous by Date: Re: [isabelle] Superscript argument to a function
- Next by Date: Re: [isabelle] Phantom locale notations
- Previous by Thread: [isabelle] 30 months postdoctoral research position at University of Sheffield involving proof-assistant-based verification -- application deadline 23 Sept. 2021
- Next by Thread: Re: [isabelle] Phantom locale notations
- 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