Re: [isabelle] No way to express duality?

05.01.2011, 17:02, "Victor Porton" <porton at>:
> 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 =
  fixes base::i
  fixes order::i
  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 MHonArc.