# Theory Compositionality

theory Compositionality
imports CompoTraces
```(*  Title:      HOL/HOLCF/IOA/Compositionality.thy
Author:     Olaf MÃ¼ller
*)

section ‹Compositionality of I/O automata›
theory Compositionality
imports CompoTraces
begin

lemma compatibility_consequence3: "eA ⟶ A ⟹ eB ∧ ¬ eA ⟶ ¬ A ⟹ (eA ∨ eB) ⟶ A = eA"
by auto

lemma 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"
apply (rule ForallPFilterQR)
text ‹i.e.: ‹(∀x. P x ⟶ (Q x = R x)) ⟹ Forall P tr ⟹ Filter Q ⋅ tr = Filter R ⋅ tr››
prefer 2 apply assumption
apply (rule compatibility_consequence3)
done

text ‹
The next two theorems are only necessary, as there is no theorem
‹ext (A ∥ B) = ext (B ∥ A)›
›

lemma compatibility_consequence4: "eA ⟶ A ⟹ eB ∧ ¬ eA ⟶ ¬ A ⟹ (eB ∨ eA) ⟶ A = eA"
by auto

lemma 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"
apply (rule ForallPFilterQR)
prefer 2 apply (assumption)
apply (rule compatibility_consequence4)
done

subsection ‹Main Compositionality Theorem›

lemma compositionality:
assumes "is_trans_of A1" and "is_trans_of A2"
and "is_trans_of B1" and "is_trans_of B2"
and "is_asig_of A1" and "is_asig_of A2"
and "is_asig_of B1" and "is_asig_of B2"
and "compatible A1 B1" and "compatible A2 B2"
and "A1 =<| A2" and "B1 =<| B2"
shows "(A1 ∥ B1) =<| (A2 ∥ B2)"
apply (insert assms)
apply (frule_tac A1 = "A1" in compat_commute [THEN iffD1])
apply (frule_tac A1 = "A2" in compat_commute [THEN iffD1])
apply (simp add: ioa_implements_def inputs_of_par outputs_of_par externals_of_par)
apply auto
apply (subgoal_tac "ext A1 = ext A2 ∧ ext B1 = ext B2")
prefer 2
apply (erule conjE)+
text ‹rewrite with proven subgoal›
apply auto
text ‹2 goals, the 3rd has been solved automatically›
text ‹1: ‹Filter A2 x ∈ traces A2››
apply (drule_tac A = "traces A1" in subsetD)
apply assumption