[isabelle] No way to express duality?



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?).





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.