Email Gateway (Aug 18 2022 at 16:53): Email Gateway (Aug 18 2022 at 16:53):From: Victor Porton <porton@narod.ru>
AFAIK, in Isabelle 2009-2 there is no way to express duality of (for example) poset or lattice in terms of locales.
Let we have:
locale poset =
fixes base::i
fixes order::i
assumes "order<=base\<times>base" and "refl(base,order)" and "antisym(order)" and "trans(order)"
How to express the dual poset?
I think, this is should be main issue on the way to Isabelle 2010 (or 2011?).
Email Gateway (Aug 18 2022 at 16:54):From: Victor Porton <porton@narod.ru>
Earlier I suggested the feature to allow to have locales defined inside locales.
I think this would solve the problem that I cannot define the dual order in a reasonable way:
locale poset =
fixes base::i
fixes order::i
assumes "order<=base\<times>base" and "refl(base,order)" and "antisym(order)" and "trans(order)"
begin
locale dual = poset "base" "converse(order)"
end
Note that this leads to infinite chains of nested locales such that order.dual.dual.dual.dual. But I think this should not be a problem.
Hey, Isabelle developers, do you take my suggestion?
Are there other ideas how we could consider a dual poset in terms of locales?
Last updated: Apr 25 2024 at 20:15 UTC