Basic general pomset theory

[eupp]

• Define pomset L structure --- labeled partial order with L being the label set. That is a partial order over carrier Tplus labeling function lab : T -> L

• Make subclass of Elem.eventStruct --- elementary event structure, which is a pomset plus axiom of finite cause (move it to prime_eventstruct.v.

• Define homomorphism of pomsets.

• Define isomorphism of pomsets.

• Make subclass of finitely supported pomset.
  {fsfun lab with dfl -> \bot} where \bot : L is distinguished label (use inhType ?).
  Require that forall e1, e2 \in supp lab. e1 < e2 is false (i.e. strict causality is false outside the finite support).

• Define pomset languages.
  There are two ways:
  (1) using quotient types
  (2) as Prop-predicate invariant under isomorphisms: P : lposet E L -> Prop s.t. forall p q, p ~= q -> P p -> P q.

• Define embedding relation of pomset languages. Prove trivial properties (preorder).

• Define ordinary word language corresponding to pomset.
  This should work only for finite pomsets? The type should be lang: fslposet E L -> seq L -> bool ?.
  Prove embedding lemma: (p ~> q) -> lang q ≦ lang p

[eupp]

I've partly addressed this in #116