1(*  Title:      HOL/HOLCF/IOA/Compositionality.thy
2    Author:     Olaf M��ller
3*)
4
5section \<open>Compositionality of I/O automata\<close>
6theory Compositionality
7imports CompoTraces
8begin
9
10lemma compatibility_consequence3: "eA \<longrightarrow> A \<Longrightarrow> eB \<and> \<not> eA \<longrightarrow> \<not> A \<Longrightarrow> (eA \<or> eB) \<longrightarrow> A = eA"
11  by auto
12
13lemma Filter_actAisFilter_extA:
14  "compatible A B \<Longrightarrow> Forall (\<lambda>a. a \<in> ext A \<or> a \<in> ext B) tr \<Longrightarrow>
15    Filter (\<lambda>a. a \<in> act A) \<cdot> tr = Filter (\<lambda>a. a \<in> ext A) \<cdot> tr"
16  apply (rule ForallPFilterQR)
17  text \<open>i.e.: \<open>(\<forall>x. P x \<longrightarrow> (Q x = R x)) \<Longrightarrow> Forall P tr \<Longrightarrow> Filter Q \<cdot> tr = Filter R \<cdot> tr\<close>\<close>
18  prefer 2 apply assumption
19  apply (rule compatibility_consequence3)
20  apply (simp_all add: ext_is_act ext1_ext2_is_not_act1)
21  done
22
23
24text \<open>
25  The next two theorems are only necessary, as there is no theorem
26  \<open>ext (A \<parallel> B) = ext (B \<parallel> A)\<close>
27\<close>
28
29lemma compatibility_consequence4: "eA \<longrightarrow> A \<Longrightarrow> eB \<and> \<not> eA \<longrightarrow> \<not> A \<Longrightarrow> (eB \<or> eA) \<longrightarrow> A = eA"
30  by auto
31
32lemma Filter_actAisFilter_extA2:
33  "compatible A B \<Longrightarrow> Forall (\<lambda>a. a \<in> ext B \<or> a \<in> ext A) tr \<Longrightarrow>
34    Filter (\<lambda>a. a \<in> act A) \<cdot> tr = Filter (\<lambda>a. a \<in> ext A) \<cdot> tr"
35  apply (rule ForallPFilterQR)
36  prefer 2 apply (assumption)
37  apply (rule compatibility_consequence4)
38  apply (simp_all add: ext_is_act ext1_ext2_is_not_act1)
39  done
40
41
42subsection \<open>Main Compositionality Theorem\<close>
43
44lemma compositionality:
45  assumes "is_trans_of A1" and "is_trans_of A2"
46    and "is_trans_of B1" and "is_trans_of B2"
47    and "is_asig_of A1" and "is_asig_of A2"
48    and "is_asig_of B1" and "is_asig_of B2"
49    and "compatible A1 B1" and "compatible A2 B2"
50    and "A1 =<| A2" and "B1 =<| B2"
51  shows "(A1 \<parallel> B1) =<| (A2 \<parallel> B2)"
52  apply (insert assms)
53  apply (simp add: is_asig_of_def)
54  apply (frule_tac A1 = "A1" in compat_commute [THEN iffD1])
55  apply (frule_tac A1 = "A2" in compat_commute [THEN iffD1])
56  apply (simp add: ioa_implements_def inputs_of_par outputs_of_par externals_of_par)
57  apply auto
58  apply (simp add: compositionality_tr)
59  apply (subgoal_tac "ext A1 = ext A2 \<and> ext B1 = ext B2")
60  prefer 2
61  apply (simp add: externals_def)
62  apply (erule conjE)+
63  text \<open>rewrite with proven subgoal\<close>
64  apply (simp add: externals_of_par)
65  apply auto
66  text \<open>2 goals, the 3rd has been solved automatically\<close>
67  text \<open>1: \<open>Filter A2 x \<in> traces A2\<close>\<close>
68  apply (drule_tac A = "traces A1" in subsetD)
69  apply assumption
70  apply (simp add: Filter_actAisFilter_extA)
71  text \<open>2: \<open>Filter B2 x \<in> traces B2\<close>\<close>
72  apply (drule_tac A = "traces B1" in subsetD)
73  apply assumption
74  apply (simp add: Filter_actAisFilter_extA2)
75  done
76
77end
78