(* 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)
apply (simp_all add: ext_is_act ext1_ext2_is_not_act1)
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)
apply (simp_all add: ext_is_act ext1_ext2_is_not_act1)
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 (simp add: is_asig_of_def)
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 (simp add: compositionality_tr)
apply (subgoal_tac
"ext A1 = ext A2 \ ext B1 = ext B2")
prefer 2
apply (simp add: externals_def)
apply (erule conjE)+
text ‹rewrite
with proven subgoal
›
apply (simp add: externals_of_par)
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
apply (simp add: Filter_actAisFilter_extA)
text ‹2:
‹Filter B2 x
∈ traces B2
››
apply (drule_tac A =
"traces B1" in subsetD)
apply assumption
apply (simp add: Filter_actAisFilter_extA2)
done
end
