Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Feature suggestion: locales inside locales

Email Gateway (Aug 18 2022 at 16:53):

From: Victor Porton <porton@narod.ru>
The following does not verify. Accepting things like below would be useful. Please take this feature suggestion for Isabelle.

theory MyOrder
imports Main_ZF
begin

locale poset =
fixes base::i
fixes order::i
assumes "order<=base×base" and "refl(base,order)" and "antisym(order)" and "trans(order)"

locale strict_poset =
fixes base::i
fixes strict_order::i
assumes "strict_order<=base×base" and "irrefl(base,strict_order)" and "antisym(strict_order)" and "trans(strict_order)"

context poset
begin
locale strict = poset "base" "order - id(base)"
end

end

Last updated: Apr 26 2024 at 12:28 UTC