Add [parallel] to libary

Invariant.v

@@ -42,3 +42,41 @@ Proof.
   clear H1.
   induction H2; eauto.
 Qed.
+
+
+(** * General parallel composition *)
+
+Record threaded_state shared private := {
+  Shared : shared;
+  Private : private
+}.
+
+Inductive parallel1 shared private1 private2
+  (init1 : threaded_state shared private1 -> Prop)
+  (init2 : threaded_state shared private2 -> Prop)
+  : threaded_state shared (private1 * private2) -> Prop :=
+| Pinit : forall sh pr1 pr2,
+  init1 {| Shared := sh; Private := pr1 |}
+  -> init2 {| Shared := sh; Private := pr2 |}
+  -> parallel1 init1 init2 {| Shared := sh; Private := (pr1, pr2) |}.
+
+Inductive parallel2 shared private1 private2
+          (step1 : threaded_state shared private1 -> threaded_state shared private1 -> Prop)
+          (step2 : threaded_state shared private2 -> threaded_state shared private2 -> Prop)
+          : threaded_state shared (private1 * private2)
+            -> threaded_state shared (private1 * private2) -> Prop :=
+| Pstep1 : forall sh pr1 pr2 sh' pr1',
+  step1 {| Shared := sh; Private := pr1 |} {| Shared := sh'; Private := pr1' |}
+  -> parallel2 step1 step2 {| Shared := sh; Private := (pr1, pr2) |}
+               {| Shared := sh'; Private := (pr1', pr2) |}
+| Pstep2 : forall sh pr1 pr2 sh' pr2',
+  step2 {| Shared := sh; Private := pr2 |} {| Shared := sh'; Private := pr2' |}
+  -> parallel2 step1 step2 {| Shared := sh; Private := (pr1, pr2) |}
+               {| Shared := sh'; Private := (pr1, pr2') |}.
+
+Definition parallel shared private1 private2
+           (sys1 : trsys (threaded_state shared private1))
+           (sys2 : trsys (threaded_state shared private2)) := {|
+  Initial := parallel1 sys1.(Initial) sys2.(Initial);
+  Step := parallel2 sys1.(Step) sys2.(Step)
+|}.