Re: [isabelle] Phantom locale notations



On 10/09/2021 03:03, 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.

I have stared at your examples for 10min, but did not see anything unusual.
Locale expressions lead to a certain canonical order of declarations, and
usually the last one "wins".

See the attached variant of your setup, where locale big_pos vs. pos_big
produce different output, due to change of the inclusion order.


We do have unclear situations concerning locale contexts, but here I think it
is right.


	Makarius
theory Scratch
  imports Main
begin

locale pos =
  fixes x :: int
  assumes x_pos: \<open>0 \<le> x\<close>
begin

abbreviation \<open>half \<equiv> x div 2\<close>

notation half ("\<clubsuit>")
term "half" \<comment>\<open>result: "\<clubsuit>"\<close>

end

locale big = pos + 
  assumes x_big: \<open>10 \<le> x\<close>
begin

notation half ("\<spadesuit>")
term "half" \<comment>\<open>result: "\<spadesuit>"\<close> 

end

locale pos_big = big + Y: pos y for y
begin

term "half" \<comment>\<open>result: "\<clubsuit>"\<close>

end

locale big_pos = Y: pos y + big for y
begin

term "half" \<comment>\<open>result: "\<spadesuit>"\<close>

end

end


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