# Theory Compositionality

Up to index of Isabelle/HOLCF/IOA

theory Compositionality
imports CompoTraces
uses [Compositionality.ML]
begin

    (*  Title:      HOLCF/IOA/meta_theory/Compositionality.thy
        ID:         $Id: Compositionality.thy,v 1.6 2005/09/02 15:24:01 wenzelm Exp $
        Author:     Olaf Müller
    *)

    header {* Compositionality of I/O automata *}
    theory Compositionality
    imports CompoTraces
    begin

    end

theorem compatibility_consequence3:

      [| eA --> A; eB ∧ ¬ eA --> ¬ A |] ==> eA ∨ eB --> A = eA

theorem Filter_actAisFilter_extA:

      [| compatible A B; Forall (%a. a ∈ ext A ∨ a ∈ ext B) tr |]
      ==> Filter (%a. a ∈ act A)·tr = Filter (%a. a ∈ ext A)·tr

theorem compatibility_consequence4:

      [| eA --> A; eB ∧ ¬ eA --> ¬ A |] ==> eB ∨ eA --> A = eA

theorem Filter_actAisFilter_extA2:

      [| compatible A B; Forall (%a. a ∈ ext B ∨ a ∈ ext A) tr |]
      ==> Filter (%a. a ∈ act A)·tr = Filter (%a. a ∈ ext A)·tr

## Main Compositionality Theorem

theorem compositionality:

      [| is_trans_of A1.0; is_trans_of A2.0; is_trans_of B1.0; is_trans_of B2.0;
         is_asig_of A1.0; is_asig_of A2.0; is_asig_of B1.0; is_asig_of B2.0;
         compatible A1.0 B1.0; compatible A2.0 B2.0; A1.0 =<| A2.0; B1.0 =<| B2.0 |]
      ==> (A1.0 || B1.0) =<| (A2.0 || B2.0)