[isabelle] "partial order" type?


I want to write a function that takes a partial-order as a parameter. Specifically, I want the following function...

fun interleave :: "'a list => 'a list => 'a partialorder => 'a list set"

... which takes two lists and a partialorder, and returns the set of all interleavings of the elements of those lists which respect the partial order.

I know that I could replace "'a partialorder" above with "('a \<times> 'a) set", and then prove a lemma saying "if that parameter is a partial-order then interleave has such-and-such a property". But it would be rather nice just to put the partial-order-ness of that parameter straight into its type. Can I do that, and if so how?

Thanks very much,

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