(*T* \usection{System Composition}\label{sect-union} *T*)

(*T* The elementary compositionality results formalized in the module
|composition| to be discussed next can be used to achieve a certain
degree of modularity and reusability in system verification. This is
in particular of interest for large systems which either can be
decomposed into meaningful subsystems and/or are build anyway from
(reusable) components. Compositional verification means that in order
to prove a system property we rely on the specifications of its
components, abstracting from their internal structure as far as
possible.  The assumption that a component satisfies a specification
may again be verified by a temporal logic proof, but may also be
confirmed by other formal or informal methods as it is often the case
in practice. *T*)

(*T* As we have already explained before, we are working in the
context of a single transition system which represents the entire
system, and we regard components of this system as particular views.
The natural composition operation then becomes a simple union of these
views, i.e. a union of sets.  A distinguishing feature of a
UNITY-style temporal logic is that almost all of its operators enjoy
elementary compositionality properties which are presented in this
section. *T*)

Theorem co_union : (E,E':view)(p,q:s_prop)
  (co E p q) -> (co E' p q) -> 
  (co (Union act E E') p q).

Intros.
Apply sc_co.
Intros.
Generalize (nc_co E p q H).
Intros.
Generalize (nc_co E' p q H0).
Intros.
Unfold Union act in H1.
Generalize H2.
Clear H2.
Elim H1.
Intros.
Apply (H4 x s s' H2 H6).
Trivial.

Intros.
Apply (H5 x s s' H2 H6).
Trivial.
Qed.

Theorem stable_union : (E,E':view)(p:s_prop)
  (stable E p) -> (stable E' p) -> 
  (stable (Union act E E') p).

Unfold stable.
Intros.
Apply co_union.
Trivial.
Trivial.
Qed.

Theorem indinv_stable_union : 
  (E,E':view)(IC:s_prop)(p:s_prop)
  (ind_invariant E IC p) -> (stable E' p) -> 
  (ind_invariant (Union act E E') IC p).

Unfold ind_invariant.
Intros.
Elim H.
Clear H.
Intros.
Split.
Trivial.
Apply stable_union.
Trivial.
Trivial.
Qed.

Theorem stable_indinv_union : 
  (E,E':view)(IC:s_prop)(p:s_prop)
  (stable E' p) -> (ind_invariant E IC p) -> 
  (ind_invariant (Union act E E') IC p).

Unfold ind_invariant.
Intros.
Elim H0.
Clear H0.
Intros.
Split.
Trivial.
Apply stable_union.
Trivial.
Trivial.
Qed.

Theorem unless_union : (E,E':view)(p,q:s_prop)
  (unless E p q) -> (unless E' p q) -> 
  (unless (Union act E E') p q).

Unfold unless.
Intros.
Apply co_union.
Trivial.
Trivial.
Qed.

Theorem unless_stable_union : (E,E':view)(p,q:s_prop)
  (unless E p q) -> (stable E' p) -> 
  (unless (Union act E E') p q).

Intros.
Apply unless_union.
Trivial.
Apply stable_imp_unless.
Trivial.
Qed.

Theorem en_union_r : (E,E':view)(p:s_prop)
  (en E' p) -> (en (Union act E E') p).

Unfold en.
Unfold Union act.
Intros.
Unfold everywhere s_imp.
Unfold everywhere s_imp in H.
Intros.
Elim (H s H0).
Intro t.
Intros.
Split with t.
Elim H1.
Clear H1.
Intros.
Split.
Auto with v62.

Trivial.
Qed.


Theorem co_sco_union : (E,E':view)(p,q:s_prop)
  (co E p q) -> (sco E' p q) -> 
  (sco (Union act E E') p q).

Unfold sco.
Intros.
Split.
Elim H0.
Intros.
Apply en_union_r.

Trivial.

Apply co_union.
Trivial.

Elim H0.
Auto.
Qed.

Theorem transient_union_r : (E,E':view)(p:s_prop)
  (transient E' p) ->
  (transient (Union act E E') p).

Unfold transient.
Intros.
Elim H.
Clear H.
Intro E'0.
Intros.
Split with E'0.
Elim H.
Clear H.
Intros.
Elim H0.
Clear H0.
Intros.
Split.
Trivial.

Split.
Unfold Union act.
Auto with v62.

Trivial.
Qed.

Theorem transient_union : (E,E':view)(p:s_prop)
  ((transient E p) \/ (transient E' p)) ->
  (transient (Union act E E') p).

Unfold transient.
Intros.
Elim H.
Clear H.
Intros.
Elim H.
Clear H.
Intros.
Elim H.
Clear H.
Intros.
Split with x.
Split.
Trivial.

Split.
Elim H0.
Intros.
Unfold Union act.
Auto with v62.

Elim H0.
Auto.

Clear H.
Intros.
Elim H.
Clear H.
Intros.
Elim H.
Clear H.
Intros.
Split with x.
Split.
Trivial.

Split.
Elim H0.
Intros.
Unfold Union act.
Auto with v62.

Elim H0.
Auto.
Qed.


Theorem ensures_unless_union : (E,E':view)(p,q:s_prop)
  (ensures E p q) -> (unless E' p q) -> 
  (ensures (Union act E E') p q).

Unfold ensures.
Intros.
Elim H.
Intros.
Split.
Apply unless_union.
Trivial.
Trivial.
Apply transient_union.
Left .
Trivial.
Qed.

Theorem unless_ensures_union : (E,E':view)(p,q:s_prop)
  (unless E p q) -> (ensures E' p q) -> 
  (ensures (Union act E E') p q).

Unfold ensures.
Intros.
Elim H0.
Intros.
Split.
Apply unless_union.
Trivial.
Trivial.
Apply transient_union.
Right .
Trivial.
Qed.

Theorem ensures_stable_union : (E,E':view)(p,q:s_prop)
  (ensures E p q) -> (stable E' p) -> 
  (ensures (Union act E E') p q).

Intros.
Apply ensures_unless_union.
Trivial.
Apply stable_imp_unless.
Trivial.
Qed.

Theorem stable_ensures_union : (E,E':view)(p,q:s_prop)
  (stable E p) -> (ensures E' p q) -> 
  (ensures (Union act E E') p q).

Intros.
Apply unless_ensures_union.
Apply stable_imp_unless.
Trivial.
Trivial.
Qed.

(*T* These proof rules support compositional reasoning with component
specifications involving |co|, |unless|, |stable|, |ind_invariant|,
|transient| and |ensures|. It is remarkable that the only operators
which do not enjoy composition rules similar to those above are
|invariant| and |leads_to|. *T*)

(*T* Clearly, the lack of simple compositionality rules for |leads_to|
is unsatisfying, but for {\em tightly coupled systems} with an
unrestricted notion of composition, as we use it here, we cannot
expect a rule similar to |ensures_union| due to the possible interference
between components. We will return to this issue in Section
\ref{sect-comp}, where we derive a formal compositionality theorem for
so-called informative |leads_to| assertions that in some sense can be
regarded as the least restrictive compositionality rule of this kind.
*T*)

(*T* Compositional verification of {\em loosely coupled systems},
i.e. systems which are interacting in a well-defined and typically
restricted way, is beyond the scope of this thesis, but we think that
the verification library can be extended by more restricted
composition rules.  As shown in \cite{ColleteKnapp97} and
\cite{CarpentierChandy1999} there are possibilities of compositional
reasoning with |leads_to| in a rely-gurantee style. Conditional
assertions, which can be easily expressed as implications in the
metalogic, are a natural starting point to support such kind of
reasoning without modifying the temporal logic itself. In fact,
\cite{CarpentierChandy1999} uses conditional assertions of a
particular kind, which is why we consider a formalization of this
approach in our general setting of labeled transition systems as an
natural future extension of our temporal logic library.  *T*)