Re: [isabelle] Importing classes into a locale in Isabelle and other related questions



Dear Dr Akihisa Yamada,

Thank you for your reply. It seems that the solution that you have proposed
may be the best solution that is currently available because it was used in
HOL on several occasions. Anecdotally, it is possible that someone else has
struggled with the same problem - theory Dense_Linear_Order in the folder
HOL/Decision_Procs/ contains the following code:

--------------------------------------------------------
locale *linorder_stupid_syntax* = linorder
begin

notation
  less_eq  ("op ⊑") and
  less_eq  ("(_/ ⊑ _)" [51, 51] 50) and
  less  ("op ⊏") and
  less  ("(_/ ⊏ _)"  [51, 51] 50)

end
--------------------------------------------------------

I have to admit that I thought that the problem is likely to be related to
notation before asking the question. However, I became slightly confused
after reading clause 5 in the following question:
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2014-August/msg00237.html.
After reading clause 5 in the aforementioned question I thought that the
problem may not have a trivial solution and decided to postpone the
independent investigation until I receive a reply from the community.

If possible, I would like to provide a copy of your reply on stack
overflow. Please let me know if this is acceptable (of course, I will
provide a link to your original answer). Alternatively, please let me know
if you would prefer to provide an answer on stack overflow yourself or you
would prefer your answer not to be copied to stack overflow.

xanonec


On Tue, May 8, 2018 at 1:32 PM, Akihisa Yamada <
ayamada at trs.cm.is.nagoya-u.ac.jp> wrote:

> Dear xanonec,
>
> let me comment to your technical questions as I also tackled the same goal
> as you. I'll be happy if there's a better solution, though.
>
> lemma (in my_locale) property_locale: "⟦ x ≤ y; y ≤ z ⟧ ⟹ x ≤ z"
>>   by nitpick
>>
>
> Interpreting a class as a locale doesn't seem to import notations, so here
> "≤" refers to the global one for "ord", which assumes nothing (you can
> check by ctrl+hover on x etc.).
>
> My solution is to define a locale for syntax and interpret it (sublocale
> is somehow slow) whenever you want to use the syntax.
>
> locale ord_syntax = ord
> begin
>
> notation less_eq (infix "⊑" 50)
> notation less (infix "⊏" 50)
> abbreviation greater_eq_syntax (infix "⊒" 50) where "greater_eq_syntax ≡
> ord.greater_eq less_eq"
> abbreviation greater_syntax (infix "⊐" 50) where "greater_syntax ≡
> ord.greater less"
>
> end
>
> context my_locale begin
> interpretation ord_syntax.
> lemma property_locale: "⟦ x ⊑ y; y ⊑ z ⟧ ⟹ x ⊑ z" using
> less_eq.order_trans.
> end
>
> Best regards,
> Akihisa
>
>
>



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