Re: [isabelle] "partial order" type?

Hi John,

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

here a short overview of the design space which combines everything said
on that here (@all: please comment if you think I've missed something)
with Isabelle folklore:

a) use (existing) type classes
  + lightweight
  + code can be generated directly
  - only one instantiation per type
  - no explicit carrier

b) use locales abstracting over the algebraic structure (which is
typically represented as a record)
  + explicit carrier
  + more flexible due to parametrisation
  - more involved in application
  - no direct code generation

c) use abstract type definition which encapsulates the properties of the
  + combines nicely with b) via interpretation
  + explicit carrier
  + code generation possible

Examples for a) can be found in the HOL standard theories, for b) in the
HOL-Algebra session.

For b) and c), the locale predicates for existing type classes can be
reused of course.

c) is quite a recent thought which I have not yet thought of thoroughly,
so I do not know about pitfalls etc.  It seems worth exploring.

Hope this helps,



PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

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