Re: [isabelle] Importing classes into a locale in Isabelle and other related questions
- To: xanonec xyz <xanonec at gmail.com>, cl-isabelle-users at lists.cam.ac.uk
- Subject: Re: [isabelle] Importing classes into a locale in Isabelle and other related questions
- From: Akihisa Yamada <ayamada at trs.cm.is.nagoya-u.ac.jp>
- Date: Tue, 8 May 2018 19:32:34 +0900
- In-reply-to: <CAGDqzRHw_UcDh+8wVjJipeT==g3JE_cx1CgS+YgV-7XOJ6J_2g@mail.gmail.com>
- References: <CAGDqzRHw_UcDh+8wVjJipeT==g3JE_cx1CgS+YgV-7XOJ6J_2g@mail.gmail.com>
- User-agent: Mozilla/5.0 (Windows NT 10.0; WOW64; rv:45.0) Gecko/20100101 Thunderbird/45.8.0
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"
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
notation less_eq (infix "⊑" 50)
notation less (infix "⊏" 50)
abbreviation greater_eq_syntax (infix "⊒" 50) where "greater_eq_syntax ≡
abbreviation greater_syntax (infix "⊐" 50) where "greater_syntax ≡
context my_locale begin
lemma property_locale: "⟦ x ⊑ y; y ⊑ z ⟧ ⟹ x ⊑ z" using less_eq.order_trans.
This archive was generated by a fusion of
Pipermail (Mailman edition) and