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



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.