Re: [isabelle] No way to express duality?
05.01.2011, 17:02, "Victor Porton" <porton at 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?).
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 =
assumes "order<=base\<times>base" and "refl(base,order)" and "antisym(order)" and "trans(order)"
locale dual = poset "base" "converse(order)"
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?
This archive was generated by a fusion of
Pipermail (Mailman edition) and