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